def sub_cons

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/w64add.bend:287

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as WD
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32.bend as U3
import bend-collections-laws-crypto@1.0.0.0/proofs/math/u64/u64.bend as P64
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32alg.bend as A

287def sub_cons(+one: Nat, +h1: {one == 1n : Nat}, +x: U32, +y: U32) -> {Nat.add(v(U32.sub(x, y)), v(y)) == Nat.add(v(x), C.shift(32n, WD.bo(U32.is_lt(x, y), one))) : Nat}:
288  +d = U32.sub(x, y)
289  +cc = P64.carry32(d, y)
290  +e0 = acons_o(one, h1, d, y)
291  +e1 = L.subst(U32, z => {Nat.add(v(z), C.shift(32n, WD.bo(cc, one))) == Nat.add(v(d), v(y)) : Nat}, U32.add(d, y), x, A.sub_add(x, y), e0)
292  +ec = Equal.trans(Bool, cc, Nat.is_lt(v(x), v(y)), U32.is_lt(x, y), borrow_eq(one, h1, v(x), v(d), v(y), cc, e1, vb(d)), Equal.sym(Bool, U32.is_lt(x, y), Nat.is_lt(v(x), v(y)), U3.is_lt_nat(x, y)))
293  +e2 = L.subst(Bool, t => {Nat.add(v(x), C.shift(32n, WD.bo(t, one))) == Nat.add(v(d), v(y)) : Nat}, cc, U32.is_lt(x, y), ec, e1)
294  Equal.sym(Nat, Nat.add(v(x), C.shift(32n, WD.bo(U32.is_lt(x, y), one))), Nat.add(v(d), v(y)), e2)