def wsd.k1

bend-osdev-word64@0.1.1.0 · PROOF_text.bend:165

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

165def 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}:
166  +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))))
167  +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)))
168  +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))
169  (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))