def pack_reflected

stelliferous@0.0.2.0 · proofs/storage_refinement.bend:24

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

24def pack_reflected(-Element: Data,storage: Array<Element>) ->
25  {Tree.pack(Element,Tree.reflect(Element,storage)) == storage : Array<Element>}:
26  match storage:
27    case ALeaf{value}: {==}
28    case ANode{left,right}:
29      %pack_reflected(Element,left) :
30        {ANode{Tree.pack(Element,Tree.reflect(Element,left)),Tree.pack(Element,Tree.reflect(Element,right))} == ANode{_,right} : Array<Element>}
31      %pack_reflected(Element,right) :
32        {ANode{Tree.pack(Element,Tree.reflect(Element,left)),Tree.pack(Element,Tree.reflect(Element,right))} == ANode{Tree.pack(Element,Tree.reflect(Element,left)),_} : Array<Element>}
33      {==}