def eq_limbs_f

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

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

308def eq_limbs_f(+k: Nat, +x1: Nat, +y1: Nat, +x2: Nat, +y2: Nat, +d1: Bool, +d2: Bool, +h1: {Nat.is_eq(x1, x2) == d1 : Bool}, +h2: {Nat.is_eq(y1, y2) == d2 : Bool}, +he: {Nat.is_eq(Nat.add(x1, C.shift(k, y1)), Nat.add(x2, C.shift(k, y2))) == False{} : Bool}) -> {Bool.and(d1, d2) == False{} : Bool}:
309  match d1 d2:
310    case True{} True{}:
311      +ex = N.eq_from_is_eq(x1, x2, h1)
312      +ey = N.eq_from_is_eq(y1, y2, h2)
313      +e = L.subst(Nat, z => {Nat.is_eq(Nat.add(x1, C.shift(k, y1)), Nat.add(z, C.shift(k, y1))) == False{} : Bool}, x2, x1, Equal.sym(Nat, x1, x2, ex), L.subst(Nat, z => {Nat.is_eq(Nat.add(x1, C.shift(k, y1)), Nat.add(x2, C.shift(k, z))) == False{} : Bool}, y2, y1, Equal.sym(Nat, y1, y2, ey), he))
314      Empty.absurd({True{} == False{} : Bool}, L.false_true(Equal.trans(Bool, False{}, Nat.is_eq(Nat.add(x1, C.shift(k, y1)), Nat.add(x1, C.shift(k, y1))), True{}, Equal.sym(Bool, Nat.is_eq(Nat.add(x1, C.shift(k, y1)), Nat.add(x1, C.shift(k, y1))), False{}, e), N.is_eq_refl(Nat.add(x1, C.shift(k, y1))))))
315    case True{} False{}:
316      {==}
317    case False{} _:
318      {==}