def sigv

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64adda.bend:96

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/src/math/w64.bend as X
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
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/math/typed/width.bend as WW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend as WA
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

96# the aligned sum value: T + jam(S >> d)
97def sigv(+tw: WU.U64, +sw: WU.U64, +T: Nat, +S: Nat, +d: Nat, +ht: {SW.value(tw) == T : Nat}, +hs: {SW.value(sw) == S : Nat}, +hT: {C.fits(62n, T) == True{} : Bool}, +hS: {C.fits(62n, S) == True{} : Bool}) -> {SW.value(X.add(tw, X.shr_jam(sw, d))) == Nat.add(SW.jam(C.high(d, S), C.low(d, S)), T) : Nat}:
98  sj = SH.shr_jam_value(sw, d)
99  +J = SW.jam(C.high(d, S), C.low(d, S))
100  +ej = Equal.trans(Nat, SW.value(X.shr_jam(sw, d)), SW.jam(C.high(d, SW.value(sw)), C.low(d, SW.value(sw))), J, sj, Equal.cong(Nat, Nat, z => SW.jam(C.high(d, z), C.low(d, z)), SW.value(sw), S, hs))
101  +fh = Equal.trans(Bool, C.fits(62n, C.high(d, S)), C.fits(Nat.add(d, 62n), S), True{}, Equal.sym(Bool, C.fits(Nat.add(d, 62n), S), C.fits(62n, C.high(d, S)), FR.fits_hc(d, 62n, S)), SH.fits_mono(62n, Nat.add(d, 62n), S, L.subst(Nat, z => {Nat.is_le(62n, z) == True{} : Bool}, Nat.add(62n, d), Nat.add(d, 62n), NA.add_comm(62n, d), N.le_add_right(62n, d)), hS))
102  +fJ = Equal.trans(Bool, C.fits(62n, J), C.fits(62n, C.high(d, S)), True{}, RT.jam_fits(61n, C.high(d, S), C.low(d, S)), fh)
103  +f64 = SH.fits_mono(63n, 64n, Nat.add(T, J), {==}, FR.fits_add1(62n, T, J, hT, fJ))
104  a1 = WA.add_value(tw, X.shr_jam(sw, d))
105  +e1 = Equal.trans(Nat, Nat.add(SW.value(tw), SW.value(X.shr_jam(sw, d))), Nat.add(T, SW.value(X.shr_jam(sw, d))), Nat.add(T, J), Equal.cong(Nat, Nat, z => Nat.add(z, SW.value(X.shr_jam(sw, d))), SW.value(tw), T, ht), Equal.cong(Nat, Nat, z => Nat.add(T, z), SW.value(X.shr_jam(sw, d)), J, ej))
106  Equal.trans(Nat, SW.value(X.add(tw, X.shr_jam(sw, d))), C.low(64n, Nat.add(SW.value(tw), SW.value(X.shr_jam(sw, d)))), Nat.add(J, T), a1, Equal.trans(Nat, C.low(64n, Nat.add(SW.value(tw), SW.value(X.shr_jam(sw, d)))), Nat.add(T, J), Nat.add(J, T), Equal.trans(Nat, C.low(64n, Nat.add(SW.value(tw), SW.value(X.shr_jam(sw, d)))), C.low(64n, Nat.add(T, J)), Nat.add(T, J), Equal.cong(Nat, Nat, z => C.low(64n, z), Nat.add(SW.value(tw), SW.value(X.shr_jam(sw, d))), Nat.add(T, J), e1), WW.low_fit(64n, Nat.add(T, J), f64)), NA.add_comm(T, J)))