law go_eq

lawful-words@0.1.0.0 · proof_nat.bend:943

import Base

943# The loop of Nat.divmod keeps d * b + r + n, with b = 1 + bp and m + r = bp.
944law go_eq:
945  for +n: Nat
946  for +m: Nat
947  for +d: Nat
948  for +r: Nat
949  for +bp: Nat
950  for +h: {Nat.add(m, r) == bp : Nat}
951  {Nat.add(Nat.mul(Pair.fst(Nat, Nat, Nat.divmod.go(n, m, d, r)), 1n+bp), Pair.snd(Nat, Nat, Nat.divmod.go(n, m, d, r)))
952    == Nat.add(Nat.mul(d, 1n+bp), Nat.add(r, n)) : Nat}