[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 olist
specification
   using olist-act
   functions 
       ins≤ : elem × list → list;
       merge : list × list → list;
   
   predicates 
       ordered≤ : list;
       ordered< : list;
   
   variables 
       x : list;
       y : list;
       z : list;
       a : elem;
       b : elem;
       c : elem;
       n : nat;
   
   
   axioms 
      le-e: ordered≤([]);
      used for: s, ls;
      
      le-o: ordered≤(a ');
      used for: s, ls;
      
      le-r: ordered≤(a ' + b ' + x) ↔ ¬ b < a ∧ ordered≤(b ' + x);
      used for: ws, lws;
      
      ls-e: ordered<([]);
      used for: s, ls;
      
      ls-o: ordered<(a ');
      used for: s, ls;
      
      ls-r: ordered<(a ' + b ' + x) ↔ a < b ∧ ordered<(b ' + x);
      used for: ws, lws;
      
      ins-e: ins≤(a, []) = a ';
      used for: s, ls;
      
      ins-y: ¬ b < a → ins≤(a, b ' + x) = a + b + x;
      used for: s, ls;
      
      ins-n: b < a → ins≤(a, b ' + x) = b + ins≤(a, x);
      used for: s, ls, lc;
      
      merge-empty: merge([], x) = x;
      used for: s, ls;
      
      merge-rec: merge(a ' + x0, x) = ins≤(a, merge(x0, x));
      used for: s, ls;
   
   
end specification