def internal_dm_fin

bend-mathlib@0.8.1.0 · u32.bend:868

import Base
import bend-mathlib@0.8.1.0/nat.bend as MNat

868def internal_dm_fin(+p: Nat, +q: Word(p), +s: Word(32n), +b: U32, +x: Bool, +r: Nat, -a: Nat, +m: Nat, +em: {Nat.pow(2n, 32n) == m : Nat}, t: Bool, g: Bool, ea: {Nat.add(Nat.mul(Word.to_nat(p, q), U32.to_nat(b)), r) == a : Nat}, +hr: MNat.lt(r, U32.to_nat(b)), es: {Nat.add(Word.to_nat(32n, s), Bool.pick(Nat, t, m, 0n)) == Nat.add(internal_bv(x), Nat.double(r)) : Nat}, eg: {Bool.or(t, U32.is_ge(U32{s}, b)) == g : Bool}) -> internal_dm_inv(1n+p, U32.to_nat(b), Nat.add(internal_bv(x), Nat.double(a)), U32.divmod.go.fin(p, q, U32{s}, b, g)):
869  match t g:
870    case True{} True{}:
871      internal_dm_take(p, q, U32.to_nat(b), U32.to_nat(U32.sub(U32{s}, b)), x, r, a, ea, hr, internal_dm_wrap(b, s, x, r, m, em, hr, es))
872    case True{} False{}:
873      Empty.absurd(internal_dm_inv(1n+p, U32.to_nat(b), Nat.add(internal_bv(x), Nat.double(a)), U32.divmod.go.fin(p, q, U32{s}, b, False{})), MNat.internal_div_true_ne_false(eg))
874    case False{} True{}:
875      +bn = U32.to_nat(b)
876      +sn = Word.to_nat(32n, s)
877      +hle = Equal.trans(Bool, Nat.is_le(bn, sn), U32.is_ge(U32{s}, b), True{}, Equal.trans(Bool, Nat.is_le(bn, sn), Nat.is_ge(sn, bn), U32.is_ge(U32{s}, b), MNat.is_ge_eq_is_le_sym(sn, bn), Equal.sym(Bool, U32.is_ge(U32{s}, b), Nat.is_ge(sn, bn), u32_is_ge_to_nat(U32{s}, b))), eg)
878      +e2 = Equal.trans(Nat, Nat.add(bn, U32.to_nat(U32.sub(U32{s}, b))), Nat.add(bn, Nat.sub(sn, bn)), Nat.add(internal_bv(x), Nat.double(r)), Equal.cong(Nat, Nat, z => Nat.add(bn, z), U32.to_nat(U32.sub(U32{s}, b)), Nat.sub(sn, bn), u32_sub_exact(U32{s}, b, hle)), Equal.trans(Nat, Nat.add(bn, Nat.sub(sn, bn)), sn, Nat.add(internal_bv(x), Nat.double(r)), MNat.add_sub_of_le(bn, sn, hle), Equal.trans(Nat, sn, Nat.add(sn, 0n), Nat.add(internal_bv(x), Nat.double(r)), MNat.add_zero_sym(sn), es)))
879      internal_dm_take(p, q, bn, U32.to_nat(U32.sub(U32{s}, b)), x, r, a, ea, hr, e2)
880    case False{} False{}:
881      +bn = U32.to_nat(b)
882      +sn = Word.to_nat(32n, s)
883      +hnle = Equal.trans(Bool, Nat.is_le(bn, sn), U32.is_ge(U32{s}, b), False{}, Equal.trans(Bool, Nat.is_le(bn, sn), Nat.is_ge(sn, bn), U32.is_ge(U32{s}, b), MNat.is_ge_eq_is_le_sym(sn, bn), Equal.sym(Bool, U32.is_ge(U32{s}, b), Nat.is_ge(sn, bn), u32_is_ge_to_nat(U32{s}, b))), eg)
884      +ek = Equal.trans(Nat, sn, Nat.add(sn, 0n), Nat.add(internal_bv(x), Nat.double(r)), MNat.add_zero_sym(sn), es)
885      (internal_div_step(0n, Word.to_nat(p, q), bn, sn, internal_bv(x), r, a, ek, ea), MNat.lt_of_not_le(bn, sn, hnle))