def lt_limbs_c

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/width.bend:292

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/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L

292def lt_limbs_c(+k: Nat, +x1: Nat, +y1: Nat, +x2: Nat, +y2: Nat, +hx1: {C.fits(k, x1) == True{} : Bool}, +hx2: {C.fits(k, x2) == True{} : Bool}, +c: Bool, +d: Bool, +hc: {Nat.is_lt(y1, y2) == c : Bool}, +hd: {Nat.is_eq(y1, y2) == d : Bool}) -> {Bool.or(c, Bool.and(d, Nat.is_lt(x1, x2))) == Nat.is_lt(Nat.add(x1, C.shift(k, y1)), Nat.add(x2, C.shift(k, y2))) : Bool}:
293  match c d:
294    case True{} _:
295      Equal.sym(Bool, Nat.is_lt(Nat.add(x1, C.shift(k, y1)), Nat.add(x2, C.shift(k, y2))), True{}, lt_hi(k, x1, y1, x2, y2, hx1, hc))
296    case False{} True{}:
297      +ey = N.eq_from_is_eq(y1, y2, hd)
298      +e1 = L.subst(Nat, z => {Nat.is_lt(Nat.add(x1, C.shift(k, y1)), Nat.add(x2, C.shift(k, z))) == Nat.is_lt(x1, x2) : Bool}, y1, y2, ey, lt_cancel_r(x1, x2, C.shift(k, y1)))
299      Equal.sym(Bool, Nat.is_lt(Nat.add(x1, C.shift(k, y1)), Nat.add(x2, C.shift(k, y2))), Nat.is_lt(x1, x2), e1)
300    case False{} False{}:
301      +h21 = N.lt_or_eq(y2, y1, N.not_lt_le(y1, y2, hc), N.is_eq_sym_false(y1, y2, hd))
302      +hb = lt_hi(k, x2, y2, x1, y1, hx2, h21)
303      Equal.sym(Bool, Nat.is_lt(Nat.add(x1, C.shift(k, y1)), Nat.add(x2, C.shift(k, y2))), False{}, N.le_not_lt(Nat.add(x1, C.shift(k, y1)), Nat.add(x2, C.shift(k, y2)), N.lt_le(Nat.add(x2, C.shift(k, y2)), Nat.add(x1, C.shift(k, y1)), hb)))