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: |
|---|---|---|
| path-base | ⊦ ¬ path([]) | An Axiom |
| path-one | ⊦ path(a ') | An Axiom |
| path-rec | ⊦ path(x + a ' + b ') ↔ b ∈ succ(a) ∧ path(x + a ') | An Axiom |
| reachset-def | ⊦ reachS(a, S, n) ↔ (∀ b. b ∈ S → reach(a, b, n) ∧ ¬ reach<(a, b, n)) | An Axiom |
| reachls-def | ⊦ reach<(a, b, n) ↔ (∃ m. m < n ∧ reach(a, b, m)) | An Axiom |
| reach-succ | ⊦ reach(a, b, n + 1) ↔ (∃ c. reach(a, c, n) ∧ b ∈ succ(c)) | An Axiom |
| reach-zero | ⊦ reach(a, b, 0) ↔ a = b | An Axiom |
| path-equiv-reach | ⊦ reach(a, b, n) ↔ (∃ x. path(x) ∧ # x = n + 1 ∧ x .first = a ∧ x .last = b) | A User Theorem |
| path-two | ⊦ path(a ' + b ') ↔ b ∈ succ(a) | A User Theorem |
| reach-one | ⊦ reach(a, b, 1) ↔ b ∈ succ(a) | A User Theorem |
| reach-rec-rev | ⊦ reach(a, b, n + 1) → (∃ c. c ∈ succ(a) ∧ reach(c, b, n)) | A User Theorem |
| reach-trans | ⊦ reach(a, b, n) ∧ reach(b, c, m) → (¬ reach(a, c, m + n) ↔ false) | A User Theorem |
| reachless-edge | ⊦ b ∈ succ(a) ∧ reach<(source, a, n0) → (¬ reach<(source, b, n0 + 1) ↔ false) | A User Theorem |
| reachless-next | ⊦ reach<(a, b, n + 1) → (¬ reach<(a, b, n + 2) ↔ false) | A User Theorem |
| reachless-one | ⊦ reach<(source, b, 1) ↔ source = b | A User Theorem |
| reachless-succ | ⊦ reach(a, b, n) → (¬ reach<(a, b, n + 1) ↔ false) | A User Theorem |
| reachless-succ-edge | ⊦ b ∈ succ(a) ∧ reach(source, a, n0) → (¬ reach<(source, b, n0 + 2) ↔ false) | A User Theorem |
| reachless-zero | ⊦ ¬ reach<(source, b, 0) | A User Theorem |
| reachset-del | ⊦ reachS(a, S, n) → (¬ reachS(a, S -- b, n) ↔ false) | A User Theorem |
| reachset-emptyset | ⊦ reachS(a, ∅, n) | A User Theorem |
| reachset-fw | ⊦ b ∈ S ∧ reachS(a, S, n) → reach(a, b, n) | A User Theorem |
| reachset-mem-reach | ⊦ reachS(a, S, n) ∧ b ∈ S → (¬ reach(a, b, n) ↔ false) | A User Theorem |
| reachset-one | ⊦ reachS(a, ∅ ++ b, n) ↔ ¬ ¬ (reach(a, b, n) ∧ ¬ reach<(a, b, n)) | A User Theorem |