[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 oarray-perm
enrich
   oarray-sorted
, 
   obag
with
   

   
   
   
   predicates  perm : array × array;
   
   
   partial functions  mkbag : array × nat → bag with λ A, n. n ≤ # A;
   

   

   axioms perm :  ⊦ perm(A, A0) ↔ mkbag(A, # A) = mkbag(A0, # A0);
          used for: ls;
          mkbag-base :  ⊦ mkbag(A, 0) = ∅;
          used for: ls;
          mkbag-rec :  ⊦ mkbag(A, n + 1) = mkbag(A, n) ++ A[n];
          used for: ls;

   

   
end enrich