Proof step 66 from proof INVR-step (previous step)

User applied rule case distinction

And obtained the following new goals

• Proof step 61:

  reachS(source, N, n + 1), reachS(source, C, n), reach(source, dest, n1 + n), v ∈ C, ∀ a0. a0 = v ∨ ¬ a0 ∈ C ∨ ¬ reach(a0, dest, n1) ∨ reach<(a0, dest, n1), n1 = 0 ∨ (∀ b. ¬ b ∈ N ∪ (succ(v) \ V) ∨ ¬ reach(b, dest, n1 - 1) ∨ reach<(b, dest, n1 - 1)) ⊦ ¬ a ∈ C ∨ ¬ reach(a, dest, n1) ∨ reach<(a, dest, n1), C = ∅, v = dest, # C = 0, reach<(source, dest, n1 + n), ∃ b0. ¬ ((∃ c. reach(source, c, n) ∧ b0 ∈ succ(c)) ∧ ¬ reach<(source, b0, n + 1) → b0 ∈ N ∨ (∃ a. a ∈ C ∧ b0 ∈ succ(a) ∧ ¬ b0 ∈ V)), ∃ b0. ¬ (b0 ∈ V ↔ reach<(source, b0, n + 1) ∨ (∃ a0. b0 ∈ succ(a0) ∧ reach(source, a0, n) ∧ ¬ reach<(source, a0, n) ∧ ¬ a0 ∈ C))

• Proof step 65:

  reachS(source, N, n + 1), reachS(source, C, n), reach(source, dest, n1 + n), v ∈ C, ∀ a0. a0 = v ∨ ¬ a0 ∈ C ∨ ¬ reach(a0, dest, n1) ∨ reach<(a0, dest, n1), n1 = 0 ∨ (∀ b. ¬ b ∈ N ∪ (succ(v) \ V) ∨ ¬ reach(b, dest, n1 - 1) ∨ reach<(b, dest, n1 - 1)) ⊦ n1 = 0 ∨ ¬ b ∈ N ∨ ¬ reach(b, dest, n1 - 1) ∨ reach<(b, dest, n1 - 1), C = ∅, v = dest, # C = 0, reach<(source, dest, n1 + n), ∃ b0. ¬ ((∃ c. reach(source, c, n) ∧ b0 ∈ succ(c)) ∧ ¬ reach<(source, b0, n + 1) → b0 ∈ N ∨ (∃ a. a ∈ C ∧ b0 ∈ succ(a) ∧ ¬ b0 ∈ V)), ∃ b0. ¬ (b0 ∈ V ↔ reach<(source, b0, n + 1) ∨ (∃ a0. b0 ∈ succ(a0) ∧ reach(source, a0, n) ∧ ¬ reach<(source, a0, n) ∧ ¬ a0 ∈ C))

Rule argument

Additional information

[[CONCRETESIMPRULES : ()]]