def jam_add

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64addp.bend:20

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/spec/math/w64.bend as SW
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as FR

20def jam_add(+t: Nat, +h: Nat, +l: Nat) -> {SW.jam(Nat.add(h, Nat.double(t)), l) == Nat.add(SW.jam(h, l), Nat.double(t)) : Nat}:
21  +mn = Nat.min(l, 1n)
22  +q = Nat.add(h, Nat.double(t))
23  Equal.trans(Nat, SW.jam(q, l), Nat.add(Nat.max(C.bit(q), mn), Nat.double(C.half(q))), Nat.add(SW.jam(h, l), Nat.double(t)), FR.jam_form(q, l), Equal.trans(Nat, Nat.add(Nat.max(C.bit(q), mn), Nat.double(C.half(q))), Nat.add(Nat.max(C.bit(h), mn), Nat.double(C.half(q))), Nat.add(SW.jam(h, l), Nat.double(t)), Equal.cong(Nat, Nat, z => Nat.add(Nat.max(z, mn), Nat.double(C.half(q))), C.bit(q), C.bit(h), WW.bit_dbl(h, t)), Equal.trans(Nat, Nat.add(Nat.max(C.bit(h), mn), Nat.double(C.half(q))), Nat.add(Nat.max(C.bit(h), mn), Nat.double(Nat.add(C.half(h), t))), Nat.add(SW.jam(h, l), Nat.double(t)), Equal.cong(Nat, Nat, z => Nat.add(Nat.max(C.bit(h), mn), Nat.double(z)), C.half(q), Nat.add(C.half(h), t), WW.half_dbl(h, t)), Equal.trans(Nat, Nat.add(Nat.max(C.bit(h), mn), Nat.double(Nat.add(C.half(h), t))), Nat.add(Nat.max(C.bit(h), mn), Nat.add(Nat.double(C.half(h)), Nat.double(t))), Nat.add(SW.jam(h, l), Nat.double(t)), Equal.cong(Nat, Nat, z => Nat.add(Nat.max(C.bit(h), mn), z), Nat.double(Nat.add(C.half(h), t)), Nat.add(Nat.double(C.half(h)), Nat.double(t)), NA.double_add(C.half(h), t)), Equal.trans(Nat, Nat.add(Nat.max(C.bit(h), mn), Nat.add(Nat.double(C.half(h)), Nat.double(t))), Nat.add(Nat.add(Nat.max(C.bit(h), mn), Nat.double(C.half(h))), Nat.double(t)), Nat.add(SW.jam(h, l), Nat.double(t)), Equal.sym(Nat, Nat.add(Nat.add(Nat.max(C.bit(h), mn), Nat.double(C.half(h))), Nat.double(t)), Nat.add(Nat.max(C.bit(h), mn), Nat.add(Nat.double(C.half(h)), Nat.double(t))), NA.add_assoc(Nat.max(C.bit(h), mn), Nat.double(C.half(h)), Nat.double(t))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.double(t)), Nat.add(Nat.max(C.bit(h), mn), Nat.double(C.half(h))), SW.jam(h, l), Equal.sym(Nat, SW.jam(h, l), Nat.add(Nat.max(C.bit(h), mn), Nat.double(C.half(h))), FR.jam_form(h, l))))))))