def rl_v

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u64int.bend:1126

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/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/instances.bend as I
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU

1126def rl_v(+K: Nat, +hK: {K == 64n : Nat}, +n: WU.U64, +k: Nat, +r: WU.U64) -> {G.root_le(~WU.U64, ~I.u64_op, ~I.u64_is, n, k, r) == Nat.is_le(Nat.pow(v(r), k), v(n)) : Bool}:
1127  +P = Nat.pow(v(r), k)
1128  Equal.trans(Bool, G.root_le_fin(~WU.U64, ~I.u64_op, ~I.u64_is, n, G.pow_go(~WU.U64, ~I.u64_op, ~I.u64_is, 1n+k, k, r, True{}, (I.u64_op(NM.One{}), True{}))), G.root_le_fin(~WU.U64, ~I.u64_op, ~I.u64_is, n, G.fits(WU.U64, Bool.not(C.fits(64n, P)), of(P))), Nat.is_le(P, v(n)), Equal.cong(Maybe<&2, WU.U64>, Bool, t => G.root_le_fin(~WU.U64, ~I.u64_op, ~I.u64_is, n, t), G.pow_go(~WU.U64, ~I.u64_op, ~I.u64_is, 1n+k, k, r, True{}, (I.u64_op(NM.One{}), True{})), G.fits(WU.U64, Bool.not(C.fits(64n, P)), of(P)), pw_val(r, k, md_init(v(r)))), rlf(K, hK, n, P, C.fits(64n, P), {==}))