Specification wellfounded

[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
   

   sorts elem;
   
   
   predicates  . ≪ . : elem × elem;
   
   variables  IHP : elem → bool;
              a : elem;
              a0 : elem;
              a1 : elem;
   
   

   

   axioms trans :  ⊦ a ≪ a0 ∧ a0 ≪ a1 → a ≪ a1;
          used for: lf, f;
          wellfounded : ∀ a. (∀ a0. a0 ≪ a → IHP(a0)) → IHP(a) ⊦ IHP(a);

   

   
end specification