PROOFText.wsd.k1: def of bend-osdev-word64@0.1.1.0 Import: import bend-osdev-word64@0.1.1.0/PROOF_text.bend as PROOFText Lines 165-169 of bend-osdev-word64@0.1.1.0/PROOF_text.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-word64@0.1.1.0/PROOF_text.bend&start_line=165&end_line=169 import Base import bend-osdev-u32@0.1.0.0/u32.bend as U import bend-osdev-u32@0.1.0.0/LAWS.bend as UL import bend-osdev-word64@0.1.1.0/proof_value.bend as P import bend-osdev-u32@0.1.0.0/LAWS_order.bend as UO def wsd.k1(+n: Nat, +h: Nat, +R: Nat, +C: Nat, +Vm: Nat, +V: Nat, +cA: Nat, +en: {Nat.add(h, h) == n : Nat}, +h10: {Nat.is_le(10n, U.U32Nat.dbl(h, 1n)) == True{} : Bool}, +hR: {Nat.is_lt(R, 10n) == True{} : Bool}, +hC: {Nat.is_lt(C, U.U32Nat.dbl(h, 1n)) == True{} : Bool}, +em: {Vm == U.U32Nat.low(n, U.U32Nat.dbl(h, R)) : Nat}, +ea: {Nat.add(V, U.U32Nat.dbl(n, cA)) == Nat.add(Vm, C) : Nat}) -> {V == Nat.add(U.U32Nat.dbl(h, R), C) : Nat} & {Nat.is_lt(V, U.U32Nat.dbl(h, 10n)) == True{} : Bool}: +evm = Equal.trans(Nat, Vm, U.U32Nat.low(n, U.U32Nat.dbl(h, R)), U.U32Nat.dbl(h, R), em, UL.low_small(n, U.U32Nat.dbl(h, R), wsd.kn(n, h, U.U32Nat.dbl(h, R), en, h10, Equal.trans(Bool, Nat.is_lt(U.U32Nat.dbl(h, R), U.U32Nat.dbl(h, 10n)), Nat.is_lt(R, 10n), True{}, UL.dbl_lt(h, R, 10n), hR)))) +vlt = UO.nat_lt_le_trans(Nat.add(U.U32Nat.dbl(h, R), C), U.U32Nat.dbl(h, 1n+R), U.U32Nat.dbl(h, 10n), Equal.trans(Bool, Nat.is_lt(Nat.add(U.U32Nat.dbl(h, R), C), U.U32Nat.dbl(h, 1n+R)), Nat.is_lt(Nat.add(U.U32Nat.dbl(h, R), C), Nat.add(Nat.sub(U.U32Nat.dbl(h, 1n), 1n+C), 1n+Nat.add(U.U32Nat.dbl(h, R), C))), True{}, Equal.sym(Bool, Nat.is_lt(Nat.add(U.U32Nat.dbl(h, R), C), Nat.add(Nat.sub(U.U32Nat.dbl(h, 1n), 1n+C), 1n+Nat.add(U.U32Nat.dbl(h, R), C))), Nat.is_lt(Nat.add(U.U32Nat.dbl(h, R), C), U.U32Nat.dbl(h, 1n+R)), Equal.cong(Nat, Bool, zz => Nat.is_lt(Nat.add(U.U32Nat.dbl(h, R), C), zz), Nat.add(Nat.sub(U.U32Nat.dbl(h, 1n), 1n+C), 1n+Nat.add(U.U32Nat.dbl(h, R), C)), U.U32Nat.dbl(h, 1n+R), Equal.trans(Nat, Nat.add(Nat.sub(U.U32Nat.dbl(h, 1n), 1n+C), 1n+Nat.add(U.U32Nat.dbl(h, R), C)), Nat.add(U.U32Nat.dbl(h, R), U.U32Nat.dbl(h, 1n)), U.U32Nat.dbl(h, 1n+R), Equal.trans(Nat, Nat.add(Nat.sub(U.U32Nat.dbl(h, 1n), 1n+C), 1n+Nat.add(U.U32Nat.dbl(h, R), C)), Nat.add(U.U32Nat.dbl(h, R), Nat.add(Nat.sub(U.U32Nat.dbl(h, 1n), 1n+C), 1n+C)), Nat.add(U.U32Nat.dbl(h, R), U.U32Nat.dbl(h, 1n)), wr.t2(Nat.sub(U.U32Nat.dbl(h, 1n), 1n+C), h, R, C), Equal.cong(Nat, Nat, zz => Nat.add(U.U32Nat.dbl(h, R), zz), Nat.add(Nat.sub(U.U32Nat.dbl(h, 1n), 1n+C), 1n+C), U.U32Nat.dbl(h, 1n), UL.nat_lt_witness(C, U.U32Nat.dbl(h, 1n), hC))), wr.t3(h, R)))), UL.nat_lt_add(Nat.add(U.U32Nat.dbl(h, R), C), Nat.sub(U.U32Nat.dbl(h, 1n), 1n+C))), Equal.trans(Bool, Nat.is_le(U.U32Nat.dbl(h, 1n+R), U.U32Nat.dbl(h, 10n)), Nat.is_le(1n+R, 10n), True{}, UL.dbl_le(h, 1n+R, 10n), Equal.trans(Bool, Nat.is_le(1n+R, 10n), Nat.is_lt(R, 10n), True{}, P.wn.le_succ(R, 10n), hR))) +ev = Equal.trans(Nat, V, Nat.add(Vm, C), Nat.add(U.U32Nat.dbl(h, R), C), UL.dbl_nowrap(n, cA, V, Nat.add(Vm, C), Nat.add(U.U32Nat.dbl(h, R), C), ea, Equal.trans(Bool, Nat.is_le(Nat.add(Vm, C), Nat.add(U.U32Nat.dbl(h, R), C)), Nat.is_le(Nat.add(U.U32Nat.dbl(h, R), C), Nat.add(U.U32Nat.dbl(h, R), C)), True{}, Equal.cong(Nat, Bool, zz => Nat.is_le(zz, Nat.add(U.U32Nat.dbl(h, R), C)), Nat.add(Vm, C), Nat.add(U.U32Nat.dbl(h, R), C), Equal.cong(Nat, Nat, zz => Nat.add(zz, C), Vm, U.U32Nat.dbl(h, R), evm)), UL.nat_le_refl(Nat.add(U.U32Nat.dbl(h, R), C))), wsd.kn(n, h, Nat.add(U.U32Nat.dbl(h, R), C), en, h10, vlt)), Equal.cong(Nat, Nat, zz => Nat.add(zz, C), Vm, U.U32Nat.dbl(h, R), evm)) (ev, Equal.trans(Bool, Nat.is_lt(V, U.U32Nat.dbl(h, 10n)), Nat.is_lt(Nat.add(U.U32Nat.dbl(h, R), C), U.U32Nat.dbl(h, 10n)), True{}, Equal.cong(Nat, Bool, zz => Nat.is_lt(zz, U.U32Nat.dbl(h, 10n)), V, Nat.add(U.U32Nat.dbl(h, R), C), Equal.sym(Nat, Nat.add(U.U32Nat.dbl(h, R), C), V, Equal.sym(Nat, V, Nat.add(U.U32Nat.dbl(h, R), C), ev))), vlt)) Uses (25): 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.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.sub https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=dbl_le https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=dbl_lt https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=dbl_nowrap https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=low_small https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=nat_le_refl https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=nat_lt_add https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=nat_lt_witness https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS_order.bend&name=nat_lt_le_trans https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/u32.bend&name=U32Nat.dbl https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/u32.bend&name=U32Nat.low https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_text.bend&name=wr.t2 https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_text.bend&name=wr.t3 https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_text.bend&name=wsd.kn https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/proof_value.bend&name=wn.le_succ