def two_limb_lt

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

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

206# r < 2^k, x < 2^j: r + shift(k, x) < 2^(k + j)
207def two_limb_lt(+k: Nat, +j: Nat, +r: Nat, +x: Nat, +hr: {Nat.is_lt(r, C.pow2(k)) == True{} : Bool}, +hx: {Nat.is_lt(x, C.pow2(j)) == True{} : Bool}) -> {Nat.is_lt(Nat.add(r, C.shift(k, x)), C.pow2(Nat.add(k, j))) == True{} : Bool}:
208  +h1 = N.lt_add_r2(r, C.pow2(k), C.shift(k, x), hr)
209  +e1 = Equal.trans(Nat, Nat.add(C.pow2(k), C.shift(k, x)), Nat.add(C.shift(k, 1n), C.shift(k, x)), C.shift(k, 1n+x), Equal.cong(Nat, Nat, t => Nat.add(t, C.shift(k, x)), C.pow2(k), C.shift(k, 1n), Equal.sym(Nat, C.shift(k, 1n), C.pow2(k), shift_one(k))), Equal.sym(Nat, C.shift(k, Nat.add(1n, x)), Nat.add(C.shift(k, 1n), C.shift(k, x)), shift_add(k, 1n, x)))
210  +h2 = L.subst(Nat, z => {Nat.is_lt(Nat.add(r, C.shift(k, x)), z) == True{} : Bool}, Nat.add(C.pow2(k), C.shift(k, x)), C.shift(k, 1n+x), e1, h1)
211  +h3 = shift_mono(k, 1n+x, C.pow2(j), N.lt_succ_le_succ(x, C.pow2(j), hx))
212  N.lt_le_trans(Nat.add(r, C.shift(k, x)), C.shift(k, 1n+x), C.pow2(Nat.add(k, j)), h2, L.subst(Nat, z => {Nat.is_le(C.shift(k, 1n+x), z) == True{} : Bool}, C.shift(k, C.pow2(j)), C.pow2(Nat.add(k, j)), shift_pow2(k, j), h3))