def loop_q

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

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

174def loop_q(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}, +hq: {Nat.mod(SW.value(q), 2n) == Nat.mod(Nat.div(N0, 1n+bp), 2n) : Nat}) -> {Nat.mod(SW.value(X.pfst(F.fm_go(fuel, b, d, (q, r)))), 2n) == Nat.mod(Nat.div(C.shift(d, N0), 1n+bp), 2n) : Nat}:
175  match fuel d:
176    case 0n 0n:
177      hq
178    case 0n 1n+ +e:
179      Empty.absurd({Nat.mod(SW.value(X.pfst(F.fm_go(0n, b, 1n+e, (q, r)))), 2n) == Nat.mod(Nat.div(C.shift(1n+e, N0), 1n+bp), 2n) : Nat}, FL.true_ne_false(Equal.sym(Bool, False{}, True{}, hd)))
180    case 1n+ +f 0n:
181      hq
182    case 1n+ +f 1n+ +e:
183      +t = Nat.min(1n+e, 10n)
184      +d2 = Nat.sub(1n+e, t)
185      +hr2 = step_r(b, bp, eB, hB, hbz, r, N0, t, min_le_r(1n+e, 10n), hr)
186      +hq2 = step_q(b, bp, eB, hB, hbz, r, N0, Nat.min(e, 9n), min_le_r(e, 9n), hr)
187      +hd2 = N.le_trans(Nat.sub(e, Nat.min(e, 9n)), e, f, EX.sub_le_self(e, Nat.min(e, 9n)), hd)
188      +ee = Equal.cong(WU.U64 & WU.U64, Nat, u => Nat.mod(SW.value(X.pfst(F.fm_go(f, b, d2, u))), 2n), 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)))
189      +rec = loop_q(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, hq2)
190      +es = Equal.cong(Nat, Nat, u => Nat.mod(Nat.div(u, 1n+bp), 2n), C.shift(d2, C.shift(t, N0)), C.shift(1n+e, N0), shc(e, t, N0, min_le_l(1n+e, 10n)))
191      Equal.trans(Nat, Nat.mod(SW.value(X.pfst(F.fm_go(f, b, d2, X.divmod(X.shl(r, t), b)))), 2n), Nat.mod(SW.value(X.pfst(F.fm_go(f, b, d2, (X.pfst(X.divmod(X.shl(r, t), b)), X.psnd(X.divmod(X.shl(r, t), b)))))), 2n), Nat.mod(Nat.div(C.shift(1n+e, N0), 1n+bp), 2n), ee, Equal.trans(Nat, Nat.mod(SW.value(X.pfst(F.fm_go(f, b, d2, (X.pfst(X.divmod(X.shl(r, t), b)), X.psnd(X.divmod(X.shl(r, t), b)))))), 2n), Nat.mod(Nat.div(C.shift(d2, C.shift(t, N0)), 1n+bp), 2n), Nat.mod(Nat.div(C.shift(1n+e, N0), 1n+bp), 2n), rec, es))