def lift_pair_observation

stelliferous@0.0.2.0 · proofs/storage_refinement.bend:483

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

483def lift_pair_observation(~Element: Data,~Context: Data,
484  ~Proposition: Context -> @-input: Array<Element> -> @-output: Array<Element> ->
485    @-input_tree: Tree.Tree<Element> -> @-output_tree: Tree.Tree<Element> -> Type,
486  +context: Context,-input: Array<Element>,-output: Array<Element>,
487  input_observation: Observation<Element,input>,output_observation: Observation<Element,output>,
488  canonical: @+input_tree: Tree.Tree<Element> -> @+output_tree: Tree.Tree<Element> ->
489    Proposition(context,Tree.pack(Element,input_tree),Tree.pack(Element,output_tree),input_tree,output_tree)) ->
490  Proposition(context,input,output,Tree.reflect(Element,input),Tree.reflect(Element,output)):
491  Observation{+input_tree,input_packed,input_reflected} = input_observation
492  Observation{+output_tree,output_packed,output_reflected} = output_observation
493  %input_reflected : Proposition(context,input,output,_,Tree.reflect(Element,output))
494  %output_reflected : Proposition(context,input,output,input_tree,_)
495  %input_packed : Proposition(context,_,output,input_tree,output_tree)
496  %output_packed : Proposition(context,Tree.pack(Element,input_tree),_,input_tree,output_tree)
497  canonical(input_tree)(output_tree)