def rec_ok

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

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD

149def rec_ok(+p: Nat, +a0: Bool, +b: U32, +hi: Word(p), qr: Word(p) & U32, ih: inv(p, hi, v(b), qr), +one: Nat, +h1: {one == 1n : Nat}) -> inv(1n+p, WCon{a0, hi}, v(b), U32.divmod.go.rec(p, a0, b, qr)):
150  match qr:
151    case (+q, +r):
152      match r:
153        case U32{+rw}:
154          (he, hr) = ih
155          +hts = Equal.trans(Nat, Nat.add(WD.uw(32n, WD.ow(32n, Word.shl.out(32n, a0, rw))), WD.sc(32n, WD.bo(WD.ob(32n, Word.shl.out(32n, a0, rw)), one))), Nat.add(S.bit_value(a0), Nat.double(WD.uw(32n, rw))), Nat.add(S.bit_value(a0), Nat.double(v(U32{rw}))),
156            WD.shl_out1(32n, one, h1, a0, rw),
157            Equal.cong(Nat, Nat, z => Nat.add(S.bit_value(a0), Nat.double(z)), WD.uw(32n, rw), v(U32{rw}), Equal.sym(Nat, v(U32{rw}), WD.uw(32n, rw), vw(rw))))
158          shl_ok(p, q, b, Word.shl.out(32n, a0, rw), a0, hi, v(U32{rw}), one, h1, he, hr, hts)