[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