~/jendhub

def upper_lt

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/array.bend:157

import bend-collections-laws-crypto@1.0.0.0/proofs/lib/array.bend as Array
import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as SC
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA

157def upper_lt(+j: Nat, +p: Nat, +hj: {Nat.is_lt(j, SC.pow2(1n+p)) == True{} : Bool}, +le: {Nat.is_le(SC.pow2(p), j) == True{} : Bool}) -> {Nat.is_lt(Nat.sub(j, SC.pow2(p)), SC.pow2(p)) == True{} : Bool}:
158  N.sub_lt(j, SC.pow2(p), SC.pow2(p), le, L.subst(Nat, n => {Nat.is_lt(j, n) == True{} : Bool}, Nat.double(SC.pow2(p)), Nat.add(SC.pow2(p), SC.pow2(p)), NA.double_self(SC.pow2(p)), hj))

Uses (11)

Used by (3)