~/jendhub

def uq.lt_succ_pw

bend-osdev-algo@0.1.0.0 · proof_u32.bend:198

import bend-osdev-algo@0.1.0.0/proof_u32.bend as ProofU32
import Base

198# x < 2^f: x2 < 2^g, for x == x2 and g == 1 + f (stated so that a fixed g,
199# such as the search's 33, is never expanded)
200def uq.lt_succ_pw(+f: Nat, -g: Nat, eg: {1n+f == g : Nat}, +x: Nat, -x2: Nat, e: {x == x2 : Nat}, h: {Nat.is_lt(x, uq.pw(f)) == True{} : Bool}) -> {Nat.is_lt(x2, uq.pw(g)) == True{} : Bool}:
201  %eg : {Nat.is_lt(x2, uq.pw(_)) == True{} : Bool}
202  %e : {Nat.is_lt(_, uq.pw(1n+f)) == True{} : Bool}
203  uq.lt_dbl_self(x, uq.pw(f), h)

Uses (5)

Used by (1)