[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 suffix-array
enrich suffix-array-base
 , 
       suffix with
   functions 
      bag< . : nat → bag;
   predicates 
      valid : suffixarray × array;
   
   axioms 
      valid :  ⊦ valid(sar, ar) ↔ sar .elems = bag< # ar ∧ (∀ n0, n1. n0 < # sar ∧ n1 < # sar → (suffix(ar, sar[n0]) < suffix(ar, sar[n1]) ↔ n0 < n1));
      used for : ls;
       
      bagle-base :  ⊦ bag< 0 = ∅;
      used for : s, ls;
       
      bagle-rec :  ⊦ bag< (n + 1) = bag< n ++ n;
      used for : s, ls;
       
end enrich