[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 erasequeue
enrich
   erasequeue-base
, 
   valid-peb, 
   lebrefset
with
   

   
   
   functions  . - . : queue × nat → queue prio 8 left;
              . - . : queue × lebref → queue prio 8 left;
              . - . : queue × volid → queue prio 8 left;
              . .lebrefs : queue → lebrefset;
   predicates  . ∈ . : nat × queue;
               . ∈ . : lebref × queue;
               . ∈ . : volid × queue;
   
   
   
   

   

   axioms queue-in :  ⊦ n ∈ q ↔ (∃ eqent. eqent.pnum = n ∧ eqent ∈ q);
          used for: ls;
          queue-in-vl :  ⊦ lref ∈ q ↔ (∃ n. eq-entry(n, lref) ∈ q);
          used for: ls;
          queue-in-v :  ⊦ v ∈ q ↔ (∃ n, m. eq-entry(n, v × m) ∈ q);
          used for: ls;
          queue-rm-base :  ⊦ [] - n = [];
          used for: s, ls;
          queue-rm-rec :  ⊦ eqent ' + q - n = (eqent.pnum = n ⊃ [];eqent ') + (q - n);
          used for: ls;
          queue-rm-vl-base :  ⊦ [] - lref = [];
          used for: s, ls;
          queue-rm-vl-rec :  ⊦ eqent ' + q - lref = (eqent.lebref = lref ⊃ q - lref;eqent ' + (q - lref));
          used for: ls;
          queue-rm-v-base :  ⊦ [] - v = [];
          used for: s, ls;
          queue-rm-v-rec :  ⊦ eqent ' + q - v = (eqent.lebref ≠ none ∧ eqent.lebref.vol = v ⊃ q - v;eqent ' + (q - v));
          used for: ls;
          lebrefs-base :  ⊦ [].lebrefs = ∅;
          used for: s, ls;
          lebrefs-rec :  ⊦ (eqent ' + q).lebrefs = q.lebrefs ∪ (eqent.lebref ≠ none ⊃ {eqent.lebref} ;∅);
          used for: s, ls;

   

   
end enrich