[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 arr2list
enrich boolarr , 
       boollist with
   functions 
      arr2list : array × nat → list;
   predicates 
      issorted : array;
      isperm : array × array;
   
   axioms 
      bool-less :  ⊦ bv < bv0 ↔ ¬ ¬ (¬ bv ∧ bv0);
      used for : s, ls;
       
      arr2list-base :  ⊦ 0 ≠ # ar → arr2list(ar, 0) = ar[0] ';
      used for : s, ls;
       
      arr2list-rec :  ⊦ n + 1 < # ar → arr2list(ar, n + 1) = arr2list(ar, n) + ar[n + 1] ';
      used for : s, ls;
       
      issorted-le-all-def :  ⊦ issorted(ar) ↔ (∀ m, n. m ≤ n ∧ n < # ar → ¬ ar[n] < ar[m]);
      used for : s, ls;
       
      isperm-def :  ⊦ isperm(ar0, ar1) ↔ perm(arr2list(ar0, # ar0 - 1), arr2list(ar1, # ar1 - 1));
      used for : s, ls;
       
end enrich