Specification rtc-rel

[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,

enrich
   nat, 
   elem-rel
with
   predicates 
       p* : Elem × Elem;
       p+ : Elem × Elem;
       rtc : Nat × Elem × Elem;
       inv : Elem × (Elem → Bool);
   
   variables 
       pelem : Elem → Bool;
   
   axioms 
      rtc: p*(a, b) ↔ (∃ n. rtc(n, a, b));
      
      rtc+: p+(a, b) ↔ (∃ n. n ≠ 0 ∧ rtc(n, a, b));
      
      rtc-base: rtc(0, a, b) ↔ a = b;
      used for: ls;
      
      rtc-rec: rtc(n + 1, a, b) ↔ (∃ c. p(a, c) ∧ rtc(n, c, b));
      used for: ls;
      
      inv: inv(a, pelem) ↔ (∀ b. p*(a, b) → pelem(b));
   
   
end enrich