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: |
|---|---|---|
| INV-def | ⊦ INV(C, N, V, n, source) ↔ ¬ ¬ ( (∀ b. b ∈ V ↔ reach<(source, b, n + 1) ∨ (∃ a. b ∈ succ(a) ∧ reachS(source, {a} , n) ∧ ¬ a ∈ C)) ∧ reachS(source, C, n) ∧ reachS(source, N, n + 1) ∧ (∀ b. reachS(source, {b} , n + 1) → b ∈ N ∨ (∃ a. a ∈ C ∧ b ∈ succ(a) ∧ ¬ b ∈ V))) | An Axiom |
| INVR-def | ⊦ INVR(C, N, V, n, n0, source, dest) ↔ ¬ ¬ ( reach(source, dest, n0) ∧ ¬ reach<(source, dest, n0) ∧ n ≤ n0 ∧ ((∃ a. a ∈ C ∧ reachS(a, {dest} , n0 - n)) ∨ n < n0 ∧ (∃ b. b ∈ N ∧ reachS(b, {dest} , n0 - n - 1)))) | An Axiom |
| INV-init | ⊦ INV(∅ ++ source, ∅, ∅ ++ source, 0, source) | A User Theorem |
| INV-nextlevel | ⊦ INV(∅, N, V, n, source) → (¬ INV(N, ∅, V, n + 1, source) ↔ false) | A User Theorem |
| INV-step | ⊦ INV(C, N, V, n, source) ∧ v ∈ C → (¬ INV(C -- v, N ∪ (succ(v) \ V), V ∪ succ(v), n, source) ↔ false) | A User Theorem |
| INVR-init | ⊦ reach(source, dest, n0) ∧ ¬ reach<(source, dest, n0) → (¬ INVR(∅ ++ source, ∅, ∅ ++ source, 0, n0, source, dest) ↔ false) | A User Theorem |
| INVR-nextlevel | ⊦ INVR(∅, N, V, n, n0, source, dest) ∧ INV(∅, N, V, n, source) → (¬ INVR(N, ∅, V, n + 1, n0, source, dest) ↔ false) | A User Theorem |
| INVR-step | ⊦ INVR(C, N, V, n, n0, source, dest) ∧ INV(C, N, V, n, source) ∧ v ∈ C ∧ v ≠ dest → (¬ INVR(C -- v, N ∪ (succ(v) \ V), V ∪ succ(v), n, n0, source, dest) ↔ false) | A User Theorem |