StorageShape.transfer_room: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/storage_shape.bend as StorageShape
Lines 101-105 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=101&end_line=105

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

def transfer_room(-Element: Data,+depth: Nat,+left: Tree.Tree<Element>,+right: Tree.Tree<Element>,+count: Nat,
  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}) ->
  {Nat.is_le(count,U32.to_nat(Tree.capacity(Element,right))) == True{} : Bool}:
  %same_capacity(Element,depth,left,right,left_balanced,right_balanced) : {Nat.is_le(count,U32.to_nat(_)) == True{} : Bool}
  room

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  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=same_capacity
  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