F64adda.sigv: def of bend-collections-laws-math@1.0.0.0 Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64adda.bend as F64adda Lines 96-106 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64adda.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64adda.bend&start_line=96&end_line=106 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 # the aligned sum value: T + jam(S >> d) def 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}: sj = SH.shr_jam_value(sw, d) +J = SW.jam(C.high(d, S), C.low(d, S)) +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)) +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)) +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) +f64 = SH.fits_mono(63n, 64n, Nat.add(T, J), {==}, FR.fits_add1(62n, T, J, hT, fJ)) a1 = WA.add_value(tw, X.shr_jam(sw, d)) +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)) 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))) Uses (25): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool 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=Base/base.bend&name=Nat.is_le https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_comm https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend&name=subst https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=le_add_right https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend&name=fits_add1 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend&name=fits_hc https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64rtools.bend&name=jam_fits https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend&name=add_value https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend&name=fits_mono https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend&name=shr_jam_value https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=low_fit https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=fits https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=high https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=low https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/w64.bend&name=jam https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/w64.bend&name=value https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/u64.bend&name=U64 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/w64.bend&name=add https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/w64.bend&name=shr_jam