[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 ordered-set
enrich
   oset
with
   comment: ordered sets with insertion and deletion of the minimum;

   
   
   
   
   procedures ordered_set_insert elem : set nonfunctional ;
              ordered_set_delete_min  : elem, set nonfunctional ;
   

   

   

   

   declaration ordered_set_delete_min : ordered_set_delete_min(; a, s){a := s.min, s := s.butmin};
                : ordered_set_insert(a; s){s := s ++ a};
end enrich