[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 natset
specification
   using actualize
            set-union
         with
            nat
            
         by morphism
            :Elem → Nat; 
            :Set → Natset; 
            ∅ → ∅; 
             . ++ .  →  . ++ . ; 
            # .  → # . ; 
            { . } → { . }; 
             . ∪ .  →  . ∪ . ; 
             . ∩ .  →  . ∩ . ; 
             . \ .  →  . \ . ; 
             . -- .  →  . -- . ; 
             . ∈ .  →  . ∈ . ; 
             . ⊆ .  →  . ⊆ . ; 
            disjoint → disjoint; 
         end actualize
   functions 
       . to . : Nat × Nat → Natset prio 7 right;
   
   variables 
       m : Nat;
       n : Nat;
       ns : Natset;
   
   axioms 
      range-def: n0 ∈ m to n ↔ m ≤ n0 ∧ n0 < n;
      used for: s, ls;
   
   
end specification