def step_q

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

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/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/math/typed/w64dmtop.bend as DQ

132def step_q(+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}, +rw: WU.U64, +N0: Nat, +p: Nat, +ht: {Nat.is_le(1n+p, 10n) == True{} : Bool}, +hr: {SW.value(rw) == Nat.mod(N0, 1n+bp) : Nat}) -> {Nat.mod(SW.value(X.pfst(X.divmod(X.shl(rw, 1n+p), b))), 2n) == Nat.mod(Nat.div(C.shift(1n+p, N0), 1n+bp), 2n) : Nat}:
133  +A = X.shl(rw, 1n+p)
134  +eA = shl_t(rw, 1n+p, ht, rfit(bp, hB, rw, N0, hr))
135  +e2 = Equal.cong(Nat, Nat, u => Nat.div(u, SW.value(b)), SW.value(A), C.shift(1n+p, SW.value(rw)), eA)
136  +e3 = Equal.cong(Nat, Nat, u => Nat.div(C.shift(1n+p, u), SW.value(b)), SW.value(rw), Nat.mod(N0, 1n+bp), hr)
137  +e4 = Equal.cong(Nat, Nat, u => Nat.div(C.shift(1n+p, Nat.mod(N0, 1n+bp)), u), SW.value(b), 1n+bp, eB)
138  +d1 = Nat.div(SW.value(A), SW.value(b))
139  +d2 = Nat.div(C.shift(1n+p, SW.value(rw)), SW.value(b))
140  +d3 = Nat.div(C.shift(1n+p, Nat.mod(N0, 1n+bp)), SW.value(b))
141  +d4 = Nat.div(C.shift(1n+p, Nat.mod(N0, 1n+bp)), 1n+bp)
142  +ed = Equal.trans(Nat, SW.value(X.quot(A, b)), d1, d4, DQ.divmod_quot(A, b, hbz), Equal.trans(Nat, d1, d2, d4, e2, Equal.trans(Nat, d2, d3, d4, e3, e4)))
143  Equal.trans(Nat, Nat.mod(SW.value(X.quot(A, b)), 2n), Nat.mod(d4, 2n), Nat.mod(Nat.div(C.shift(1n+p, N0), 1n+bp), 2n), Equal.cong(Nat, Nat, u => Nat.mod(u, 2n), SW.value(X.quot(A, b)), d4, ed), par_shift(N0, bp, p))