~/jendhub

def dbl_final

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

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

730def dbl_final(n: Nat, pr: {snd_nat(cap_dbl(n, Nat.is_le(n, 1n), n, 0n, 1n)) == pow2(fst_nat(cap_dbl(n, Nat.is_le(n, 1n), n, 0n, 1n))) : Nat} & {True{} == leb(n, snd_nat(cap_dbl(n, Nat.is_le(n, 1n), n, 0n, 1n))) : Bool}) -> {True{} == leb(n, pow2(cap_depth(n))) : Bool}:
731  match pr:
732    case Tuple{i1, i2}:
733      %i1 : {True{} == leb(n, _) : Bool}
734      i2

Uses (11)

Used by (1)