def rp_c
bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64round.bend:249
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as F64round
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/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/natcmp.bend as NC
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend as SH
import bend-collections-laws-math@1.0.0.0/proofs/lib/u32half.bend as UH
249def rp_c(+q0: Nat, +r0: Nat, +hr: {C.fits(10n, r0) == True{} : Bool}, +c: Cmp, +hc: {Nat.cmp(r0, 512n) == c : Cmp}) -> {SF.pick(Nat, Nat.is_eq(r0, 512n), Nat.sub(Nat.add(q0, C.high(10n, Nat.add(r0, 512n))), Nat.mod(Nat.add(q0, C.high(10n, Nat.add(r0, 512n))), 2n)), Nat.add(q0, C.high(10n, Nat.add(r0, 512n)))) == SF.rne_up(q0, r0, 512n) : Nat}:
250 match c:
251 case LT{}:
252 +hlt = NC.lt_of_cmp(r0, 512n, hc)
253 +he = Equal.cong(Cmp, Bool, t => Cmp.is_eq(t), Nat.cmp(r0, 512n), LT{}, hc)
254 +hg = Equal.cong(Cmp, Bool, t => Cmp.is_lt(t), Nat.cmp(512n, r0), GT{}, Equal.trans(Cmp, Nat.cmp(512n, r0), SF.flip(Nat.cmp(r0, 512n)), GT{}, Equal.sym(Cmp, SF.flip(Nat.cmp(r0, 512n)), Nat.cmp(512n, r0), NC.cmp_flip(r0, 512n)), Equal.cong(Cmp, Cmp, t => SF.flip(t), Nat.cmp(r0, 512n), LT{}, hc)))
255 +f = WW.fits_of_lt(10n, Nat.add(r0, 512n), N.lt_add_r2(r0, 512n, 512n, hlt))
256 +h0 = N.eq_from_is_eq(C.high(10n, Nat.add(r0, 512n)), 0n, f)
257 +l1 = Equal.cong(Bool, Nat, t => SF.pick(Nat, t, Nat.sub(Nat.add(q0, C.high(10n, Nat.add(r0, 512n))), Nat.mod(Nat.add(q0, C.high(10n, Nat.add(r0, 512n))), 2n)), Nat.add(q0, C.high(10n, Nat.add(r0, 512n)))), Nat.is_eq(r0, 512n), False{}, he)
258 +l2 = Equal.cong(Nat, Nat, z => Nat.add(q0, z), C.high(10n, Nat.add(r0, 512n)), 0n, h0)
259 +r1 = Equal.cong(Bool, Nat, t => Nat.add(q0, SF.b2n(Bool.or(t, Bool.and(Nat.is_eq(r0, 512n), Nat.is_eq(Nat.mod(q0, 2n), 1n))))), Nat.is_lt(512n, r0), False{}, hg)
260 +r2 = Equal.cong(Bool, Nat, t => Nat.add(q0, SF.b2n(Bool.or(False{}, Bool.and(t, Nat.is_eq(Nat.mod(q0, 2n), 1n))))), Nat.is_eq(r0, 512n), False{}, he)
261 Equal.trans(Nat, SF.pick(Nat, Nat.is_eq(r0, 512n), Nat.sub(Nat.add(q0, C.high(10n, Nat.add(r0, 512n))), Nat.mod(Nat.add(q0, C.high(10n, Nat.add(r0, 512n))), 2n)), Nat.add(q0, C.high(10n, Nat.add(r0, 512n)))), Nat.add(q0, C.high(10n, Nat.add(r0, 512n))), SF.rne_up(q0, r0, 512n), l1, Equal.trans(Nat, Nat.add(q0, C.high(10n, Nat.add(r0, 512n))), Nat.add(q0, 0n), SF.rne_up(q0, r0, 512n), l2, Equal.sym(Nat, SF.rne_up(q0, r0, 512n), Nat.add(q0, 0n), Equal.trans(Nat, SF.rne_up(q0, r0, 512n), Nat.add(q0, SF.b2n(Bool.or(False{}, Bool.and(Nat.is_eq(r0, 512n), Nat.is_eq(Nat.mod(q0, 2n), 1n))))), Nat.add(q0, 0n), r1, r2))))
262 case GT{}:
263 +hgt = NC.lt_of_gt(r0, 512n, hc)
264 +he = Equal.cong(Cmp, Bool, t => Cmp.is_eq(t), Nat.cmp(r0, 512n), GT{}, hc)
265 +d = Nat.sub(r0, 512n)
266 +ed = N.sub_add(r0, 512n, N.lt_le(512n, r0, hgt))
267 +ex = Equal.trans(Nat, Nat.add(r0, 512n), Nat.add(Nat.add(512n, d), 512n), Nat.add(d, C.shift(10n, 1n)), Equal.cong(Nat, Nat, z => Nat.add(z, 512n), r0, Nat.add(512n, d), Equal.sym(Nat, Nat.add(512n, d), r0, ed)), Equal.trans(Nat, Nat.add(Nat.add(512n, d), 512n), Nat.add(512n, Nat.add(d, 512n)), Nat.add(d, C.shift(10n, 1n)), NA.add_assoc(512n, d, 512n), Equal.trans(Nat, Nat.add(512n, Nat.add(d, 512n)), Nat.add(1024n, d), Nat.add(d, C.shift(10n, 1n)), Equal.cong(Nat, Nat, z => Nat.add(512n, z), Nat.add(d, 512n), Nat.add(512n, d), NA.add_comm(d, 512n)), NA.add_comm(1024n, d))))
268 +hd = SH.fits_lek(10n, d, r0, UH.sub_le(r0, 512n), hr)
269 +h1 = Equal.trans(Nat, C.high(10n, Nat.add(r0, 512n)), C.high(10n, Nat.add(d, C.shift(10n, 1n))), 1n, Equal.cong(Nat, Nat, z => C.high(10n, z), Nat.add(r0, 512n), Nat.add(d, C.shift(10n, 1n)), ex), WW.high_u(10n, d, 1n, hd))
270 +l1 = Equal.cong(Bool, Nat, t => SF.pick(Nat, t, Nat.sub(Nat.add(q0, C.high(10n, Nat.add(r0, 512n))), Nat.mod(Nat.add(q0, C.high(10n, Nat.add(r0, 512n))), 2n)), Nat.add(q0, C.high(10n, Nat.add(r0, 512n)))), Nat.is_eq(r0, 512n), False{}, he)
271 +l2 = Equal.cong(Nat, Nat, z => Nat.add(q0, z), C.high(10n, Nat.add(r0, 512n)), 1n, h1)
272 +r1 = Equal.cong(Bool, Nat, t => Nat.add(q0, SF.b2n(Bool.or(t, Bool.and(Nat.is_eq(r0, 512n), Nat.is_eq(Nat.mod(q0, 2n), 1n))))), Nat.is_lt(512n, r0), True{}, hgt)
273 Equal.trans(Nat, SF.pick(Nat, Nat.is_eq(r0, 512n), Nat.sub(Nat.add(q0, C.high(10n, Nat.add(r0, 512n))), Nat.mod(Nat.add(q0, C.high(10n, Nat.add(r0, 512n))), 2n)), Nat.add(q0, C.high(10n, Nat.add(r0, 512n)))), Nat.add(q0, C.high(10n, Nat.add(r0, 512n))), SF.rne_up(q0, r0, 512n), l1, Equal.trans(Nat, Nat.add(q0, C.high(10n, Nat.add(r0, 512n))), Nat.add(q0, 1n), SF.rne_up(q0, r0, 512n), l2, Equal.sym(Nat, SF.rne_up(q0, r0, 512n), Nat.add(q0, 1n), r1)))
274 case EQ{}:
275 +er = NC.eq_of_cmp(r0, 512n, hc)
276 +b1 = subm(Nat.add(q0, 1n))
277 +b2 = Equal.trans(Nat, Nat.add(q0, SF.b2n(Nat.is_eq(Nat.mod(q0, 2n), 1n))), Nat.add(q0, SF.b2n(Nat.is_eq(C.bit(q0), 1n))), Nat.double(C.half(Nat.add(q0, 1n))), Equal.cong(Nat, Nat, z => Nat.add(q0, SF.b2n(Nat.is_eq(z, 1n))), Nat.mod(q0, 2n), C.bit(q0), Equal.sym(Nat, C.bit(q0), Nat.mod(q0, 2n), WW.bit_mod(q0))), parq(q0))
278 +base = Equal.trans(Nat, Nat.sub(Nat.add(q0, 1n), Nat.mod(Nat.add(q0, 1n), 2n)), Nat.double(C.half(Nat.add(q0, 1n))), Nat.add(q0, SF.b2n(Nat.is_eq(Nat.mod(q0, 2n), 1n))), b1, Equal.sym(Nat, Nat.add(q0, SF.b2n(Nat.is_eq(Nat.mod(q0, 2n), 1n))), Nat.double(C.half(Nat.add(q0, 1n))), b2))
279 L.subst(Nat, z => {SF.pick(Nat, Nat.is_eq(z, 512n), Nat.sub(Nat.add(q0, C.high(10n, Nat.add(z, 512n))), Nat.mod(Nat.add(q0, C.high(10n, Nat.add(z, 512n))), 2n)), Nat.add(q0, C.high(10n, Nat.add(z, 512n)))) == SF.rne_up(q0, z, 512n) : Nat}, 512n, r0, Equal.sym(Nat, r0, 512n, er), base)