def step_r

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

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/w64dmrem.bend as DR

119def step_r(+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, +t: Nat, +ht: {Nat.is_le(t, 10n) == True{} : Bool}, +hr: {SW.value(rw) == Nat.mod(N0, 1n+bp) : Nat}) -> {SW.value(X.psnd(X.divmod(X.shl(rw, t), b))) == Nat.mod(C.shift(t, N0), 1n+bp) : Nat}:
120  +A = X.shl(rw, t)
121  +eA = shl_t(rw, t, ht, rfit(bp, hB, rw, N0, hr))
122  +e2 = Equal.cong(Nat, Nat, u => Nat.mod(u, SW.value(b)), SW.value(A), C.shift(t, SW.value(rw)), eA)
123  +e3 = Equal.cong(Nat, Nat, u => Nat.mod(C.shift(t, u), SW.value(b)), SW.value(rw), Nat.mod(N0, 1n+bp), hr)
124  +e4 = Equal.cong(Nat, Nat, u => Nat.mod(C.shift(t, Nat.mod(N0, 1n+bp)), u), SW.value(b), 1n+bp, eB)
125  +m1 = Nat.mod(SW.value(A), SW.value(b))
126  +m2 = Nat.mod(C.shift(t, SW.value(rw)), SW.value(b))
127  +m3 = Nat.mod(C.shift(t, Nat.mod(N0, 1n+bp)), SW.value(b))
128  +m4 = Nat.mod(C.shift(t, Nat.mod(N0, 1n+bp)), 1n+bp)
129  +m5 = Nat.mod(C.shift(t, N0), 1n+bp)
130  Equal.trans(Nat, SW.value(X.rem(A, b)), m1, m5, DR.divmod_rem(A, b, hbz), Equal.trans(Nat, m1, m2, m5, e2, Equal.trans(Nat, m2, m3, m5, e3, Equal.trans(Nat, m3, m4, m5, e4, mod_shift(N0, bp, t)))))