def rp_sub

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

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/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/math/typed/w64sh.bend as SH

841def rp_sub(+one: Nat, +h1: {one == 1n : Nat}, +s: Bool, +e: Nat, +sig: WU.U64, +x: Nat, +hx: {Nat.add(x, 2180n) == e : Nat}, +h62: {C.fits(62n, SW.value(sig)) == False{} : Bool}, +h63: {C.fits(63n, SW.value(sig)) == True{} : Bool}, +hb: {Nat.is_lt(x, 1916n) == True{} : Bool}, +u: Nat, +hu: {Nat.max(Nat.add(10n, x), 1926n) == u : Nat}) -> {F.rp_neg(s, e, sig, True{}) == SF.round_u(s, SW.value(sig), x, u) : F.F64}:
842  +hu1 = Equal.trans(Nat, u, Nat.max(Nat.add(10n, x), 1926n), 1926n, Equal.sym(Nat, Nat.max(Nat.add(10n, x), 1926n), u, hu), max_r(Nat.add(10n, x), 1926n, hb))
843  +d = Nat.sub(F.off(), e)
844  +ed = Equal.trans(Nat, d, Nat.sub(F.off(), Nat.add(x, 2180n)), Nat.sub(1916n, x), Equal.cong(Nat, Nat, z => Nat.sub(F.off(), z), e, Nat.add(x, 2180n), Equal.sym(Nat, Nat.add(x, 2180n), e, hx)), sub_cancel_r(1916n, x, 2180n))
845  +hd1 = L.subst(Nat, z => {Nat.is_le(1n, z) == True{} : Bool}, Nat.sub(1916n, x), d, Equal.sym(Nat, d, Nat.sub(1916n, x), ed), lt_sub_pos(x, 1916n, hb))
846  +ku = Equal.trans(Nat, Nat.sub(u, x), Nat.sub(1926n, x), Nat.add(10n, d), Equal.cong(Nat, Nat, z => Nat.sub(z, x), u, 1926n, hu1), Equal.trans(Nat, Nat.sub(1926n, x), Nat.add(10n, Nat.sub(1916n, x)), Nat.add(10n, d), sub_add_a(10n, 1916n, x, N.lt_le(x, 1916n, hb)), Equal.cong(Nat, Nat, z => Nat.add(10n, z), Nat.sub(1916n, x), d, Equal.sym(Nat, d, Nat.sub(1916n, x), ed))))
847  +hle = L.subst(Nat, z => {Nat.is_le(x, z) == True{} : Bool}, 1926n, u, Equal.sym(Nat, u, 1926n, hu1), N.le_trans(x, 1916n, 1926n, N.lt_le(x, 1916n, hb), {==}))
848  sj = SH.shr_jam_value(sig, d)
849  sj2 = SH.shr_jam_value(sig, d)
850  +est = sticky(8n, d, SW.value(sig))
851  +eq = Equal.trans(Nat, SF.rne(SW.value(sig), Nat.add(10n, d)), SF.rne(SW.jam(C.high(d, SW.value(sig)), C.low(d, SW.value(sig))), 10n), SF.rne(SW.value(X.shr_jam(sig, d)), 10n), est, Equal.cong(Nat, Nat, z => SF.rne(z, 10n), SW.jam(C.high(d, SW.value(sig)), C.low(d, SW.value(sig))), SW.value(X.shr_jam(sig, d)), Equal.sym(Nat, SW.value(X.shr_jam(sig, d)), SW.jam(C.high(d, SW.value(sig)), C.low(d, SW.value(sig))), sj)))
852  +hJ = L.subst(Nat, z => {C.fits(63n, z) == True{} : Bool}, SW.jam(C.high(d, SW.value(sig)), C.low(d, SW.value(sig))), SW.value(X.shr_jam(sig, d)), Equal.sym(Nat, SW.value(X.shr_jam(sig, d)), SW.jam(C.high(d, SW.value(sig)), C.low(d, SW.value(sig))), sj2), jfit(d, SW.value(sig), hd1, h63))
853  +hqJ = rne_top(one, h1, SW.value(X.shr_jam(sig, d)), hJ)
854  +hq = L.subst(Nat, z => {Nat.is_le(z, C.shift(53n, one)) == True{} : Bool}, SF.rne(SW.value(X.shr_jam(sig, d)), 10n), SF.rne(SW.value(sig), Nat.add(10n, d)), Equal.sym(Nat, SF.rne(SW.value(sig), Nat.add(10n, d)), SF.rne(SW.value(X.shr_jam(sig, d)), 10n), eq), hqJ)
855  +h0 = or_t(Bool.not(C.fits(52n, SF.rne(SW.value(sig), Nat.add(10n, d)))))
856  +hov = pick_lt(C.fits(53n, SF.rne(SW.value(sig), Nat.add(10n, d))))
857  +s1 = Equal.cong(Bool, F.F64, t => SF.pack(s, SF.pick(Nat, t, SF.rne(SW.value(sig), Nat.sub(u, x)), C.shift(Nat.sub(x, u), SW.value(sig))), u), Nat.is_le(x, u), True{}, hle)
858  +s2 = Equal.cong(Nat, F.F64, z => SF.pack(s, SF.rne(SW.value(sig), z), u), Nat.sub(u, x), Nat.add(10n, d), ku)
859  +s3 = pkg(one, h1, s, SF.rne(SW.value(sig), Nat.add(10n, d)), u, 0n, Equal.sym(Nat, u, 1926n, hu1), hq, h0, hov)
860  +sp = Equal.trans(F.F64, SF.round_u(s, SW.value(sig), x, u), SF.pack(s, SF.rne(SW.value(sig), Nat.sub(u, x)), u), bits(s, Nat.add(SF.rne(SW.value(sig), Nat.add(10n, d)), C.shift(52n, 0n))), s1, Equal.trans(F.F64, SF.pack(s, SF.rne(SW.value(sig), Nat.sub(u, x)), u), SF.pack(s, SF.rne(SW.value(sig), Nat.add(10n, d)), u), bits(s, Nat.add(SF.rne(SW.value(sig), Nat.add(10n, d)), C.shift(52n, 0n))), s2, s3))
861  +f54 = SH.fits_mono(54n, 63n, SF.rne(SW.value(X.shr_jam(sig, d)), 10n), {==}, fit54(one, h1, SF.rne(SW.value(X.shr_jam(sig, d)), 10n), hqJ))
862  +hq0 = L.subst(Nat, z => {C.fits(63n, z) == True{} : Bool}, SF.rne(SW.value(X.shr_jam(sig, d)), 10n), Nat.add(SF.rne(SW.value(X.shr_jam(sig, d)), 10n), 0n), Equal.sym(Nat, Nat.add(SF.rne(SW.value(X.shr_jam(sig, d)), 10n), 0n), SF.rne(SW.value(X.shr_jam(sig, d)), 10n), N.add_zero(SF.rne(SW.value(X.shr_jam(sig, d)), 10n))), f54)
863  +i1 = rpf0(s, X.shr_jam(sig, d), hJ, hq0)
864  +i2 = Equal.cong(Nat, F.F64, z => bits(s, Nat.add(z, C.shift(52n, 0n))), SF.rne(SW.value(X.shr_jam(sig, d)), 10n), SF.rne(SW.value(sig), Nat.add(10n, d)), Equal.sym(Nat, SF.rne(SW.value(sig), Nat.add(10n, d)), SF.rne(SW.value(X.shr_jam(sig, d)), 10n), eq))
865  Equal.trans(F.F64, F.rp_fin(s, 0n, X.shr_jam(sig, d)), bits(s, Nat.add(SF.rne(SW.value(sig), Nat.add(10n, d)), C.shift(52n, 0n))), SF.round_u(s, SW.value(sig), x, u), Equal.trans(F.F64, F.rp_fin(s, 0n, X.shr_jam(sig, d)), bits(s, Nat.add(SF.rne(SW.value(X.shr_jam(sig, d)), 10n), C.shift(52n, 0n))), bits(s, Nat.add(SF.rne(SW.value(sig), Nat.add(10n, d)), C.shift(52n, 0n))), i1, i2), Equal.sym(F.F64, SF.round_u(s, SW.value(sig), x, u), bits(s, Nat.add(SF.rne(SW.value(sig), Nat.add(10n, d)), C.shift(52n, 0n))), sp))