def caseLT

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

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/math/typed/f64round.bend as FR
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addg.bend as AG
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addh.bend as AH

115def caseLT(+one: Nat, +h1: {one == 1n : Nat}, +x: F.F64, +y: F.F64, +sa: Bool, +sb: Bool, +ea: Nat, +eb: 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}, +hb: {Nat.is_eq(eb, 2047n) == False{} : Bool}, +hlt: {Nat.is_lt(ea, eb) == True{} : Bool}, +sg: Bool, +hsg: {Bool.not(Bool.xor(sa, sb)) == sg : Bool}) -> {SF.pick(F.F64, sg, F.am_case(x, y, sa, ea, eb, LT{}), F.sm_case(x, y, sa, ea, eb, LT{})) == SF.add_mag(sa, AG.mt(ea, Fa), sb, C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb)), AG.xe(ea)) : F.F64}:
116  match sg:
117    case True{}:
118      +i1 = Equal.cong(Bool, F.F64, t => F.am_big(y, sa, eb, F.frac(y), ea, F.frac(x), t), Nat.is_eq(eb, 2047n), False{}, hb)
119      +i2 = AH.bigA(one, h1, sa, eb, F.frac(y), ea, F.frac(x), Fb, Fa, hfb, hfa, hFb, hFa, hlt)
120      +sp = Equal.cong(Bool, F.F64, t => SF.pick(F.F64, t, SF.round(sa, Nat.add(AG.mt(ea, Fa), C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb))), AG.xe(ea)), SF.sub_mag(sa, AG.mt(ea, Fa), sb, C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb)), AG.xe(ea), Nat.cmp(AG.mt(ea, Fa), C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb))))), Bool.not(Bool.xor(sa, sb)), True{}, hsg)
121      Equal.trans(F.F64, SF.pick(F.F64, True{}, F.am_case(x, y, sa, ea, eb, LT{}), F.sm_case(x, y, sa, ea, eb, LT{})), F.am_case(x, y, sa, ea, eb, LT{}), SF.add_mag(sa, AG.mt(ea, Fa), sb, C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb)), AG.xe(ea)), FR.pk_t(F.F64, F.am_case(x, y, sa, ea, eb, LT{}), F.sm_case(x, y, sa, ea, eb, LT{})), Equal.trans(F.F64, F.am_case(x, y, sa, ea, eb, LT{}), SF.round(sa, Nat.add(AG.mt(ea, Fa), C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb))), AG.xe(ea)), SF.add_mag(sa, AG.mt(ea, Fa), sb, C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb)), AG.xe(ea)), Equal.trans(F.F64, F.am_case(x, y, sa, ea, eb, LT{}), F.rp62(sa, Nat.add(F.off(), eb), X.add(X.add(WU.U64{0, 536870912}, X.shl(F.frac(y), 9n)), X.shr_jam(F.am_small(ea, X.shl(F.frac(x), 9n)), Nat.sub(eb, ea)))), SF.round(sa, Nat.add(AG.mt(ea, Fa), C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb))), AG.xe(ea)), i1, i2), Equal.sym(F.F64, SF.add_mag(sa, AG.mt(ea, Fa), sb, C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb)), AG.xe(ea)), SF.round(sa, Nat.add(AG.mt(ea, Fa), C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb))), AG.xe(ea)), sp)))
122    case False{}:
123      +i1 = Equal.cong(Bool, F.F64, t => F.sm_big(y, Bool.not(sa), eb, F.frac(y), ea, F.frac(x), t), Nat.is_eq(eb, 2047n), False{}, hb)
124      +i2 = AH.bigS(one, h1, Bool.not(sa), eb, F.frac(y), ea, F.frac(x), Fb, Fa, hfb, hfa, hFb, hFa, hlt)
125      +i3 = Equal.cong(Bool, F.F64, t => SF.round(t, Nat.sub(C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb)), AG.mt(ea, Fa)), AG.xe(ea)), Bool.not(sa), sb, AG.sgn(sa, sb, hsg))
126      +sp1 = Equal.cong(Bool, F.F64, t => SF.pick(F.F64, t, SF.round(sa, Nat.add(AG.mt(ea, Fa), C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb))), AG.xe(ea)), SF.sub_mag(sa, AG.mt(ea, Fa), sb, C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb)), AG.xe(ea), Nat.cmp(AG.mt(ea, Fa), C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb))))), Bool.not(Bool.xor(sa, sb)), False{}, hsg)
127      +sp2 = Equal.cong(Cmp, F.F64, t => SF.sub_mag(sa, AG.mt(ea, Fa), sb, C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb)), AG.xe(ea), t), Nat.cmp(AG.mt(ea, Fa), C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb))), LT{}, AG.bigcmp(one, h1, eb, ea, Fb, Fa, hFb, hFa, hlt))
128      +imp = Equal.trans(F.F64, F.sm_case(x, y, sa, ea, eb, LT{}), F.norm_round_pack(Bool.not(sa), Nat.add(F.off(), Nat.sub(eb, 1n)), X.sub(X.add(X.shl(F.frac(y), 10n), WU.U64{0, 1073741824}), X.shr_jam(F.sm_small(ea, X.shl(F.frac(x), 10n)), Nat.sub(eb, ea)))), SF.round(sb, Nat.sub(C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb)), AG.mt(ea, Fa)), AG.xe(ea)), i1, Equal.trans(F.F64, F.norm_round_pack(Bool.not(sa), Nat.add(F.off(), Nat.sub(eb, 1n)), X.sub(X.add(X.shl(F.frac(y), 10n), WU.U64{0, 1073741824}), X.shr_jam(F.sm_small(ea, X.shl(F.frac(x), 10n)), Nat.sub(eb, ea)))), SF.round(Bool.not(sa), Nat.sub(C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb)), AG.mt(ea, Fa)), AG.xe(ea)), SF.round(sb, Nat.sub(C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb)), AG.mt(ea, Fa)), AG.xe(ea)), i2, i3))
129      +spc = Equal.trans(F.F64, SF.add_mag(sa, AG.mt(ea, Fa), sb, C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb)), AG.xe(ea)), SF.sub_mag(sa, AG.mt(ea, Fa), sb, C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb)), AG.xe(ea), Nat.cmp(AG.mt(ea, Fa), C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb)))), SF.round(sb, Nat.sub(C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb)), AG.mt(ea, Fa)), AG.xe(ea)), sp1, sp2)
130      Equal.trans(F.F64, SF.pick(F.F64, False{}, F.am_case(x, y, sa, ea, eb, LT{}), F.sm_case(x, y, sa, ea, eb, LT{})), F.sm_case(x, y, sa, ea, eb, LT{}), SF.add_mag(sa, AG.mt(ea, Fa), sb, C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb)), AG.xe(ea)), FR.pk_f(F.F64, F.am_case(x, y, sa, ea, eb, LT{}), F.sm_case(x, y, sa, ea, eb, LT{})), Equal.trans(F.F64, F.sm_case(x, y, sa, ea, eb, LT{}), SF.round(sb, Nat.sub(C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb)), AG.mt(ea, Fa)), AG.xe(ea)), SF.add_mag(sa, AG.mt(ea, Fa), sb, C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb)), AG.xe(ea)), imp, Equal.sym(F.F64, SF.add_mag(sa, AG.mt(ea, Fa), sb, C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb)), AG.xe(ea)), SF.round(sb, Nat.sub(C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb)), AG.mt(ea, Fa)), AG.xe(ea)), spc)))