def fresh_equation

stelliferous@0.0.2.0 · proofs/storage_certificate.bend:74

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

74def fresh_equation(-Element: Data,+depth: Nat,value: Element) ->
75  {Array.new(Element,depth,value) == Tree.pack(Element,normalized(Element,depth,Tree.reflect(Element,Array.new(Element,depth,value)))) : Array<Element>}:
76  %restored(Element,depth,Array.new(Element,depth,value),Witness.fresh(Element,depth,value)) :
77    {_ == Tree.pack(Element,normalized(Element,depth,Tree.reflect(Element,Array.new(Element,depth,value)))) : Array<Element>}
78  {==}