Specification list-to-set

[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,

enrich
   list, 
   set-basic
with
   functions 
       { . } : List('s) → Set('s);
   
   variables 
       s : 's;
       sl : List('s);
   
   
   axioms 
      list-to-set-null: {[]}  = ∅;
      
      list-to-set-cons: {s ' + sl}  = {sl}  ++ s;
   
   
end enrich