def bigcmp_c

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64addg.bend:130

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/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/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as FR

130def bigcmp_c(+one: Nat, +h1: {one == 1n : Nat}, +el: Nat, +es: Nat, +Fl: Nat, +Fs: Nat, +hFl: {C.fits(52n, Fl) == True{} : Bool}, +hFs: {C.fits(52n, Fs) == True{} : Bool}, +hlt: {Nat.is_lt(es, el) == True{} : Bool}, +z: Bool, +hz: {Nat.is_eq(es, 0n) == z : Bool}) -> {Nat.is_lt(mt(es, Fs), C.shift(Nat.sub(xe(el), xe(es)), mt(el, Fl))) == True{} : Bool}:
131  match z:
132    case True{}:
133      +hl1 = N.lt_succ_le_succ(es, el, hlt)
134      +hel = posz(el, N.le_trans(1n, 1n+es, el, N.zero_le(es), hl1))
135      +ml = mt_n(one, h1, el, Fl, hel)
136      +hPl = L.subst(Nat, w => {Nat.is_le(C.shift(52n, one), w) == True{} : Bool}, Nat.add(C.shift(52n, one), Fl), Nat.add(Fl, C.shift(52n, one)), NA.add_comm(C.shift(52n, one), Fl), N.le_add_right(C.shift(52n, one), Fl))
137      +hPm = L.subst(Nat, w => {Nat.is_le(C.shift(52n, one), w) == True{} : Bool}, Nat.add(Fl, C.shift(52n, one)), mt(el, Fl), Equal.sym(Nat, mt(el, Fl), Nat.add(Fl, C.shift(52n, one)), ml), hPl)
138      +ms = mt_z(es, Fs, hz)
139      +l0 = Equal.trans(Bool, Nat.is_lt(Fs, C.shift(52n, one)), C.fits(52n, Fs), True{}, FR.lt_fit(52n, one, h1, Fs), hFs)
140      +l1 = N.lt_le_trans(Fs, C.shift(52n, one), C.shift(Nat.sub(xe(el), xe(es)), mt(el, Fl)), l0, N.le_trans(C.shift(52n, one), mt(el, Fl), C.shift(Nat.sub(xe(el), xe(es)), mt(el, Fl)), hPm, WW.shift_ge(Nat.sub(xe(el), xe(es)), mt(el, Fl))))
141      L.subst(Nat, w => {Nat.is_lt(w, C.shift(Nat.sub(xe(el), xe(es)), mt(el, Fl))) == True{} : Bool}, Fs, mt(es, Fs), Equal.sym(Nat, mt(es, Fs), Fs, ms), l1)
142    case False{}:
143      +hl1 = N.lt_succ_le_succ(es, el, hlt)
144      +hel = posz(el, N.le_trans(1n, 1n+es, el, N.zero_le(es), hl1))
145      +ml = mt_n(one, h1, el, Fl, hel)
146      +hPl = L.subst(Nat, w => {Nat.is_le(C.shift(52n, one), w) == True{} : Bool}, Nat.add(C.shift(52n, one), Fl), Nat.add(Fl, C.shift(52n, one)), NA.add_comm(C.shift(52n, one), Fl), N.le_add_right(C.shift(52n, one), Fl))
147      +hPm = L.subst(Nat, w => {Nat.is_le(C.shift(52n, one), w) == True{} : Bool}, Nat.add(Fl, C.shift(52n, one)), mt(el, Fl), Equal.sym(Nat, mt(el, Fl), Nat.add(Fl, C.shift(52n, one)), ml), hPl)
148      +ms = mt_n(one, h1, es, Fs, hz)
149      +xs = xe_n(es, hz)
150      +xl = xe_n(el, hel)
151      +ed = Equal.trans(Nat, Nat.sub(xe(el), xe(es)), Nat.sub(Nat.add(1925n, el), Nat.add(1925n, es)), Nat.sub(el, es), Equal.trans(Nat, Nat.sub(xe(el), xe(es)), Nat.sub(Nat.add(1925n, el), xe(es)), Nat.sub(Nat.add(1925n, el), Nat.add(1925n, es)), Equal.cong(Nat, Nat, w => Nat.sub(w, xe(es)), xe(el), Nat.add(1925n, el), xl), Equal.cong(Nat, Nat, w => Nat.sub(Nat.add(1925n, el), w), xe(es), Nat.add(1925n, es), xs)), sub_kk(1925n, el, es))
152      +hd = L.subst(Nat, w => {Nat.is_le(1n, w) == True{} : Bool}, Nat.sub(el, es), Nat.sub(xe(el), xe(es)), Equal.sym(Nat, Nat.sub(xe(el), xe(es)), Nat.sub(el, es), ed), FR.lt_sub_pos(es, el, hlt))
153      +l0 = Equal.trans(Bool, Nat.is_lt(Nat.add(Fs, C.shift(52n, one)), C.shift(53n, one)), C.fits(53n, Nat.add(Fs, C.shift(52n, one))), True{}, FR.lt_fit(53n, one, h1, Nat.add(Fs, C.shift(52n, one))), f53(one, h1, Fs, hFs))
154      +l2 = N.le_trans(C.shift(1n, C.shift(52n, one)), C.shift(1n, mt(el, Fl)), C.shift(Nat.sub(xe(el), xe(es)), mt(el, Fl)), WW.shift_mono(1n, C.shift(52n, one), mt(el, Fl), hPm), shmk(1n, Nat.sub(xe(el), xe(es)), mt(el, Fl), hd))
155      +l1 = N.lt_le_trans(Nat.add(Fs, C.shift(52n, one)), C.shift(53n, one), C.shift(Nat.sub(xe(el), xe(es)), mt(el, Fl)), l0, l2)
156      L.subst(Nat, w => {Nat.is_lt(w, C.shift(Nat.sub(xe(el), xe(es)), mt(el, Fl))) == True{} : Bool}, Nat.add(Fs, C.shift(52n, one)), mt(es, Fs), Equal.sym(Nat, mt(es, Fs), Nat.add(Fs, C.shift(52n, one)), ms), l1)