F64addf.caseGT: def of bend-collections-laws-math@1.0.0.0 Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addf.bend as F64addf Lines 132-150 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addf.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addf.bend&start_line=132&end_line=150 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/lemmas/proofs/nat_algebra.bend as NA 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/f64addg.bend as AG import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addh.bend as AH def caseGT(+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}, +ha: {Nat.is_eq(ea, 2047n) == False{} : Bool}, +hgt: {Nat.is_lt(eb, ea) == 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, GT{}), F.sm_case(x, y, sa, ea, eb, GT{})) == SF.add_mag(sa, C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), sb, AG.mt(eb, Fb), AG.xe(eb)) : F.F64}: match sg: case True{}: +i1 = Equal.cong(Bool, F.F64, t => F.am_big(x, sa, ea, F.frac(x), eb, F.frac(y), t), Nat.is_eq(ea, 2047n), False{}, ha) +i2 = AH.bigA(one, h1, sa, ea, F.frac(x), eb, F.frac(y), Fa, Fb, hfa, hfb, hFa, hFb, hgt) +i3 = Equal.cong(Nat, F.F64, z => SF.round(sa, z, AG.xe(eb)), Nat.add(AG.mt(eb, Fb), C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa))), Nat.add(C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), AG.mt(eb, Fb)), NA.add_comm(AG.mt(eb, Fb), C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)))) +sp = Equal.cong(Bool, F.F64, t => SF.pick(F.F64, t, SF.round(sa, Nat.add(C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), AG.mt(eb, Fb)), AG.xe(eb)), SF.sub_mag(sa, C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), sb, AG.mt(eb, Fb), AG.xe(eb), Nat.cmp(C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), AG.mt(eb, Fb)))), Bool.not(Bool.xor(sa, sb)), True{}, hsg) +imp = Equal.trans(F.F64, F.am_case(x, y, sa, ea, eb, GT{}), F.rp62(sa, Nat.add(F.off(), ea), X.add(X.add(WU.U64{0, 536870912}, X.shl(F.frac(x), 9n)), X.shr_jam(F.am_small(eb, X.shl(F.frac(y), 9n)), Nat.sub(ea, eb)))), SF.round(sa, Nat.add(C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), AG.mt(eb, Fb)), AG.xe(eb)), i1, Equal.trans(F.F64, F.rp62(sa, Nat.add(F.off(), ea), X.add(X.add(WU.U64{0, 536870912}, X.shl(F.frac(x), 9n)), X.shr_jam(F.am_small(eb, X.shl(F.frac(y), 9n)), Nat.sub(ea, eb)))), SF.round(sa, Nat.add(AG.mt(eb, Fb), C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa))), AG.xe(eb)), SF.round(sa, Nat.add(C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), AG.mt(eb, Fb)), AG.xe(eb)), i2, i3)) Equal.trans(F.F64, SF.pick(F.F64, True{}, F.am_case(x, y, sa, ea, eb, GT{}), F.sm_case(x, y, sa, ea, eb, GT{})), F.am_case(x, y, sa, ea, eb, GT{}), SF.add_mag(sa, C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), sb, AG.mt(eb, Fb), AG.xe(eb)), FR.pk_t(F.F64, F.am_case(x, y, sa, ea, eb, GT{}), F.sm_case(x, y, sa, ea, eb, GT{})), Equal.trans(F.F64, F.am_case(x, y, sa, ea, eb, GT{}), SF.round(sa, Nat.add(C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), AG.mt(eb, Fb)), AG.xe(eb)), SF.add_mag(sa, C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), sb, AG.mt(eb, Fb), AG.xe(eb)), imp, Equal.sym(F.F64, SF.add_mag(sa, C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), sb, AG.mt(eb, Fb), AG.xe(eb)), SF.round(sa, Nat.add(C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), AG.mt(eb, Fb)), AG.xe(eb)), sp))) case False{}: +i1 = Equal.cong(Bool, F.F64, t => F.sm_big(x, sa, ea, F.frac(x), eb, F.frac(y), t), Nat.is_eq(ea, 2047n), False{}, ha) +i2 = AH.bigS(one, h1, sa, ea, F.frac(x), eb, F.frac(y), Fa, Fb, hfa, hfb, hFa, hFb, hgt) +c1 = AG.bigcmp(one, h1, ea, eb, Fa, Fb, hFa, hFb, hgt) +c2 = Equal.trans(Cmp, Nat.cmp(C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), AG.mt(eb, Fb)), SF.flip(Nat.cmp(AG.mt(eb, Fb), C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)))), GT{}, Equal.sym(Cmp, SF.flip(Nat.cmp(AG.mt(eb, Fb), C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)))), Nat.cmp(C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), AG.mt(eb, Fb)), NC.cmp_flip(AG.mt(eb, Fb), C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)))), Equal.cong(Cmp, Cmp, t => SF.flip(t), Nat.cmp(AG.mt(eb, Fb), C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa))), LT{}, c1)) +sp1 = Equal.cong(Bool, F.F64, t => SF.pick(F.F64, t, SF.round(sa, Nat.add(C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), AG.mt(eb, Fb)), AG.xe(eb)), SF.sub_mag(sa, C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), sb, AG.mt(eb, Fb), AG.xe(eb), Nat.cmp(C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), AG.mt(eb, Fb)))), Bool.not(Bool.xor(sa, sb)), False{}, hsg) +sp2 = Equal.cong(Cmp, F.F64, t => SF.sub_mag(sa, C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), sb, AG.mt(eb, Fb), AG.xe(eb), t), Nat.cmp(C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), AG.mt(eb, Fb)), GT{}, c2) +imp = Equal.trans(F.F64, F.sm_case(x, y, sa, ea, eb, GT{}), F.norm_round_pack(sa, Nat.add(F.off(), Nat.sub(ea, 1n)), X.sub(X.add(X.shl(F.frac(x), 10n), WU.U64{0, 1073741824}), X.shr_jam(F.sm_small(eb, X.shl(F.frac(y), 10n)), Nat.sub(ea, eb)))), SF.round(sa, Nat.sub(C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), AG.mt(eb, Fb)), AG.xe(eb)), i1, i2) +spc = Equal.trans(F.F64, SF.add_mag(sa, C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), sb, AG.mt(eb, Fb), AG.xe(eb)), SF.sub_mag(sa, C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), sb, AG.mt(eb, Fb), AG.xe(eb), Nat.cmp(C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), AG.mt(eb, Fb))), SF.round(sa, Nat.sub(C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), AG.mt(eb, Fb)), AG.xe(eb)), sp1, sp2) Equal.trans(F.F64, SF.pick(F.F64, False{}, F.am_case(x, y, sa, ea, eb, GT{}), F.sm_case(x, y, sa, ea, eb, GT{})), F.sm_case(x, y, sa, ea, eb, GT{}), SF.add_mag(sa, C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), sb, AG.mt(eb, Fb), AG.xe(eb)), FR.pk_f(F.F64, F.am_case(x, y, sa, ea, eb, GT{}), F.sm_case(x, y, sa, ea, eb, GT{})), Equal.trans(F.F64, F.sm_case(x, y, sa, ea, eb, GT{}), SF.round(sa, Nat.sub(C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), AG.mt(eb, Fb)), AG.xe(eb)), SF.add_mag(sa, C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), sb, AG.mt(eb, Fb), AG.xe(eb)), imp, Equal.sym(F.F64, SF.add_mag(sa, C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), sb, AG.mt(eb, Fb), AG.xe(eb)), SF.round(sa, Nat.sub(C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), AG.mt(eb, Fb)), AG.xe(eb)), spc))) Uses (46): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.not https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.xor https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Cmp 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.cmp https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub 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/math/typed/f64addg.bend&name=bigcmp https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addg.bend&name=mt https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addg.bend&name=xe https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addh.bend&name=bigA https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addh.bend&name=bigS https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend&name=pk_f https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend&name=pk_t https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/natcmp.bend&name=cmp_flip 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=shift https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=add_mag https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=flip https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=pick https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=round https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=sub_mag 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/f64.bend&name=F64 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=am_big https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=am_case https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=am_small https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=frac https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=norm_round_pack https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=off https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=rp62 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=sm_big https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=sm_case https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=sm_small 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=shl https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/w64.bend&name=shr_jam https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/w64.bend&name=sub