Specification wolist

[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-perm, 
   gen-weakord
with
   functions 
       ins≤ : weakord × list(weakord) → list(weakord);
       merge : list(weakord) × list(weakord) → list(weakord);
   
   predicates 
       ordered≤ : list(weakord);
       ordered< : list(weakord);
   
   variables 
       x : list(weakord);
       y : list(weakord);
       z : list(weakord);
       a : weakord;
       b : weakord;
       c : weakord;
       n : nat;
       m : 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 enrich