def caseEQ

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

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/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/f64addc.bend as AC
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addg.bend as AG

196def caseEQ(+one: Nat, +h1: {one == 1n : Nat}, +x: F.F64, +y: F.F64, +sa: Bool, +sb: 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}, +sg: Bool, +hsg: {Bool.not(Bool.xor(sa, sb)) == sg : Bool}) -> {SF.pick(F.F64, sg, F.am_case(x, y, sa, ea, ea, EQ{}), F.sm_case(x, y, sa, ea, ea, EQ{})) == SF.add_mag(sa, AG.mt(ea, Fa), sb, AG.mt(ea, Fb), AG.xe(ea)) : F.F64}:
197  match sg:
198    case True{}:
199      +ha = N.is_eq_lt(ea, 2047n, hlta)
200      +i1 = aeq_c(one, h1, x, y, sa, ea, Fa, Fb, hfa, hfb, hFa, hFb, ha, Nat.is_eq(ea, 0n), {==})
201      +sp = Equal.cong(Bool, F.F64, t => SF.pick(F.F64, t, SF.round(sa, Nat.add(AG.mt(ea, Fa), AG.mt(ea, Fb)), AG.xe(ea)), SF.sub_mag(sa, AG.mt(ea, Fa), sb, AG.mt(ea, Fb), AG.xe(ea), Nat.cmp(AG.mt(ea, Fa), AG.mt(ea, Fb)))), Bool.not(Bool.xor(sa, sb)), True{}, hsg)
202      Equal.trans(F.F64, SF.pick(F.F64, True{}, F.am_case(x, y, sa, ea, ea, EQ{}), F.sm_case(x, y, sa, ea, ea, EQ{})), F.am_case(x, y, sa, ea, ea, EQ{}), SF.add_mag(sa, AG.mt(ea, Fa), sb, AG.mt(ea, Fb), AG.xe(ea)), FR.pk_t(F.F64, F.am_case(x, y, sa, ea, ea, EQ{}), F.sm_case(x, y, sa, ea, ea, EQ{})), Equal.trans(F.F64, F.am_case(x, y, sa, ea, ea, EQ{}), SF.round(sa, Nat.add(AG.mt(ea, Fa), AG.mt(ea, Fb)), AG.xe(ea)), SF.add_mag(sa, AG.mt(ea, Fa), sb, AG.mt(ea, Fb), AG.xe(ea)), i1, Equal.sym(F.F64, SF.add_mag(sa, AG.mt(ea, Fa), sb, AG.mt(ea, Fb), AG.xe(ea)), SF.round(sa, Nat.add(AG.mt(ea, Fa), AG.mt(ea, Fb)), AG.xe(ea)), sp)))
203    case False{}:
204      +ha = N.is_eq_lt(ea, 2047n, hlta)
205      +i1 = Equal.cong(Bool, F.F64, t => F.sm_eq(sa, ea, F.frac(x), F.frac(y), t), Nat.is_eq(ea, 2047n), False{}, ha)
206      +ec = Equal.trans(Cmp, X.cmp(F.frac(x), F.frac(y)), Nat.cmp(SW.value(F.frac(x)), SW.value(F.frac(y))), Nat.cmp(Fa, Fb), AC.cmpv(F.frac(x), F.frac(y)), Equal.trans(Cmp, Nat.cmp(SW.value(F.frac(x)), SW.value(F.frac(y))), Nat.cmp(Fa, SW.value(F.frac(y))), Nat.cmp(Fa, Fb), Equal.cong(Nat, Cmp, w => Nat.cmp(w, SW.value(F.frac(y))), SW.value(F.frac(x)), Fa, hfa), Equal.cong(Nat, Cmp, w => Nat.cmp(Fa, w), SW.value(F.frac(y)), Fb, hfb)))
207      +i2 = Equal.cong(Cmp, F.F64, t => F.sm_eq2(sa, ea, F.frac(x), F.frac(y), t), X.cmp(F.frac(x), F.frac(y)), Nat.cmp(Fa, Fb), ec)
208      +i3 = seq(one, h1, x, y, sa, sb, hsg, ea, Fa, Fb, hfa, hfb, hFa, hFb, hlta, Nat.cmp(Fa, Fb), {==})
209      +sp1 = Equal.cong(Bool, F.F64, t => SF.pick(F.F64, t, SF.round(sa, Nat.add(AG.mt(ea, Fa), AG.mt(ea, Fb)), AG.xe(ea)), SF.sub_mag(sa, AG.mt(ea, Fa), sb, AG.mt(ea, Fb), AG.xe(ea), Nat.cmp(AG.mt(ea, Fa), AG.mt(ea, Fb)))), Bool.not(Bool.xor(sa, sb)), False{}, hsg)
210      +sp2 = Equal.cong(Cmp, F.F64, t => SF.sub_mag(sa, AG.mt(ea, Fa), sb, AG.mt(ea, Fb), AG.xe(ea), t), Nat.cmp(AG.mt(ea, Fa), AG.mt(ea, Fb)), Nat.cmp(Fa, Fb), NC.cmp_addr(Fa, Fb, C.shift(52n, SF.b2n(Bool.not(Nat.is_eq(ea, 0n))))))
211      +imp = Equal.trans(F.F64, F.sm_case(x, y, sa, ea, ea, EQ{}), F.sm_eq2(sa, ea, F.frac(x), F.frac(y), X.cmp(F.frac(x), F.frac(y))), SF.sub_mag(sa, AG.mt(ea, Fa), sb, AG.mt(ea, Fb), AG.xe(ea), Nat.cmp(Fa, Fb)), i1, Equal.trans(F.F64, F.sm_eq2(sa, ea, F.frac(x), F.frac(y), X.cmp(F.frac(x), F.frac(y))), F.sm_eq2(sa, ea, F.frac(x), F.frac(y), Nat.cmp(Fa, Fb)), SF.sub_mag(sa, AG.mt(ea, Fa), sb, AG.mt(ea, Fb), AG.xe(ea), Nat.cmp(Fa, Fb)), i2, i3))
212      +spc = Equal.trans(F.F64, SF.add_mag(sa, AG.mt(ea, Fa), sb, AG.mt(ea, Fb), AG.xe(ea)), SF.sub_mag(sa, AG.mt(ea, Fa), sb, AG.mt(ea, Fb), AG.xe(ea), Nat.cmp(AG.mt(ea, Fa), AG.mt(ea, Fb))), SF.sub_mag(sa, AG.mt(ea, Fa), sb, AG.mt(ea, Fb), AG.xe(ea), Nat.cmp(Fa, Fb)), sp1, sp2)
213      Equal.trans(F.F64, SF.pick(F.F64, False{}, F.am_case(x, y, sa, ea, ea, EQ{}), F.sm_case(x, y, sa, ea, ea, EQ{})), F.sm_case(x, y, sa, ea, ea, EQ{}), SF.add_mag(sa, AG.mt(ea, Fa), sb, AG.mt(ea, Fb), AG.xe(ea)), FR.pk_f(F.F64, F.am_case(x, y, sa, ea, ea, EQ{}), F.sm_case(x, y, sa, ea, ea, EQ{})), Equal.trans(F.F64, F.sm_case(x, y, sa, ea, ea, EQ{}), SF.sub_mag(sa, AG.mt(ea, Fa), sb, AG.mt(ea, Fb), AG.xe(ea), Nat.cmp(Fa, Fb)), SF.add_mag(sa, AG.mt(ea, Fa), sb, AG.mt(ea, Fb), AG.xe(ea)), imp, Equal.sym(F.F64, SF.add_mag(sa, AG.mt(ea, Fa), sb, AG.mt(ea, Fb), AG.xe(ea)), SF.sub_mag(sa, AG.mt(ea, Fa), sb, AG.mt(ea, Fb), AG.xe(ea), Nat.cmp(Fa, Fb)), spc)))