[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 array-list
enrich
   array-copy
with
   

   
   constants  [] : array;
   functions  . + . : elem × array → array;
              . .first : array → elem;
              . .rest : array → array;
   predicates  . < . : array × array;
   
   variables  ar : array;
              ar0 : array;
              ar1 : array;
              ar2 : array;
              ar3 : array;
              ar4 : array;
              ar5 : array;
              ar6 : array;
              ar7 : array;
              ar8 : array;
              ar9 : array;
              ar10 : array;
   
   

   

   axioms nil :  ⊦ [] = mkarray(0);
          cons :  ⊦ a + ar = copy(ar, 0, mkarray(# ar + 1), 1, # ar)[0, a];
          first :  ⊦ ar.first = ar[0];
          rest :  ⊦ ar.rest = subarray(ar, 1, # ar - 1);
          postfix :  ⊦ ar0 < ar1 ↔ # ar0 < # ar1 ∧ ar0 = subarray(ar1, # ar1 - # ar0, # ar0);

   

   
end enrich