def fold

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/f64bits.bend:347

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/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WW

347# f + 2^20 E + 2^31 t is f + 2^20 (E + 2^11 t)
348def fold(+f: Nat, +E: Nat, +t: Nat) -> {Nat.add(Nat.add(f, C.shift(20n, E)), C.shift(31n, t)) == Nat.add(f, C.shift(20n, Nat.add(E, C.shift(11n, t)))) : Nat}:
349  +e1 = NA.add_assoc(f, C.shift(20n, E), C.shift(31n, t))
350  +e2 = Equal.cong(Nat, Nat, z => Nat.add(f, Nat.add(C.shift(20n, E), z)), C.shift(31n, t), C.shift(20n, C.shift(11n, t)), WW.shift_comp(20n, 11n, t))
351  +e3 = Equal.cong(Nat, Nat, z => Nat.add(f, z), Nat.add(C.shift(20n, E), C.shift(20n, C.shift(11n, t))), C.shift(20n, Nat.add(E, C.shift(11n, t))), Equal.sym(Nat, C.shift(20n, Nat.add(E, C.shift(11n, t))), Nat.add(C.shift(20n, E), C.shift(20n, C.shift(11n, t))), WW.shift_add(20n, E, C.shift(11n, t))))
352  Equal.trans(Nat, Nat.add(Nat.add(f, C.shift(20n, E)), C.shift(31n, t)), Nat.add(f, Nat.add(C.shift(20n, E), C.shift(31n, t))), Nat.add(f, C.shift(20n, Nat.add(E, C.shift(11n, t)))), e1, Equal.trans(Nat, Nat.add(f, Nat.add(C.shift(20n, E), C.shift(31n, t))), Nat.add(f, Nat.add(C.shift(20n, E), C.shift(20n, C.shift(11n, t)))), Nat.add(f, C.shift(20n, Nat.add(E, C.shift(11n, t)))), e2, e3))