def observed_node
stelliferous@0.0.2.0 · proofs/storage_refinement.bend:460
import stelliferous@0.0.2.0/proofs/storage_refinement.bend as StorageRefinement
import Base
import stelliferous@0.0.2.0/proofs/storage_tree_model.bend as Tree
460def observed_node(-Element: Data,-left: Array<Element>,-right: Array<Element>,
461 left_observation: Observation<Element,left>,right_observation: Observation<Element,right>) -> Observation<Element,ANode{left,right}>:
462 Observation{+left_tree,left_packed,left_reflected} = left_observation
463 Observation{+right_tree,right_packed,right_reflected} = right_observation
464 Observation{Tree.Node{left_tree,right_tree},observed_node_equation(Element,left,right,left_tree,right_tree,left_packed,right_packed),
465 observed_node_reflection(Element,left,right,left_tree,right_tree,left_reflected,right_reflected)}