U64bgcd.of48v: def of bend-collections-laws-math@1.0.0.0 Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64bgcd.bend as U64bgcd Lines 207-223 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64bgcd.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64bgcd.bend&start_line=207&end_line=223 import Base import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natlight.bend as SR import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X # the two words of g < 2^64 def of48v(+one: Nat, +h1: {one == 1n : Nat}, +g: Nat, +hg: {C.fits(64n, g) == True{} : Bool}) -> {v(X.of48(g)) == g : Nat}: +r1 = Nat.mod(g, 65536n) +r2 = Nat.mod(Nat.div(g, 65536n), 65536n) +h = Nat.div(Nat.div(g, 65536n), 65536n) +L0 = Nat.add(C.shift(16n, r2), r1) +M = Nat.mul(Nat.mul(h, 65536n), 65536n) +es = o48_split(one, h1, g) +eg = Equal.sym(Nat, Nat.add(C.shift(32n, h), L0), g, Equal.trans(Nat, Nat.add(C.shift(32n, h), L0), Nat.add(L0, C.shift(32n, h)), g, NA.add_comm(C.shift(32n, h), L0), es)) +eE = Equal.trans(Nat, Nat.sub(g, M), Nat.sub(g, C.shift(32n, h)), Nat.sub(Nat.add(C.shift(32n, h), L0), C.shift(32n, h)), Equal.cong(Nat, Nat, z => Nat.sub(g, z), M, C.shift(32n, h), s32(one, h1, h)), Equal.cong(Nat, Nat, z => Nat.sub(z, C.shift(32n, h)), g, Nat.add(C.shift(32n, h), L0), eg)) +eL = Equal.trans(Nat, Nat.sub(g, M), Nat.sub(Nat.add(C.shift(32n, h), L0), C.shift(32n, h)), L0, eE, N.add_sub_cancel(C.shift(32n, h), L0)) +bL = o48_lo_lt(one, h1, r1, r2, SR.dml(g, 65536n, {==}), SR.dml(Nat.div(g, 65536n), 65536n, {==})) +bLo = L.subst(Nat, z => {Nat.is_lt(z, C.shift(32n, one)) == True{} : Bool}, L0, Nat.sub(g, M), Equal.sym(Nat, Nat.sub(g, M), L0, eL), bL) +bh = o48_hi_lt(one, h1, g, hg, L0, h, es) +eLo = Equal.trans(Nat, U32.to_nat(U32.from_nat(Nat.sub(g, M))), Nat.sub(g, M), L0, tnfn(one, h1, Nat.sub(g, M), bLo), eL) +f1 = Equal.trans(Nat, Nat.add(U32.to_nat(U32.from_nat(Nat.sub(g, M))), C.shift(32n, U32.to_nat(U32.from_nat(h)))), Nat.add(L0, C.shift(32n, U32.to_nat(U32.from_nat(h)))), Nat.add(L0, C.shift(32n, h)), Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(32n, U32.to_nat(U32.from_nat(h)))), U32.to_nat(U32.from_nat(Nat.sub(g, M))), L0, eLo), Equal.cong(Nat, Nat, z => Nat.add(L0, C.shift(32n, z)), U32.to_nat(U32.from_nat(h)), h, tnfn(one, h1, h, bh))) Equal.trans(Nat, v(X.of48(g)), Nat.add(L0, C.shift(32n, h)), g, f1, es) Uses (26): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool 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.div 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.sub https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.from_nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_comm https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend&name=subst https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=add_sub_cancel https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/natlight.bend&name=dml https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64bgcd.bend&name=o48_hi_lt https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64bgcd.bend&name=o48_lo_lt https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64bgcd.bend&name=o48_split https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64bgcd.bend&name=s32 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64bgcd.bend&name=tnfn https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64bgcd.bend&name=v https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=fits https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=shift https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/w64.bend&name=of48