def borrow_eq

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

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/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW

274# x - y mod 2^32, plus y, is x plus 2^32 when x < y
275def borrow_eq(+one: Nat, +h1: {one == 1n : Nat}, +vx: Nat, +vs: Nat, +vy: Nat, +cc: Bool, +e: {Nat.add(vx, C.shift(32n, WD.bo(cc, one))) == Nat.add(vs, vy) : Nat}, +hs: {C.fits(32n, vs) == True{} : Bool}) -> {cc == Nat.is_lt(vx, vy) : Bool}:
276  match cc:
277    case True{}:
278      +h1s = WW.lt_one(32n, one, h1, vs, hs)
279      +h2 = L.subst(Nat, z => {Nat.is_lt(Nat.add(vs, vy), z) == True{} : Bool}, Nat.add(C.shift(32n, one), vy), Nat.add(vy, C.shift(32n, one)), N.add_comm(C.shift(32n, one), vy), N.lt_add_r2(vs, C.shift(32n, one), vy, h1s))
280      +h3 = L.subst(Nat, z => {Nat.is_lt(z, Nat.add(vy, C.shift(32n, one))) == True{} : Bool}, Nat.add(vs, vy), Nat.add(vx, C.shift(32n, one)), Equal.sym(Nat, Nat.add(vx, C.shift(32n, one)), Nat.add(vs, vy), e), h2)
281      Equal.sym(Bool, Nat.is_lt(vx, vy), True{}, Equal.trans(Bool, Nat.is_lt(vx, vy), Nat.is_lt(Nat.add(vx, C.shift(32n, one)), Nat.add(vy, C.shift(32n, one))), True{}, Equal.sym(Bool, Nat.is_lt(Nat.add(vx, C.shift(32n, one)), Nat.add(vy, C.shift(32n, one))), Nat.is_lt(vx, vy), WW.lt_cancel_r(vx, vy, C.shift(32n, one))), h3))
282    case False{}:
283      +e0 = Equal.trans(Nat, vx, Nat.add(vx, C.shift(32n, 0n)), Nat.add(vs, vy), Equal.sym(Nat, Nat.add(vx, C.shift(32n, 0n)), vx, Equal.trans(Nat, Nat.add(vx, C.shift(32n, 0n)), Nat.add(vx, 0n), vx, Equal.cong(Nat, Nat, t => Nat.add(vx, t), C.shift(32n, 0n), 0n, WW.shift_zero(32n)), N.add_zero(vx))), e)
284      +hle = L.subst(Nat, z => {Nat.is_le(vy, z) == True{} : Bool}, Nat.add(vy, vs), vx, Equal.trans(Nat, Nat.add(vy, vs), Nat.add(vs, vy), vx, N.add_comm(vy, vs), Equal.sym(Nat, vx, Nat.add(vs, vy), e0)), N.le_add_right(vy, vs))
285      Equal.sym(Bool, Nat.is_lt(vx, vy), False{}, N.le_not_lt(vx, vy, hle))