def jam_form

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64round.bend:148

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/w64add.bend as WA

148# jam(H, L) is H with bit 0 replaced by t = max(bit H, [L > 0])
149def jam_form(+h: Nat, +l: Nat) -> {SW.jam(h, l) == Nat.add(Nat.max(C.bit(h), Nat.min(l, 1n)), Nat.double(C.half(h))) : Nat}:
150  +t = Nat.max(C.bit(h), Nat.min(l, 1n))
151  +e1 = Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(2n, z), Nat.max(Nat.mod(h, 2n), Nat.min(l, 1n))), Nat.div(h, 2n), C.half(h), Equal.sym(Nat, C.half(h), Nat.div(h, 2n), WA.half_div(h)))
152  +e2 = Equal.cong(Nat, Nat, z => Nat.add(z, Nat.max(Nat.mod(h, 2n), Nat.min(l, 1n))), Nat.mul(2n, C.half(h)), Nat.double(C.half(h)), Equal.sym(Nat, Nat.double(C.half(h)), Nat.mul(2n, C.half(h)), NA.double_mul(C.half(h))))
153  +e3 = Equal.cong(Nat, Nat, z => Nat.add(Nat.double(C.half(h)), Nat.max(z, Nat.min(l, 1n))), Nat.mod(h, 2n), C.bit(h), Equal.sym(Nat, C.bit(h), Nat.mod(h, 2n), WW.bit_mod(h)))
154  +e4 = NA.add_comm(Nat.double(C.half(h)), t)
155  Equal.trans(Nat, SW.jam(h, l), Nat.add(Nat.mul(2n, C.half(h)), Nat.max(Nat.mod(h, 2n), Nat.min(l, 1n))), Nat.add(t, Nat.double(C.half(h))), e1, Equal.trans(Nat, Nat.add(Nat.mul(2n, C.half(h)), Nat.max(Nat.mod(h, 2n), Nat.min(l, 1n))), Nat.add(Nat.double(C.half(h)), Nat.max(Nat.mod(h, 2n), Nat.min(l, 1n))), Nat.add(t, Nat.double(C.half(h))), e2, Equal.trans(Nat, Nat.add(Nat.double(C.half(h)), Nat.max(Nat.mod(h, 2n), Nat.min(l, 1n))), Nat.add(Nat.double(C.half(h)), t), Nat.add(t, Nat.double(C.half(h))), e3, e4)))