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 | ⊦ p*(a, b) ↔ (∃ n. rtc(n, a, b)) | An Axiom |
| rtc+ | ⊦ p+(a, b) ↔ (∃ n. n ≠ 0 ∧ rtc(n, a, b)) | An Axiom |
| rtc-base | ⊦ rtc(0, a, b) ↔ a = b | An Axiom |
| rtc-rec | ⊦ rtc(n + 1, a, b) ↔ (∃ c. p(a, c) ∧ rtc(n, c, b)) | An Axiom |
| inv | ⊦ inv(a, Pelem) ↔ (∀ b. p*(a, b) → Pelem(b)) | An Axiom |
| inv-propagate | Pelem(a), ∀ a, b. Pelem(a) ∧ p(a, b) → Pelem(b) ⊦ inv(a, Pelem) | A User Theorem |
| invx | ⊦ inv(a, Pelem) ∧ p*(a, b) → Pelem(b) | A User Theorem |
| rtc+-unfold | ⊦ p+(a, b) ↔ (∃ c. p(a, c) ∧ p*(c, b)) | A User Theorem |
| rtc+-unfold-last | ⊦ p+(a, b) ↔ (∃ c. p*(a, c) ∧ p(c, b)) | A User Theorem |
| rtc-is-base | ⊦ rtc(0, a, a) | A User Theorem |
| rtc-last | ⊦ n ≠ 0 → (rtc(n, a, b) ↔ (∃ c. rtc(n - 1, a, c) ∧ p(c, b))) | A User Theorem |
| rtc-one | ⊦ p(a, b) → (¬ p*(a, b) ↔ false) | A User Theorem |
| rtc-refl | ⊦ p*(a, a) | A User Theorem |
| rtc-star | ⊦ rtc(n, a, b) → (¬ p*(a, b) ↔ false) | A User Theorem |
| rtc-trans | ⊦ p*(a, b) ∧ p*(b, c) → p*(a, c) | A User Theorem |
| rtc-unfold | ⊦ p*(a, b) ↔ a = b ∨ p+(a, b) | A User Theorem |
| rtc1 | ⊦ rtc(1, a, b) ↔ p(a, b) | A User Theorem |