[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 oset
enrich
   set-union, 
   gen-tord
with
   predicates 
       . < . : Tord × Set(Tord);
       . < . : Set(Tord) × Tord;
   
   variables 
       s : Set(Tord);
       a : Tord;
       b : Tord;
   
   partial functions 
       . .min : Set(Tord) → Tord with λ s. s ≠ ∅;
       . .butmin : Set(Tord) → Set(Tord) with λ s. s ≠ ∅;
       . .max : Set(Tord) → Tord with λ s. s ≠ ∅;
       . .butmax : Set(Tord) → Set(Tord) with λ s. s ≠ ∅;
   
   
   axioms 
      Min-in: s ≠ ∅ → s.min ∈ s;
      used for: lf;
      
      Min-min: a ∈ s → ¬ a < s.min;
      used for: lf;
      
      Butmin: s ≠ ∅ → s.butmin = s -- s.min;
      used for: ls;
      
      Max-in: s ≠ ∅ → s.max ∈ s;
      used for: lf;
      
      Max-max: a ∈ s → ¬ s.max < a;
      used for: lf;
      
      Butmax: s ≠ ∅ → s.butmax = s -- s.max;
      used for: ls;
      
      Less: a < s ↔ (∀ b. b ∈ s → a < b);
      used for: ls;
      
      Greater: s < a ↔ (∀ b. b ∈ s → b < a);
      used for: ls;
   
   
end enrich