[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Specification sqns
enrich
   bag-max, 
   valid-peb
with
   

   
   
   functions  valid-sqns : volid × nat × apebs → nat-bag;
              valid-sqns : volid × nat × apebs × nat → nat-bag;
   
   
   
   
   

   

   axioms valid-sqns :  ⊦ valid-sqns(v, m, apebs) = valid-sqns(v, m, apebs, # apebs);
          used for: ls;
          valid-sqns-base :  ⊦ valid-sqns(v, m, apebs, 0) = ∅;
          used for: s, ls;
          valid-sqns-rec
          : ⊦   n < # apebs
              → valid-sqns(v, m, apebs, n + 1) = valid-sqns(v, m, apebs, n) ∪ (valid-peb(v, m, apebs[n]) ⊃ {apebs[n].vidhdr.sqn} ;∅);
          used for: s, ls;

   

   
end enrich