def low_lt

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/width.bend:116

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L

116def low_lt(+k: Nat, +n: Nat) -> {Nat.is_lt(C.low(k, n), C.pow2(k)) == True{} : Bool}:
117  match k:
118    case 0n:
119      {==}
120    case 1n+ +p:
121      +l = C.low(p, C.half(n))
122      +ih = low_lt(p, C.half(n))
123      +b = C.bit(n)
124      +hb1 = bit_le1(n)
125      +h2 = N.lt_succ_le_succ(l, C.pow2(p), ih)
126      +h3 = N.double_le(1n+l, C.pow2(p), h2)
127      +h4 = L.subst(Nat, z => {Nat.is_le(z, Nat.double(C.pow2(p))) == True{} : Bool}, Nat.double(1n+l), Nat.add(2n, Nat.double(l)), N.double_succ(l), h3)
128      +h5 = N.le_lt_trans(Nat.add(b, Nat.double(l)), Nat.add(1n, Nat.double(l)), Nat.add(2n, Nat.double(l)), le_add_r(b, 1n, Nat.double(l), hb1), N.lt_succ(1n+Nat.double(l)))
129      N.lt_le_trans(Nat.add(b, Nat.double(l)), Nat.add(2n, Nat.double(l)), Nat.double(C.pow2(p)), h5, h4)