def stepv

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u32int.bend:544

import Base
import bend-collections-laws-math@1.0.0.0/src/math/generic.bend as G
import bend-collections-laws-math@1.0.0.0/src/math/num.bend as NM
import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M
import bend-collections-laws-math@1.0.0.0/src/math/instances.bend as I
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as NR
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend as LW

544def stepv(+k: Nat, +hk: {k == 32n : Nat}, +m: U32, +mp: Nat, +hm: {v(m) == 1n+mp : Nat}, +q: U32, +s0: U32, +s1: U32, +nq: Nat, +ns0: Nat, +ns1: Nat, +hq: {v(q) == nq : Nat}, +hs0: {v(s0) == ns0 : Nat}, +hs1: {v(s1) == ns1 : Nat}, +hb0: {Nat.is_lt(ns0, 1n+mp) == True{} : Bool}, +hb1: {Nat.is_lt(ns1, 1n+mp) == True{} : Bool}) -> {v(G.inv_step(~U32, ~I.u32_op, ~I.u32_is, m, q, s0, s1)) == M.inv_step(1n+mp, nq, ns0, ns1) : Nat}:
545  +rq = I.u32_op(NM.Rem{q, m})
546  +erq = Equal.trans(Nat, v(rq), Nat.mod(v(q), 1n+mp), Nat.mod(nq, 1n+mp), pm_rem(q, m, mp, hm), Equal.cong(Nat, Nat, t => Nat.mod(t, 1n+mp), v(q), nq, hq))
547  +x = I.u32_op(NM.MulMod{rq, s1, m})
548  e1 = LW.ops_mulmod(rq, s1, m, lt_mn(rq, m, mp, hm, Nat.mod(nq, 1n+mp), erq, NR.dm_lt(mp, nq)), lt_mn(s1, m, mp, hm, ns1, hs1, hb1))
549  +e2 = Equal.trans(Nat, Nat.mod(Nat.mul(v(rq), v(s1)), v(m)), Nat.mod(Nat.mul(v(rq), v(s1)), 1n+mp), Nat.mod(Nat.mul(Nat.mod(nq, 1n+mp), ns1), 1n+mp), Equal.cong(Nat, Nat, t => Nat.mod(Nat.mul(v(rq), v(s1)), t), v(m), 1n+mp, hm), Equal.trans(Nat, Nat.mod(Nat.mul(v(rq), v(s1)), 1n+mp), Nat.mod(Nat.mul(Nat.mod(nq, 1n+mp), v(s1)), 1n+mp), Nat.mod(Nat.mul(Nat.mod(nq, 1n+mp), ns1), 1n+mp), Equal.cong(Nat, Nat, t => Nat.mod(Nat.mul(t, v(s1)), 1n+mp), v(rq), Nat.mod(nq, 1n+mp), erq), Equal.cong(Nat, Nat, t => Nat.mod(Nat.mul(Nat.mod(nq, 1n+mp), t), 1n+mp), v(s1), ns1, hs1)))
550  +ex = Equal.trans(Nat, v(x), Nat.mod(Nat.mul(v(rq), v(s1)), v(m)), Nat.mod(Nat.mul(nq, ns1), 1n+mp), e1, Equal.trans(Nat, Nat.mod(Nat.mul(v(rq), v(s1)), v(m)), Nat.mod(Nat.mul(Nat.mod(nq, 1n+mp), ns1), 1n+mp), Nat.mod(Nat.mul(nq, ns1), 1n+mp), e2, NR.mod_mul_l(mp, nq, ns1)))
551  subv(k, hk, m, mp, hm, s0, x, ns0, Nat.mod(Nat.mul(nq, ns1), 1n+mp), hs0, ex, hb0, NR.dm_lt(mp, Nat.mul(nq, ns1)), I.u32_is(NM.Lt{s0, x}), {==})