F64bits.fold: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/f64bits.bend as F64bits
Lines 347-352 of bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/f64bits.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/f64bits.bend&start_line=347&end_line=352

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

# f + 2^20 E + 2^31 t is f + 2^20 (E + 2^11 t)
def 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}:
  +e1 = NA.add_assoc(f, C.shift(20n, E), C.shift(31n, t))
  +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))
  +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))))
  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))

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_assoc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend&name=shift_add
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend&name=shift_comp
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=shift