def go_ok

bend-collections-laws-math@1.0.0.0 · proofs/lib/u32div.bend:160

import Base

160# the invariant holds for every prefix of the dividend
161def go_ok(+m: Nat, +a: Word(m), +b: U32, +hb: {Nat.is_lt(0n, v(b)) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}) -> inv(m, a, v(b), U32.divmod.go(m, a, b)):
162  match m a:
163    case 0n WNil{}:
164      ({==}, hb)
165    case 1n+p WCon{a0, hi}:
166      rec_ok(p, a0, b, hi, U32.divmod.go(p, hi, b), go_ok(p, hi, b, hb, one, h1), one, h1)