def eq_limbs_c

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

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

320def eq_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, +hc: {Nat.is_eq(Nat.add(x1, C.shift(k, y1)), Nat.add(x2, C.shift(k, y2))) == c : Bool}) -> {Bool.and(Nat.is_eq(x1, x2), Nat.is_eq(y1, y2)) == c : Bool}:
321  match c:
322    case True{}:
323      +e = N.eq_from_is_eq(Nat.add(x1, C.shift(k, y1)), Nat.add(x2, C.shift(k, y2)), hc)
324      +ex = Equal.trans(Nat, x1, C.low(k, Nat.add(x1, C.shift(k, y1))), x2, Equal.sym(Nat, C.low(k, Nat.add(x1, C.shift(k, y1))), x1, low_u(k, x1, y1, hx1)), Equal.trans(Nat, C.low(k, Nat.add(x1, C.shift(k, y1))), C.low(k, Nat.add(x2, C.shift(k, y2))), x2, Equal.cong(Nat, Nat, t => C.low(k, t), Nat.add(x1, C.shift(k, y1)), Nat.add(x2, C.shift(k, y2)), e), low_u(k, x2, y2, hx2)))
325      +ey = Equal.trans(Nat, y1, C.high(k, Nat.add(x1, C.shift(k, y1))), y2, Equal.sym(Nat, C.high(k, Nat.add(x1, C.shift(k, y1))), y1, high_u(k, x1, y1, hx1)), Equal.trans(Nat, C.high(k, Nat.add(x1, C.shift(k, y1))), C.high(k, Nat.add(x2, C.shift(k, y2))), y2, Equal.cong(Nat, Nat, t => C.high(k, t), Nat.add(x1, C.shift(k, y1)), Nat.add(x2, C.shift(k, y2)), e), high_u(k, x2, y2, hx2)))
326      +a = L.subst(Nat, z => {Nat.is_eq(x1, z) == True{} : Bool}, x1, x2, ex, N.is_eq_refl(x1))
327      +b = L.subst(Nat, z => {Nat.is_eq(y1, z) == True{} : Bool}, y1, y2, ey, N.is_eq_refl(y1))
328      Equal.trans(Bool, Bool.and(Nat.is_eq(x1, x2), Nat.is_eq(y1, y2)), Bool.and(True{}, Nat.is_eq(y1, y2)), True{}, Equal.cong(Bool, Bool, t => Bool.and(t, Nat.is_eq(y1, y2)), Nat.is_eq(x1, x2), True{}, a), b)
329    case False{}:
330      eq_limbs_f(k, x1, y1, x2, y2, Nat.is_eq(x1, x2), Nat.is_eq(y1, y2), {==}, {==}, hc)