~/jendhub

def cap_succ

bend-ml-tensor-array@0.1.19.0 · main.bend:706

import bend-ml-tensor-array@0.1.19.0/main.bend as BendMlTensorArray
import Base

706def cap_succ(+m: Nat, ih: {snd_nat(cap_pair(m)) == pow2(fst_nat(cap_pair(m))) : Nat} & {True{} == leb(m, snd_nat(cap_pair(m))) : Bool}) -> {snd_nat(cap_pair(1n+m)) == pow2(fst_nat(cap_pair(1n+m))) : Nat} & {True{} == leb(1n+m, snd_nat(cap_pair(1n+m))) : Bool}:
707  match ih:
708    case Tuple{i1, i2}:
709      step_pair_ok(m, cap_pair(m), i1, i2)

Uses (10)

Used by (1)