def seq

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64addf.bend:173

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/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/w64add.bend as WA
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natcmp.bend as NC
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/f64adde.bend as AE
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addg.bend as AG

173def seq(+one: Nat, +h1: {one == 1n : Nat}, +x: F.F64, +y: F.F64, +sa: Bool, +sb: Bool, +hsg: {Bool.not(Bool.xor(sa, sb)) == False{} : Bool}, +ea: Nat, +Fa: Nat, +Fb: Nat, +hfa: {SW.value(F.frac(x)) == Fa : Nat}, +hfb: {SW.value(F.frac(y)) == Fb : Nat}, +hFa: {C.fits(52n, Fa) == True{} : Bool}, +hFb: {C.fits(52n, Fb) == True{} : Bool}, +hlta: {Nat.is_lt(ea, 2047n) == True{} : Bool}, +d: Cmp, +hd: {Nat.cmp(Fa, Fb) == d : Cmp}) -> {F.sm_eq2(sa, ea, F.frac(x), F.frac(y), d) == SF.sub_mag(sa, AG.mt(ea, Fa), sb, AG.mt(ea, Fb), AG.xe(ea), d) : F.F64}:
174  match d:
175    case EQ{}:
176      AG.zero_v(False{})
177    case GT{}:
178      +hlt = NC.lt_of_gt(Fa, Fb, hd)
179      +hle = L.subst(Nat, w => {Nat.is_le(w, SW.value(F.frac(x))) == True{} : Bool}, Fb, SW.value(F.frac(y)), Equal.sym(Nat, SW.value(F.frac(y)), Fb, hfb), L.subst(Nat, w => {Nat.is_le(Fb, w) == True{} : Bool}, Fa, SW.value(F.frac(x)), Equal.sym(Nat, SW.value(F.frac(x)), Fa, hfa), N.lt_le(Fb, Fa, hlt)))
180      +hdv = Equal.trans(Nat, SW.value(X.sub(F.frac(x), F.frac(y))), Nat.sub(SW.value(F.frac(x)), SW.value(F.frac(y))), Nat.sub(Fa, Fb), WA.sub_value(F.frac(x), F.frac(y), hle), Equal.trans(Nat, Nat.sub(SW.value(F.frac(x)), SW.value(F.frac(y))), Nat.sub(Fa, SW.value(F.frac(y))), Nat.sub(Fa, Fb), Equal.cong(Nat, Nat, w => Nat.sub(w, SW.value(F.frac(y))), SW.value(F.frac(x)), Fa, hfa), Equal.cong(Nat, Nat, w => Nat.sub(Fa, w), SW.value(F.frac(y)), Fb, hfb)))
181      +hD = Equal.trans(Bool, C.fits(52n, Nat.sub(Fa, Fb)), Nat.is_lt(Nat.sub(Fa, Fb), C.shift(52n, one)), True{}, Equal.sym(Bool, Nat.is_lt(Nat.sub(Fa, Fb), C.shift(52n, one)), C.fits(52n, Nat.sub(Fa, Fb)), FR.lt_fit(52n, one, h1, Nat.sub(Fa, Fb))), N.le_lt_trans(Nat.sub(Fa, Fb), Fa, C.shift(52n, one), AG.sub_le(Fa, Fb), Equal.trans(Bool, Nat.is_lt(Fa, C.shift(52n, one)), C.fits(52n, Fa), True{}, FR.lt_fit(52n, one, h1, Fa), hFa)))
182      +hz = AG.posz(Nat.sub(Fa, Fb), FR.lt_sub_pos(Fb, Fa, hlt))
183      +r = AE.smx(one, h1, sa, Nat.sub(ea, 1n), X.sub(F.frac(x), F.frac(y)), Nat.sub(Fa, Fb), hdv, hD, hz, hovm(ea, hlta))
184      +b = rc2(sa, sa, {==}, Nat.sub(Fa, Fb), Nat.sub(AG.mt(ea, Fa), AG.mt(ea, Fb)), Equal.sym(Nat, Nat.sub(AG.mt(ea, Fa), AG.mt(ea, Fb)), Nat.sub(Fa, Fb), FR.sub_cancel_r(Fa, Fb, C.shift(52n, SF.b2n(Bool.not(Nat.is_eq(ea, 0n)))))), Nat.add(1926n, Nat.sub(ea, 1n)), AG.xe(ea), xem(ea))
185      Equal.trans(F.F64, F.sm_exact(sa, Nat.sub(ea, 1n), X.sub(F.frac(x), F.frac(y))), SF.round(sa, Nat.sub(Fa, Fb), Nat.add(1926n, Nat.sub(ea, 1n))), SF.round(sa, Nat.sub(AG.mt(ea, Fa), AG.mt(ea, Fb)), AG.xe(ea)), r, b)
186    case LT{}:
187      +hlt = NC.lt_of_cmp(Fa, Fb, hd)
188      +hle = L.subst(Nat, w => {Nat.is_le(w, SW.value(F.frac(y))) == True{} : Bool}, Fa, SW.value(F.frac(x)), Equal.sym(Nat, SW.value(F.frac(x)), Fa, hfa), L.subst(Nat, w => {Nat.is_le(Fa, w) == True{} : Bool}, Fb, SW.value(F.frac(y)), Equal.sym(Nat, SW.value(F.frac(y)), Fb, hfb), N.lt_le(Fa, Fb, hlt)))
189      +hdv = Equal.trans(Nat, SW.value(X.sub(F.frac(y), F.frac(x))), Nat.sub(SW.value(F.frac(y)), SW.value(F.frac(x))), Nat.sub(Fb, Fa), WA.sub_value(F.frac(y), F.frac(x), hle), Equal.trans(Nat, Nat.sub(SW.value(F.frac(y)), SW.value(F.frac(x))), Nat.sub(Fb, SW.value(F.frac(x))), Nat.sub(Fb, Fa), Equal.cong(Nat, Nat, w => Nat.sub(w, SW.value(F.frac(x))), SW.value(F.frac(y)), Fb, hfb), Equal.cong(Nat, Nat, w => Nat.sub(Fb, w), SW.value(F.frac(x)), Fa, hfa)))
190      +hD = Equal.trans(Bool, C.fits(52n, Nat.sub(Fb, Fa)), Nat.is_lt(Nat.sub(Fb, Fa), C.shift(52n, one)), True{}, Equal.sym(Bool, Nat.is_lt(Nat.sub(Fb, Fa), C.shift(52n, one)), C.fits(52n, Nat.sub(Fb, Fa)), FR.lt_fit(52n, one, h1, Nat.sub(Fb, Fa))), N.le_lt_trans(Nat.sub(Fb, Fa), Fb, C.shift(52n, one), AG.sub_le(Fb, Fa), Equal.trans(Bool, Nat.is_lt(Fb, C.shift(52n, one)), C.fits(52n, Fb), True{}, FR.lt_fit(52n, one, h1, Fb), hFb)))
191      +hz = AG.posz(Nat.sub(Fb, Fa), FR.lt_sub_pos(Fa, Fb, hlt))
192      +r = AE.smx(one, h1, Bool.not(sa), Nat.sub(ea, 1n), X.sub(F.frac(y), F.frac(x)), Nat.sub(Fb, Fa), hdv, hD, hz, hovm(ea, hlta))
193      +b = rc2(Bool.not(sa), sb, AG.sgn(sa, sb, hsg), Nat.sub(Fb, Fa), Nat.sub(AG.mt(ea, Fb), AG.mt(ea, Fa)), Equal.sym(Nat, Nat.sub(AG.mt(ea, Fb), AG.mt(ea, Fa)), Nat.sub(Fb, Fa), FR.sub_cancel_r(Fb, Fa, C.shift(52n, SF.b2n(Bool.not(Nat.is_eq(ea, 0n)))))), Nat.add(1926n, Nat.sub(ea, 1n)), AG.xe(ea), xem(ea))
194      Equal.trans(F.F64, F.sm_exact(Bool.not(sa), Nat.sub(ea, 1n), X.sub(F.frac(y), F.frac(x))), SF.round(Bool.not(sa), Nat.sub(Fb, Fa), Nat.add(1926n, Nat.sub(ea, 1n))), SF.round(sb, Nat.sub(AG.mt(ea, Fb), AG.mt(ea, Fa)), AG.xe(ea)), r, b)