def transfer_room

stelliferous@0.0.2.0 · proofs/storage_shape.bend:101

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

101def transfer_room(-Element: Data,+depth: Nat,+left: Tree.Tree<Element>,+right: Tree.Tree<Element>,+count: Nat,
102  left_balanced: Balanced(Element,depth,left),right_balanced: Balanced(Element,depth,right),room: {Nat.is_le(count,U32.to_nat(Tree.capacity(Element,left))) == True{} : Bool}) ->
103  {Nat.is_le(count,U32.to_nat(Tree.capacity(Element,right))) == True{} : Bool}:
104  %same_capacity(Element,depth,left,right,left_balanced,right_balanced) : {Nat.is_le(count,U32.to_nat(_)) == True{} : Bool}
105  room