def eq_limbs

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

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C

332def eq_limbs(+k: Nat, +x1: Nat, +y1: Nat, +x2: Nat, +y2: Nat, +hx1: {C.fits(k, x1) == True{} : Bool}, +hx2: {C.fits(k, x2) == True{} : Bool}) -> {Bool.and(Nat.is_eq(x1, x2), Nat.is_eq(y1, y2)) == Nat.is_eq(Nat.add(x1, C.shift(k, y1)), Nat.add(x2, C.shift(k, y2))) : Bool}:
333  eq_limbs_c(k, x1, y1, x2, y2, hx1, hx2, Nat.is_eq(Nat.add(x1, C.shift(k, y1)), Nat.add(x2, C.shift(k, y2))), {==})