def odd_limb

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

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

346def odd_limb(+p: Nat, +x: Nat, +y: Nat) -> {Nat.mod(Nat.add(x, C.shift(1n+p, y)), 2n) == Nat.mod(x, 2n) : Nat}:
347  Equal.trans(Nat, Nat.mod(Nat.add(x, Nat.double(C.shift(p, y))), 2n), C.bit(Nat.add(x, Nat.double(C.shift(p, y)))), Nat.mod(x, 2n), Equal.sym(Nat, C.bit(Nat.add(x, Nat.double(C.shift(p, y)))), Nat.mod(Nat.add(x, Nat.double(C.shift(p, y))), 2n), bit_mod(Nat.add(x, Nat.double(C.shift(p, y))))), Equal.trans(Nat, C.bit(Nat.add(x, Nat.double(C.shift(p, y)))), C.bit(x), Nat.mod(x, 2n), bit_dbl(x, C.shift(p, y)), bit_mod(x)))