def pw_val

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

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/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend as LW

1109def pw_val(+x: U32, +k: Nat, p: {mode(Nat.is_le(1n, v(x)), v(x)) == True{} : Bool} & {mode(Nat.is_le(1n, v(x)), 1n) == True{} : Bool}) -> {G.pow_go(~U32, ~I.u32_op, ~I.u32_is, 1n+k, k, x, True{}, (I.u32_op(NM.One{}), True{})) == G.fits(U32, Bool.not(C.fits(32n, Nat.pow(v(x), k))), of(Nat.pow(v(x), k))) : Maybe<&2, U32>}:
1110  (+hmb, +hma) = p
1111  +t0 = Nat.pow(v(x), k)
1112  +ht = Equal.trans(Nat, Nat.mul(1n, t0), Nat.add(t0, 0n), t0, {==}, N.add_zero(t0))
1113  powsim(1n+k, k, x, True{}, I.u32_op(NM.One{}), True{}, v(x), 1n, t0, Nat.is_le(1n, v(x)), C.fits(32n, t0), N.le_succ(k), LW.vb(x), {==}, hmb, {==}, one_v(), hma, ht, {==})