def smb_c
bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64adds.bend:80
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64adds.bend as F64adds
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/f64.bend as SF
import bend-collections-laws-math@1.0.0.0/spec/math/w64.bend as SW
import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
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/lib/u32half.bend as UH
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/w64sh.bend as SH
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as FR
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64rtools.bend as RT
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addp.bend as AP
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64adda.bend as AA
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64nrp.bend as NP
80def smb_c(+one: Nat, +h1: {one == 1n : Nat}, +s: Bool, +e: Nat, +sig: WU.U64, +t: Nat, +S1: Nat, +d: Nat, +x0: Nat, +hsig: {SW.value(sig) == Nat.sub(Nat.double(t), SW.jam(C.high(d, C.shift(10n, S1)), C.low(d, C.shift(10n, S1)))) : Nat}, +he: {Nat.add(Nat.add(x0, d), 2180n) == e : Nat}, +hx63: {Nat.is_le(63n, Nat.add(x0, d)) == True{} : Bool}, +hd1: {Nat.is_le(1n, d) == True{} : Bool}, +hS: {C.fits(63n, C.shift(10n, S1)) == True{} : Bool}, +hT62: {C.fits(62n, Nat.double(t)) == False{} : Bool}, +hT63: {C.fits(63n, Nat.double(t)) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(C.low(d, C.shift(10n, S1)), 0n) == c : Bool}) -> {F.norm_round_pack(s, e, sig) == SF.round(s, Nat.sub(C.shift(d, Nat.double(t)), C.shift(10n, S1)), x0) : F.F64}:
81 match c:
82 case True{}:
83 +el0 = N.eq_from_is_eq(C.low(d, C.shift(10n, S1)), 0n, hc)
84 +hh = hlt(one, h1, s, e, sig, t, S1, d, x0, hsig, he, hx63, hd1, hS, hT62, hT63)
85 +eS = Equal.trans(Nat, C.shift(10n, S1), Nat.add(C.low(d, C.shift(10n, S1)), C.shift(d, C.high(d, C.shift(10n, S1)))), C.shift(d, C.high(d, C.shift(10n, S1))), WW.low_high(d, C.shift(10n, S1)), Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(d, C.high(d, C.shift(10n, S1)))), C.low(d, C.shift(10n, S1)), 0n, el0))
86 +ev = Equal.trans(Nat, SW.value(sig), Nat.sub(Nat.double(t), SW.jam(C.high(d, C.shift(10n, S1)), C.low(d, C.shift(10n, S1)))), Nat.sub(Nat.double(t), C.high(d, C.shift(10n, S1))), hsig, Equal.cong(Nat, Nat, z => Nat.sub(Nat.double(t), z), SW.jam(C.high(d, C.shift(10n, S1)), C.low(d, C.shift(10n, S1))), C.high(d, C.shift(10n, S1)), Equal.trans(Nat, SW.jam(C.high(d, C.shift(10n, S1)), C.low(d, C.shift(10n, S1))), SW.jam(C.high(d, C.shift(10n, S1)), 0n), C.high(d, C.shift(10n, S1)), Equal.cong(Nat, Nat, z => SW.jam(C.high(d, C.shift(10n, S1)), z), C.low(d, C.shift(10n, S1)), 0n, el0), AP.jam_z(C.high(d, C.shift(10n, S1))))))
87 +pos = FR.lt_sub_pos(C.high(d, C.shift(10n, S1)), Nat.double(t), hh)
88 +hz = L.subst(Nat, z => {Nat.is_eq(z, 0n) == False{} : Bool}, Nat.sub(Nat.double(t), C.high(d, C.shift(10n, S1))), SW.value(sig), Equal.sym(Nat, SW.value(sig), Nat.sub(Nat.double(t), C.high(d, C.shift(10n, S1))), ev), posz(Nat.sub(Nat.double(t), C.high(d, C.shift(10n, S1))), pos))
89 +h63 = L.subst(Nat, z => {C.fits(63n, z) == True{} : Bool}, Nat.sub(Nat.double(t), C.high(d, C.shift(10n, S1))), SW.value(sig), Equal.sym(Nat, SW.value(sig), Nat.sub(Nat.double(t), C.high(d, C.shift(10n, S1))), ev), SH.fits_lek(63n, Nat.sub(Nat.double(t), C.high(d, C.shift(10n, S1))), Nat.double(t), UH.sub_le(Nat.double(t), C.high(d, C.shift(10n, S1))), hT63))
90 +r1 = NP.nrp(one, h1, s, e, sig, Nat.add(x0, d), he, hz, h63, hx63)
91 +r2 = Equal.cong(Nat, F.F64, z => SF.round(s, z, Nat.add(x0, d)), SW.value(sig), Nat.sub(Nat.double(t), C.high(d, C.shift(10n, S1))), ev)
92 +r3 = Equal.sym(F.F64, SF.round(s, C.shift(d, Nat.sub(Nat.double(t), C.high(d, C.shift(10n, S1)))), x0), SF.round(s, Nat.sub(Nat.double(t), C.high(d, C.shift(10n, S1))), Nat.add(x0, d)), RT.round_shift(s, d, Nat.sub(Nat.double(t), C.high(d, C.shift(10n, S1))), x0))
93 +r4 = Equal.cong(Nat, F.F64, z => SF.round(s, z, x0), C.shift(d, Nat.sub(Nat.double(t), C.high(d, C.shift(10n, S1)))), Nat.sub(C.shift(d, Nat.double(t)), C.shift(10n, S1)), Equal.trans(Nat, C.shift(d, Nat.sub(Nat.double(t), C.high(d, C.shift(10n, S1)))), Nat.sub(C.shift(d, Nat.double(t)), C.shift(d, C.high(d, C.shift(10n, S1)))), Nat.sub(C.shift(d, Nat.double(t)), C.shift(10n, S1)), Equal.sym(Nat, Nat.sub(C.shift(d, Nat.double(t)), C.shift(d, C.high(d, C.shift(10n, S1)))), C.shift(d, Nat.sub(Nat.double(t), C.high(d, C.shift(10n, S1)))), AP.sub_shift(d, Nat.double(t), C.high(d, C.shift(10n, S1)), N.lt_le(C.high(d, C.shift(10n, S1)), Nat.double(t), hh))), Equal.cong(Nat, Nat, z => Nat.sub(C.shift(d, Nat.double(t)), z), C.shift(d, C.high(d, C.shift(10n, S1))), C.shift(10n, S1), Equal.sym(Nat, C.shift(10n, S1), C.shift(d, C.high(d, C.shift(10n, S1))), eS))))
94 Equal.trans(F.F64, F.norm_round_pack(s, e, sig), SF.round(s, SW.value(sig), Nat.add(x0, d)), SF.round(s, Nat.sub(C.shift(d, Nat.double(t)), C.shift(10n, S1)), x0), r1, Equal.trans(F.F64, SF.round(s, SW.value(sig), Nat.add(x0, d)), SF.round(s, Nat.sub(Nat.double(t), C.high(d, C.shift(10n, S1))), Nat.add(x0, d)), SF.round(s, Nat.sub(C.shift(d, Nat.double(t)), C.shift(10n, S1)), x0), r2, Equal.trans(F.F64, SF.round(s, Nat.sub(Nat.double(t), C.high(d, C.shift(10n, S1))), Nat.add(x0, d)), SF.round(s, C.shift(d, Nat.sub(Nat.double(t), C.high(d, C.shift(10n, S1)))), x0), SF.round(s, Nat.sub(C.shift(d, Nat.double(t)), C.shift(10n, S1)), x0), r3, r4)))
95 case False{}:
96 +hh = hlt(one, h1, s, e, sig, t, S1, d, x0, hsig, he, hx63, hd1, hS, hT62, hT63)
97 +W2 = Nat.sub(C.shift(d, Nat.double(t)), Nat.add(C.low(d, C.shift(10n, S1)), C.shift(d, C.high(d, C.shift(10n, S1)))))
98 +eW = Equal.cong(Nat, Nat, z => Nat.sub(C.shift(d, Nat.double(t)), z), Nat.add(C.low(d, C.shift(10n, S1)), C.shift(d, C.high(d, C.shift(10n, S1)))), C.shift(10n, S1), Equal.sym(Nat, C.shift(10n, S1), Nat.add(C.low(d, C.shift(10n, S1)), C.shift(d, C.high(d, C.shift(10n, S1)))), WW.low_high(d, C.shift(10n, S1))))
99 +ej = AP.jsub(t, d, C.high(d, C.shift(10n, S1)), C.low(d, C.shift(10n, S1)), hc, WW.low_fits(d, C.shift(10n, S1)), hh)
100 +ev = Equal.trans(Nat, SW.value(sig), Nat.sub(Nat.double(t), SW.jam(C.high(d, C.shift(10n, S1)), C.low(d, C.shift(10n, S1)))), SW.jam(C.high(d, Nat.sub(C.shift(d, Nat.double(t)), C.shift(10n, S1))), C.low(d, Nat.sub(C.shift(d, Nat.double(t)), C.shift(10n, S1)))), hsig, Equal.trans(Nat, Nat.sub(Nat.double(t), SW.jam(C.high(d, C.shift(10n, S1)), C.low(d, C.shift(10n, S1)))), SW.jam(C.high(d, W2), C.low(d, W2)), SW.jam(C.high(d, Nat.sub(C.shift(d, Nat.double(t)), C.shift(10n, S1))), C.low(d, Nat.sub(C.shift(d, Nat.double(t)), C.shift(10n, S1)))), ej, Equal.cong(Nat, Nat, z => SW.jam(C.high(d, z), C.low(d, z)), W2, Nat.sub(C.shift(d, Nat.double(t)), C.shift(10n, S1)), eW)))
101 +hd11 = d11_c(d, S1, Nat.is_le(d, 10n), {==}, hc)
102 +nW = wbig(one, h1, t, C.shift(10n, S1), d, N.le_trans(2n, 11n, d, {==}, hd11), hT62, hS)
103 +hb = N.le_trans(Nat.add(d, 55n), 1n+Nat.add(d, 61n), M.bit_length(Nat.sub(C.shift(d, Nat.double(t)), C.shift(10n, S1))), L.subst(Nat, z => {Nat.is_le(Nat.add(d, 55n), z) == True{} : Bool}, Nat.add(d, 62n), 1n+Nat.add(d, 61n), N.add_succ(d, 61n), N.le_add_left(55n, 62n, d, {==})), AA.nfit_bl(Nat.add(d, 61n), Nat.sub(C.shift(d, Nat.double(t)), C.shift(10n, S1)), nW))
104 +JW = SW.jam(C.high(d, Nat.sub(C.shift(d, Nat.double(t)), C.shift(10n, S1))), C.low(d, Nat.sub(C.shift(d, Nat.double(t)), C.shift(10n, S1))))
105 +kh = C.half(C.high(d, C.shift(10n, S1)))
106 +hk = AP.half_lt(kh, t, N.le_lt_trans(Nat.double(kh), C.high(d, C.shift(10n, S1)), Nat.double(t), L.subst(Nat, z => {Nat.is_le(Nat.double(kh), z) == True{} : Bool}, Nat.add(Nat.double(kh), C.bit(C.high(d, C.shift(10n, S1)))), C.high(d, C.shift(10n, S1)), Equal.trans(Nat, Nat.add(Nat.double(kh), C.bit(C.high(d, C.shift(10n, S1)))), Nat.add(C.bit(C.high(d, C.shift(10n, S1))), Nat.double(kh)), C.high(d, C.shift(10n, S1)), NA.add_comm(Nat.double(kh), C.bit(C.high(d, C.shift(10n, S1)))), Equal.sym(Nat, C.high(d, C.shift(10n, S1)), Nat.add(C.bit(C.high(d, C.shift(10n, S1))), Nat.double(kh)), WW.hb(C.high(d, C.shift(10n, S1))))), N.le_add_right(Nat.double(kh), C.bit(C.high(d, C.shift(10n, S1))))), hh))
107 +ev2 = Equal.trans(Nat, SW.value(sig), Nat.sub(Nat.double(t), SW.jam(C.high(d, C.shift(10n, S1)), C.low(d, C.shift(10n, S1)))), Nat.sub(Nat.double(t), 1n+Nat.double(kh)), hsig, Equal.cong(Nat, Nat, z => Nat.sub(Nat.double(t), z), SW.jam(C.high(d, C.shift(10n, S1)), C.low(d, C.shift(10n, S1))), 1n+Nat.double(kh), AP.jam_nz(C.high(d, C.shift(10n, S1)), C.low(d, C.shift(10n, S1)), hc)))
108 +hz = L.subst(Nat, z => {Nat.is_eq(z, 0n) == False{} : Bool}, Nat.sub(Nat.double(t), 1n+Nat.double(kh)), SW.value(sig), Equal.sym(Nat, SW.value(sig), Nat.sub(Nat.double(t), 1n+Nat.double(kh)), ev2), sub_odd(t, kh, hk))
109 +h63 = L.subst(Nat, z => {C.fits(63n, z) == True{} : Bool}, Nat.sub(Nat.double(t), SW.jam(C.high(d, C.shift(10n, S1)), C.low(d, C.shift(10n, S1)))), SW.value(sig), Equal.sym(Nat, SW.value(sig), Nat.sub(Nat.double(t), SW.jam(C.high(d, C.shift(10n, S1)), C.low(d, C.shift(10n, S1)))), hsig), SH.fits_lek(63n, Nat.sub(Nat.double(t), SW.jam(C.high(d, C.shift(10n, S1)), C.low(d, C.shift(10n, S1)))), Nat.double(t), UH.sub_le(Nat.double(t), SW.jam(C.high(d, C.shift(10n, S1)), C.low(d, C.shift(10n, S1)))), hT63))
110 +r1 = NP.nrp(one, h1, s, e, sig, Nat.add(x0, d), he, hz, h63, hx63)
111 +r2 = Equal.cong(Nat, F.F64, z => SF.round(s, z, Nat.add(x0, d)), SW.value(sig), JW, ev)
112 +r3 = Equal.sym(F.F64, SF.round(s, Nat.sub(C.shift(d, Nat.double(t)), C.shift(10n, S1)), x0), SF.round(s, JW, Nat.add(x0, d)), RT.round_jam(s, d, Nat.sub(C.shift(d, Nat.double(t)), C.shift(10n, S1)), x0, hb))
113 Equal.trans(F.F64, F.norm_round_pack(s, e, sig), SF.round(s, SW.value(sig), Nat.add(x0, d)), SF.round(s, Nat.sub(C.shift(d, Nat.double(t)), C.shift(10n, S1)), x0), r1, Equal.trans(F.F64, SF.round(s, SW.value(sig), Nat.add(x0, d)), SF.round(s, JW, Nat.add(x0, d)), SF.round(s, Nat.sub(C.shift(d, Nat.double(t)), C.shift(10n, S1)), x0), r2, r3))