def same_capacity

stelliferous@0.0.2.0 · proofs/storage_shape.bend:94

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

94# Balanced trees at the same depth expose the same native capacity.
95def same_capacity(-Element: Data,+depth: Nat,+left: Tree.Tree<Element>,+right: Tree.Tree<Element>,
96  left_balanced: Balanced(Element,depth,left),right_balanced: Balanced(Element,depth,right)) ->
97  {Tree.capacity(Element,left) == Tree.capacity(Element,right) : U32}:
98  Equal.trans(U32,Tree.capacity(Element,left),U32.shln(1,depth),Tree.capacity(Element,right),capacity(Element,depth,left,left_balanced),
99    Equal.sym(U32,Tree.capacity(Element,right),U32.shln(1,depth),capacity(Element,depth,right,right_balanced)))