[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 order
generic specification 
   parameter elem
    target 
         predicates 
            reflexive : (elem × elem → bool);
            transitive : (elem × elem → bool);
            total : (elem × elem → bool);
         variables 
            R : elem × elem → bool; 
         
         axioms 
            reflexive :  ⊦ reflexive(R) ↔ (∀ a. R(a, a));
            used for : ls;
             
            transitive :  ⊦ transitive(R) ↔ (∀ a, b, c. R(a, b) ∧ R(b, c) → R(a, c));
            used for : ls;
             
            total :  ⊦ total(R) ↔ (∀ a, b. R(a, b) ∨ R(b, a) ∨ a = b);
            used for : ls;
             
   
end generic specification