def capacity

stelliferous@0.0.2.0 · proofs/storage_shape.bend:70

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

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