def unique_depth

stelliferous@0.0.2.0 · proofs/storage_shape.bend:81

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

81def unique_depth(-Element: Data,tree: Tree.Tree<Element>,left_depth: Nat,right_depth: Nat,
82  left: Balanced(Element,left_depth,tree),right: Balanced(Element,right_depth,tree)) -> {left_depth == right_depth : Nat}:
83  match tree left_depth right_depth:
84    case Tree.Leaf{value} 0n 0n: {==}
85    case Tree.Leaf{value} 0n 1n+right_depth: match right:
86    case Tree.Leaf{value} 1n+left_depth right_depth: match left:
87    case Tree.Node{left_tree,right_tree} 0n right_depth: match left:
88    case Tree.Node{left_tree,right_tree} 1n+left_depth 0n: match right:
89    case Tree.Node{+left_tree,right_tree} 1n+ +left_depth 1n+ +right_depth:
90      Both{left_balanced,left_other} = left
91      Both{right_balanced,right_other} = right
92      Equal.cong(Nat,Nat,depth => 1n+depth,left_depth,right_depth,unique_depth(Element,left_tree,left_depth,right_depth,left_balanced,right_balanced))