def loop_r

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64fmod.bend:156

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/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/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64light.bend as FL
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64exp.bend as EX

156def loop_r(fuel: Nat, +b: WU.U64, +bp: Nat, +eB: {SW.value(b) == 1n+bp : Nat}, +hB: {C.fits(53n, 1n+bp) == True{} : Bool}, +hbz: {X.is_zero(b) == False{} : Bool}, +d: Nat, +hd: {Nat.is_le(d, fuel) == True{} : Bool}, +q: WU.U64, +r: WU.U64, +N0: Nat, +hr: {SW.value(r) == Nat.mod(N0, 1n+bp) : Nat}) -> {SW.value(X.psnd(F.fm_go(fuel, b, d, (q, r)))) == Nat.mod(C.shift(d, N0), 1n+bp) : Nat}:
157  match fuel d:
158    case 0n 0n:
159      hr
160    case 0n 1n+ +e:
161      Empty.absurd({SW.value(X.psnd(F.fm_go(0n, b, 1n+e, (q, r)))) == Nat.mod(C.shift(1n+e, N0), 1n+bp) : Nat}, FL.true_ne_false(Equal.sym(Bool, False{}, True{}, hd)))
162    case 1n+ +f 0n:
163      hr
164    case 1n+ +f 1n+ +e:
165      +t = Nat.min(1n+e, 10n)
166      +d2 = Nat.sub(1n+e, t)
167      +hr2 = step_r(b, bp, eB, hB, hbz, r, N0, t, min_le_r(1n+e, 10n), hr)
168      +hd2 = N.le_trans(Nat.sub(e, Nat.min(e, 9n)), e, f, EX.sub_le_self(e, Nat.min(e, 9n)), hd)
169      +ee = Equal.cong(WU.U64 & WU.U64, Nat, u => SW.value(X.psnd(F.fm_go(f, b, d2, u))), X.divmod(X.shl(r, t), b), (X.pfst(X.divmod(X.shl(r, t), b)), X.psnd(X.divmod(X.shl(r, t), b))), eta(X.divmod(X.shl(r, t), b)))
170      +rec = loop_r(f, b, bp, eB, hB, hbz, d2, hd2, X.pfst(X.divmod(X.shl(r, t), b)), X.psnd(X.divmod(X.shl(r, t), b)), C.shift(t, N0), hr2)
171      +es = Equal.cong(Nat, Nat, u => Nat.mod(u, 1n+bp), C.shift(d2, C.shift(t, N0)), C.shift(1n+e, N0), shc(e, t, N0, min_le_l(1n+e, 10n)))
172      Equal.trans(Nat, SW.value(X.psnd(F.fm_go(f, b, d2, X.divmod(X.shl(r, t), b)))), SW.value(X.psnd(F.fm_go(f, b, d2, (X.pfst(X.divmod(X.shl(r, t), b)), X.psnd(X.divmod(X.shl(r, t), b)))))), Nat.mod(C.shift(1n+e, N0), 1n+bp), ee, Equal.trans(Nat, SW.value(X.psnd(F.fm_go(f, b, d2, (X.pfst(X.divmod(X.shl(r, t), b)), X.psnd(X.divmod(X.shl(r, t), b)))))), Nat.mod(C.shift(d2, C.shift(t, N0)), 1n+bp), Nat.mod(C.shift(1n+e, N0), 1n+bp), rec, es))