law split_step

lawful-words@0.1.0.0 · proof_word.bend:1110

import Base
import lawful-words@0.1.0.0/proof_nat.bend as N

1110# y + 2r = 2a + (y + 2b) when r = a + b.
1111law split_step:
1112  for +y: Bool
1113  for +a: Nat
1114  for +b: Nat
1115  for +r: Nat
1116  for +ih: {r == Nat.add(a, b) : Nat}
1117  {Nat.add(N.bn(y), Nat.double(r)) == Nat.add(Nat.double(a), Nat.add(N.bn(y), Nat.double(b))) : Nat}