def fin_false

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/u32div.bend:129

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/word_comparison.bend as WC

129def fin_false(+p: Nat, +q: Word(p), +s: U32, +b: U32, +a0: Bool, +hi: Word(p), +r: Nat, +he: {Nat.add(Nat.mul(S.unsigned(p, q), v(b)), r) == S.unsigned(p, hi) : Nat}, +hr: {Nat.is_lt(r, v(b)) == True{} : Bool}, +hs: {v(s) == Nat.add(S.bit_value(a0), Nat.double(r)) : Nat}, +g: Bool, +hg: {U32.is_ge(s, b) == g : Bool}) -> inv(1n+p, WCon{a0, hi}, v(b), U32.divmod.go.fin(p, q, s, b, g)):
130  match g:
131    case True{}:
132      fin_ge(p, q, s, b, a0, hi, r, he, hr, hs, Equal.trans(Bool, Nat.is_ge(v(s), v(b)), U32.is_ge(s, b), True{}, Equal.sym(Bool, U32.is_ge(s, b), Nat.is_ge(v(s), v(b)), WC.u32_ge(s, b)), hg))
133    case False{}:
134      fin_lt(p, q, s, b, a0, hi, r, he, hs, Equal.trans(Bool, Nat.is_ge(v(s), v(b)), U32.is_ge(s, b), False{}, Equal.sym(Bool, U32.is_ge(s, b), Nat.is_ge(v(s), v(b)), WC.u32_ge(s, b)), hg))