Specification partial-sorted

[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
   olist
, 
   nat-div

with
   

   
   
   functions  violations : list → nat;
              less# : elem × list → nat;
   predicates  partial-sorted : list × nat × nat;
   
   
   
   

   

   axioms partial-sorted :  ⊦ partial-sorted(x, n, m) ↔ (∀ n0. n + 2 * n0 + 1 < m → ¬ x[n + 2 * n0 + 1] < x[n + 2 * n0]);
          used for: ls;
          violations-base :  ⊦ violations([]) = 0;
          used for: s, ls;
          violations-rec :  ⊦ violations(a ' + x) = less#(a, x) + violations(x);
          used for: s, ls;
          less-base :  ⊦ less#(a, []) = 0;
          used for: s, ls;
          less-rec :  ⊦ less#(a, b ' + x) = (b < a ⊃ 1;0) + less#(a, x);
          used for: s, ls;

   

   
end enrich