ProofU32.uq.lt_succ_pw: def of bend-osdev-algo@0.1.0.0
Import: import bend-osdev-algo@0.1.0.0/proof_u32.bend as ProofU32
Lines 198-203 of bend-osdev-algo@0.1.0.0/proof_u32.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-algo@0.1.0.0/proof_u32.bend&start_line=198&end_line=203

import Base

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

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_u32.bend&name=uq.lt_dbl_self
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_u32.bend&name=uq.pw