This is a listing of all goals defined over the current specification. Axioms are yellow, proof obligations purple and theorems green. Click on individual names to get more information on the proof.
| Name: | Sequent: | Type: |
|---|---|---|
| rtc | ⊦ Pelem ^*(a, b) ↔ (∃ n. rtc(n, Pelem)(a, b)) | An Axiom |
| rtc-base | ⊦ rtc(0, Pelem)(a, b) ↔ a = b | An Axiom |
| rtc-rec | ⊦ rtc(n + 1, Pelem)(a, b) ↔ (∃ c. Pelem(a, c) ∧ rtc(n, Pelem)(c, b)) | An Axiom |
| rtc-last | ⊦ n ≠ 0 → (rtc(n, Pelem)(a, b) ↔ (∃ c. rtc(n - 1, Pelem)(a, c) ∧ Pelem(c, b))) | A User Theorem |
| rtc-one | ⊦ Pelem(a, b) → (¬ Pelem ^*(a, b) ↔ false) | A User Theorem |
| rtc-refl | ⊦ Pelem ^*(a, a) | A User Theorem |
| rtc-trans | ⊦ Pelem ^*(a, b) ∧ Pelem ^*(b, c) → Pelem ^*(a, c) | A User Theorem |
| rtc1 | ⊦ rtc(1, Pelem)(a, b) ↔ Pelem(a, b) | A User Theorem |