[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 lrs
enrich lcp
 , 
       suffix-array with
   predicates 
      rs : array × nat × nat × nat;
      lrs : array × nat × nat × nat;
   variables 
      m1 : nat; 
   
   axioms 
      rs :  ⊦ rs(ar, n0, n1, n) ↔ ¬ ¬ (n0 ≠ n1 ∧ n0 < # ar ∧ n1 ≤ # ar ∧ lcp(ar, n0, n1) = n);
      used for : s, ls;
       
      lrs :  ⊦ lrs(ar, n0, n1, n) ↔ ¬ ¬ (rs(ar, n0, n1, n) ∧ (∀ m0, m1, m. rs(ar, m0, m1, m) → m ≤ n));
      used for : s, ls;
       
end enrich