[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