[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 abs
enrich
   hashset-preds, 
   set-basic
with
   predicates 
       absset : Array(Elem) × Set(Elem);
   
   variables 
       e : Elem;
       set : Set(Elem);
       n : Nat;
       ar : Array(Elem);
       b : Bool;
   
   
   axioms 
      absset-def: absset(ar, set) ↔ (∀ e. e ∈ set ↔ (∃ n. n < # ar ∧ e = ar[n] ∧ e ≠ ⊥));
      used for: ls;
   
   
end enrich