law divstep1

lawful-words@0.1.0.0 · proof_u32.bend:642

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

642# One step of long division, as numbers (quotient bit 1, then 0).
643law divstep1:
644  for +q: Nat
645  for +b: Nat
646  for +r: Nat
647  for +h: Nat
648  for +a0: Bool
649  for +r2: Nat
650  for +e1: {Nat.add(Nat.mul(q, b), r) == h : Nat}
651  for +e: {Nat.add(b, r2) == Nat.add(N.bn(a0), Nat.double(r)) : Nat}
652  {Nat.add(Nat.mul(1n+Nat.double(q), b), r2) == Nat.add(N.bn(a0), Nat.double(h)) : Nat}