ProofU32.dm_fin.t: def of lawful-words@0.1.0.0 Import: import lawful-words@0.1.0.0/proof_u32.bend as ProofU32 Lines 731-781 of lawful-words@0.1.0.0/proof_u32.bend: https://jend.leeeet.dev/read.txt?path=lawful-words@0.1.0.0/proof_u32.bend&start_line=731&end_line=781 import Base import lawful-words@0.1.0.0/proof_nat.bend as N import lawful-words@0.1.0.0/proof_word.bend as W # The quotient bit is 1: the remainder becomes 2r + a0 - b. def dm_fin.t(+p: Nat, +q: Word(p), +s: Word(32n), +t: Bool, +b: U32, +a0: Bool, +hi: Word(p), +r: Nat, +m: Nat, +hm: {Nat.pow(2n, 32n) == m : Nat}, +g: Bool, +eg: {Bool.or(t, U32.is_ge(U32{s}, b)) == g : Bool}, +e1: {Nat.add(Nat.mul(Word.to_nat(p, q), U32.to_nat(b)), r) == Word.to_nat(p, hi) : Nat}, +e2: {Nat.is_lt(r, U32.to_nat(b)) == True{} : Bool}, +ep: {Nat.add(Word.to_nat(32n, s), Nat.mul(N.bn(t), m)) == Nat.add(N.bn(a0), Nat.double(r)) : Nat}) -> DMOK(1n+p, Nat.add(N.bn(a0), Nat.double(Word.to_nat(p, hi))), U32.to_nat(b), U32.divmod.go.fin(p, q, U32{s}, b, g)): match t g: case True{} True{}: +bb = U32.to_nat(b) +sv = Word.to_nat(32n, s) +rr = Nat.add(N.bn(a0), Nat.double(r)) # 2r + a0 = s + m +er = Equal.trans(Nat, rr, Nat.add(sv, Nat.mul(1n, m)), Nat.add(sv, m), Equal.sym(Nat, Nat.add(sv, Nat.mul(1n, m)), rr, ep), Equal.cong(Nat, Nat, z => Nat.add(sv, z), Nat.mul(1n, m), m, N.add_zero(m))) +hle = N.lt_to_le(bb, rr, %Equal.sym(Nat, rr, Nat.add(sv, m), er) : {Nat.is_lt(bb, _) == True{} : Bool}; N.lt_le_trans(bb, m, Nat.add(sv, m), to_nat_lt.m(b, m, hm), N.le_add_l(m, sv))) +hlt = sub_lt_dbl(rr, bb, W.lt_dbl_bit(r, bb, a0, e2), hle) +ev = Equal.trans(Nat, U32.to_nat(U32.sub(U32{s}, b)), Nat.mod(Nat.sub(Nat.add(sv, m), bb), m), Nat.sub(rr, bb), to_nat_sub.m(U32{s}, b, m, hm), %er : {Nat.mod(Nat.sub(_, bb), m) == Nat.sub(rr, bb) : Nat} N.mod_small(Nat.sub(rr, bb), m, N.lt_trans(Nat.sub(rr, bb), bb, m, hlt, to_nat_lt.m(b, m, hm)))) (%Equal.sym(Nat, U32.to_nat(U32.sub(U32{s}, b)), Nat.sub(rr, bb), ev) : {Nat.add(Nat.mul(1n+Nat.double(Word.to_nat(p, q)), bb), _) == Nat.add(N.bn(a0), Nat.double(Word.to_nat(p, hi))) : Nat} divstep1(Word.to_nat(p, q), bb, r, Word.to_nat(p, hi), a0, Nat.sub(rr, bb), e1, N.le_sub_add(bb, rr, hle)), %Equal.sym(Nat, U32.to_nat(U32.sub(U32{s}, b)), Nat.sub(rr, bb), ev) : {Nat.is_lt(_, bb) == True{} : Bool}; hlt) case True{} False{}: Empty.absurd(DMOK(1n+p, Nat.add(N.bn(a0), Nat.double(Word.to_nat(p, hi))), U32.to_nat(b), (WCon{False{}, q}, U32{s})), N.true_ne_false(eg)) case False{} True{}: +bb = U32.to_nat(b) +sv = Word.to_nat(32n, s) +rr = Nat.add(N.bn(a0), Nat.double(r)) +er = Equal.trans(Nat, rr, Nat.add(sv, 0n), sv, Equal.sym(Nat, Nat.add(sv, 0n), rr, ep), N.add_zero(sv)) +hle = {%Equal.sym(Nat, rr, sv, er) : {Nat.is_le(bb, _) == True{} : Bool}; %ge_le(sv, bb) : {_ == True{} : Bool}; %is_ge_to_nat(U32{s}, b) : {_ == True{} : Bool}; eg : {Nat.is_le(bb, rr) == True{} : Bool}} +hlt = sub_lt_dbl(rr, bb, W.lt_dbl_bit(r, bb, a0, e2), hle) +ev = Equal.trans(Nat, U32.to_nat(U32.sub(U32{s}, b)), Nat.mod(Nat.sub(Nat.add(sv, m), bb), m), Nat.sub(rr, bb), to_nat_sub.m(U32{s}, b, m, hm), %Equal.sym(Nat, rr, sv, er) : {Nat.mod(Nat.sub(Nat.add(sv, m), bb), m) == Nat.sub(_, bb) : Nat} %Equal.sym(Nat, Nat.sub(Nat.add(sv, m), bb), Nat.add(Nat.sub(sv, bb), m), sub_add_comm(sv, m, bb, %er : {Nat.is_le(bb, _) == True{} : Bool}; hle)) : {Nat.mod(_, m) == Nat.sub(sv, bb) : Nat} %Equal.sym(Nat, Nat.mod(Nat.add(Nat.sub(sv, bb), m), m), Nat.mod(Nat.sub(sv, bb), m), mod_add_self(Nat.sub(sv, bb), m)) : {_ == Nat.sub(sv, bb) : Nat} N.mod_small(Nat.sub(sv, bb), m, N.le_lt_trans(Nat.sub(sv, bb), sv, m, sub_le(sv, bb), wlt.m(s, m, hm)))) (%Equal.sym(Nat, U32.to_nat(U32.sub(U32{s}, b)), Nat.sub(rr, bb), ev) : {Nat.add(Nat.mul(1n+Nat.double(Word.to_nat(p, q)), bb), _) == Nat.add(N.bn(a0), Nat.double(Word.to_nat(p, hi))) : Nat} divstep1(Word.to_nat(p, q), bb, r, Word.to_nat(p, hi), a0, Nat.sub(rr, bb), e1, N.le_sub_add(bb, rr, hle)), %Equal.sym(Nat, U32.to_nat(U32.sub(U32{s}, b)), Nat.sub(rr, bb), ev) : {Nat.is_lt(_, bb) == True{} : Bool}; hlt) case False{} False{}: +bb = U32.to_nat(b) +sv = Word.to_nat(32n, s) +er = Equal.trans(Nat, sv, Nat.add(sv, 0n), Nat.add(N.bn(a0), Nat.double(r)), Equal.sym(Nat, Nat.add(sv, 0n), sv, N.add_zero(sv)), ep) +hlt = N.not_le_lt(bb, sv, %ge_le(sv, bb) : {_ == False{} : Bool}; %is_ge_to_nat(U32{s}, b) : {_ == False{} : Bool}; eg) (divstep0(Word.to_nat(p, q), bb, r, Word.to_nat(p, hi), a0, sv, e1, er), hlt) Uses (48): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.or https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.double https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mod https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.pow https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32 https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.divmod.go.fin https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_ge https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.sub https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Con https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.to_nat https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=add_zero https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=bn https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=le_add_l https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=le_lt_trans https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=le_sub_add https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=lt_le_trans https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=lt_to_le https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=lt_trans https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=mod_small https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=not_le_lt https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=true_ne_false https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_u32.bend&name=DMOK https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_u32.bend&name=divstep0 https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_u32.bend&name=divstep1 https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_u32.bend&name=ge_le https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_u32.bend&name=is_ge_to_nat https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_u32.bend&name=mod_add_self https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_u32.bend&name=sub_add_comm https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_u32.bend&name=sub_le https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_u32.bend&name=sub_lt_dbl https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_u32.bend&name=to_nat_lt.m https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_u32.bend&name=to_nat_sub.m https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_u32.bend&name=wlt.m https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_word.bend&name=lt_dbl_bit