[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
   set-union
, 
   cuckoo
with
   
   constants  SIZE : nat;
   functions  abs : table × table × (elem → nat) × (elem → nat) → set;
   predicates  inv : table × (elem → nat);
               disj : table × table;
   
   variables  h : elem → nat;

   

   axioms inv :  ⊦ inv(T, h) ↔ # T = SIZE ∧ (∀ a. h(a) < SIZE) ∧ (∀ n, a. n < # T ∧ T[n] = full(a) → h(a) = n);
          in-abs :  ⊦ a ∈ abs(T1, T2, h1, h2) ↔ ¬ ¬(T1[h1(a)] = full(a) ∨ T2[h2(a)] = full(a));
          disj :  ⊦ disj(T1, T2) ↔ (∀ n, m. n < # T1 ∧ m < # T2 ∧ T1[n] ≠ empty ∧ T2[m] ≠ empty → T1[n].elem ≠ T2[m].elem)

   

   
end enrich