StorageShape.capacity: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/storage_shape.bend as StorageShape
Lines 70-79 of stelliferous@0.0.2.0/proofs/storage_shape.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/storage_shape.bend&start_line=70&end_line=79

import Base
import stelliferous@0.0.2.0/proofs/storage_tree_model.bend as Tree

def capacity(-Element: Data,+depth: Nat,+tree: Tree.Tree<Element>,balanced: Balanced(Element,depth,tree)) ->
  {Tree.capacity(Element,tree) == U32.shln(1,depth) : U32}:
  match depth tree:
    case 0n Tree.Leaf{value}: {==}
    case 0n Tree.Node{left,right}: match balanced:
    case 1n+rest Tree.Leaf{value}: match balanced:
    case 1n+ +rest Tree.Node{+left,+right}:
      Both{left_balanced,right_balanced} = balanced
      %capacity(Element,rest,left,left_balanced) : {U32.shl(Tree.capacity(Element,left)) == U32.shl(_) : U32}
      {==}

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.shl
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.shln
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_shape.bend&name=Balanced
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_shape.bend&name=Both
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_tree_model.bend&name=Tree
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_tree_model.bend&name=capacity