def rlf

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

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/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/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32.bend as U32P
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend as LW

1115def rlf(+K: Nat, +hK: {K == 32n : Nat}, +n: U32, +P: Nat, +c: Bool, +hc: {C.fits(32n, P) == c : Bool}) -> {G.root_le_fin(~U32, ~I.u32_op, ~I.u32_is, n, G.fits(U32, Bool.not(c), of(P))) == Nat.is_le(P, v(n)) : Bool}:
1116  match c:
1117    case True{}:
1118      lev(of(P), n, P, v(n), LW.vo(P, hc), {==})
1119    case False{}:
1120      +h1 = L.subst(Nat, z => {C.fits(z, P) == False{} : Bool}, 32n, K, Equal.sym(Nat, K, 32n, hK), hc)
1121      +h2 = Equal.trans(Bool, Nat.is_lt(P, C.pow2(K)), C.fits(K, P), False{}, Equal.sym(Bool, C.fits(K, P), Nat.is_lt(P, C.pow2(K)), WW.fits_lt(K, P)), h1)
1122      +hn = N.lt_le_trans(v(n), C.pow2(K), P, U32P.val_lt(1n, {==}, K, hK, n), N.not_lt_le(P, C.pow2(K), h2))
1123      Equal.sym(Bool, Nat.is_le(P, v(n)), False{}, N.lt_not_le(v(n), P, hn))