def fresh_certificate

stelliferous@0.0.2.0 · proofs/storage_buffer_model.bend:120

import Base
import stelliferous@0.0.2.0/proofs/storage_tree_model.bend as Tree
import stelliferous@0.0.2.0/proofs/storage_refinement.bend as StorageLaws
import stelliferous@0.0.2.0/proofs/storage_certificate.bend as Certificate

120def fresh_certificate(~Element: Data,+depth: Nat,+fill: Element) -> Certificate.Certificate<Element,Tree.pack(Element,Tree.fresh(Element,depth,fill))>:
121  Certificate.Certificate{depth,
122    %StorageLaws.fresh(Element,depth,fill) : {_ == Tree.pack(Element,Certificate.normalized(Element,depth,Tree.reflect(Element,_))) : Array<Element>}
123    Certificate.fresh_equation(Element,depth,fill)}