[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 tidset-npset
specification
   

   

   

   using rename
            set-union
         
            
         by morphism
            :elem → Tid; 
            :set → Tidset; 
            ∅ → ∅; 
            ++ → ++; 
            # → #; 
            { } → { }; 
            ∪ → ∪; 
            ∩ → ∩; 
            \ → \; 
            -- → --; 
            ∈ → ∈; 
            ⊆ → ⊆; 
         end rename, 
         sparsearray

   

   

   

   

   
   
   
   predicates  alldisjointp : Tidset × (Tid → sparsearray);
               disjointp : sparsearray × sparsearray;
   
   variables  ts : Tidset;
              f : Tid → sparsearray;
              np : natpair;
              tid : Tid;
              sa : sparsearray;
   partial functions  U : Tidset × (Tid → sparsearray) → sparsearray with alldisjointp;
                      . ∪ . : sparsearray × sparsearray → sparsearray with disjointp;
   

   

   axioms disjointp-def :  ⊦ disjointp(sa1, sa2) ↔ (∀ np. np ∈ sa1 → ¬ np ∈ sa2);
          used for: ls;
          alldisjointp-def :  ⊦ alldisjointp(ts, f) ↔ (∀ tid1, tid2, np. tid1 ∈ ts ∧ tid2 ∈ ts ∧ np ∈ f(tid1) ∧ tid1 ≠ tid2 → ¬ np ∈ f(tid2));
          used for: ls;
          union-def :  ⊦ sa1 ∪ sa2 = sa1 ⊕ sa2;
          used for: ls;
          bigunion-in :  ⊦ alldisjointp(ts, f) → (np ∈ U(ts, f) ↔ (∃ tid. tid ∈ ts ∧ np ∈ f(tid)));
          used for: s, ls;
          bigunion-get :  ⊦ alldisjointp(ts, f) ∧ np ∈ f(tid) → U(ts, f)[np] = f(tid)[np];
          used for: s, ls;

   

   
end specification