Proof step 1 from proof hpal-reachset-set (conclusion) (back to tree)

User applied rule induction

And obtained the following new goals

• Proof step 2:

  finout(g), ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ s0. ∀ b. (∃ a. a ∈ s ∧ path(g)(a, b)) ↔ b ∈ s0

Rule argument

Additional information

Used simplifier rules: <; (wellfounded) Used terms: # s

Proof step 2 from proof hpal-reachset-set (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ s0. ∀ b. (∃ a. a ∈ s ∧ path(g)(a, b)) ↔ b ∈ s0

Rule argument

Additional information

Used simplifier rules: finout-def: ⊦ finout(g) ↔ (∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s);

Proof step 3 from proof hpal-reachset-set (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 4:

  ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∃ a. a ∈ s, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ s0. ∀ b. (∃ a. a ∈ s ∧ path(g)(a, b)) ↔ b ∈ s0

• Proof step 102:

  ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ s0. ∀ b. (∃ a. a ∈ s ∧ path(g)(a, b)) ↔ b ∈ s0, ∃ a. a ∈ s

Rule argument

Additional information

Used formulas: ∃ a. a ∈ s

Proof step 4 from proof hpal-reachset-set (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  # s ≠ 0, s ≠ ∅, a ∈ s, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ s0. ∀ b. (∃ a. a ∈ s ∧ path(g)(a, b)) ↔ b ∈ s0

Rule argument

Additional information

Used simplifier rules: size-zero-01: ⊦ s ≠ ∅ → # s ≠ 0; (forward) from specification set-basic ne-01: ⊦ a ∈ s → s ≠ ∅; (forward) from specification set-basic

Proof step 5 from proof hpal-reachset-set (previous step) (back to tree)

User applied rule apply induction

And obtained the following new goals

• Proof step 6:

  # s ≠ 0, s ≠ ∅, a ∈ s, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ s0. ∀ b. (∃ a. a ∈ s ∧ path(g)(a, b)) ↔ b ∈ s0, finout(g) ∧ (∀ a0. a0 ∈ s -- a → ¬ haspathanylength(g)(a0))

• Proof step 8:

  # s ≠ 0, s ≠ ∅, a ∈ s, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∃ s1. ∀ b. (∃ a0. a0 ∈ s -- a ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ s0. ∀ b. (∃ a. a ∈ s ∧ path(g)(a, b)) ↔ b ∈ s0

Rule argument

Additional information

Used simplifier rules: ⊦ a ∈ s → #(s -- a) = # s - 1; (s) ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ m < 1 ↔ m = 0; (s) n0 ≤ n ⊦ n - n0 < m ↔ n < m + n0; (s) ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ ¬ n < n; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: s -- a, g

Proof step 6 from proof hpal-reachset-set (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  # s ≠ 0, a0 ≠ a, s ≠ ∅, haspathanylength(g)(a0), a ∈ s, a0 ∈ s, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ s0. ∀ b. (∃ a. a ∈ s ∧ path(g)(a, b)) ↔ b ∈ s0

Rule argument

Additional information

Used simplifier rules: finout-def: ⊦ finout(g) ↔ (∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s); ⊦ a ∈ s -- a0 ↔ a ≠ a0 ∧ a ∈ s; (s)

Proof step 7 from proof hpal-reachset-set (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: a0

Proof step 8 from proof hpal-reachset-set (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  # s ≠ 0, s ≠ ∅, a ∈ s, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ b. (∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ s0. ∀ b. (∃ a. a ∈ s ∧ path(g)(a, b)) ↔ b ∈ s0

Rule argument

Additional information

Used simplifier rules: ⊦ a ∈ s -- a0 ↔ a ≠ a0 ∧ a ∈ s; (s)

Proof step 9 from proof hpal-reachset-set (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 10:

  # s ≠ 0, s ≠ ∅, a ∈ s, a ∈ s → ¬ haspathanylength(g)(a), ∀ b. (∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ s0. ∀ b. (∃ a. a ∈ s ∧ path(g)(a, b)) ↔ b ∈ s0

Rule argument

Additional information

Used terms: a

Proof step 10 from proof hpal-reachset-set (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  # s ≠ 0, s ≠ ∅, a ∈ s, ¬ haspathanylength(g)(a), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ b. (∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ s0. ∀ b. (∃ a. a ∈ s ∧ path(g)(a, b)) ↔ b ∈ s0

Rule argument

Additional information

Proof step 11 from proof hpal-reachset-set (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

  ⊦ haspathanylength(g)(a) ↔ (∀ n. ∃ x. x.head = a ∧ # x = n + 1 ∧ pathp(g)(⌜x⌝ ))

• Proof step 13:

  # s ≠ 0, s ≠ ∅, a ∈ s, ∀ b. (∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∃ n. ¬(∃ x. x.head = a ∧ # x = n + 1 ∧ pathp(g)(⌜x⌝ )), ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ s0. ∀ b. (∃ a. a ∈ s ∧ path(g)(a, b)) ↔ b ∈ s0

Rule argument

Additional information

Used terms: a, g

Proof step 12 from proof hpal-reachset-set (previous step) (back to tree)

Lemma haspathanylength-def

Proof step 13 from proof hpal-reachset-set (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  # s ≠ 0, s ≠ ∅, a ∈ s, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ b. (∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ s0. ∀ b. (∃ a. a ∈ s ∧ path(g)(a, b)) ↔ b ∈ s0, ∃ x. x.head = a ∧ # x = n + 1 ∧ pathp(g)(⌜x⌝ )

Rule argument

Additional information

Proof step 14 from proof hpal-reachset-set (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 15:

  finout(g) ⊦ ∃ s0. ∀ a. reach≤(g)(s, n)(a) ↔ a ∈ s0

• Proof step 16:

  # s ≠ 0, s ≠ ∅, a ∈ s, ∀ b. (∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∃ s0. ∀ a. reach≤(g)(s, n)(a) ↔ a ∈ s0, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ x. x.head = a ∧ # x = n + 1 ∧ pathp(g)(⌜x⌝ ), ∃ s0. ∀ b. (∃ a. a ∈ s ∧ path(g)(a, b)) ↔ b ∈ s0

Rule argument

Additional information

Used simplifier rules: finout-def: ⊦ finout(g) ↔ (∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s); Used terms: g, s, n

Proof step 15 from proof hpal-reachset-set (previous step) (back to tree)

Lemma finreachle-fin

Proof step 16 from proof hpal-reachset-set (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  # s ≠ 0, s ≠ ∅, a ∈ s, ∀ a. reach≤(g)(s, n)(a) ↔ a ∈ s0, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ b. (∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ s0. ∀ b. (∃ a. a ∈ s ∧ path(g)(a, b)) ↔ b ∈ s0, ∃ x. x.head = a ∧ # x = n + 1 ∧ pathp(g)(⌜x⌝ )

Rule argument

Additional information

Proof step 17 from proof hpal-reachset-set (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 18:

  # s ≠ 0, s ≠ ∅, a ∈ s, ∀ b. (∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. reach≤(g)(s, n)(a) ↔ a ∈ s0, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∀ b. (∃ a. a ∈ s ∧ path(g)(a, b)) ↔ b ∈ s1 ∪ s0, ∃ x. x.head = a ∧ # x = n + 1 ∧ pathp(g)(⌜x⌝ )

Rule argument

Additional information

Used terms: s1 ∪ s0

Proof step 18 from proof hpal-reachset-set (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  # s ≠ 0, s ≠ ∅, a ∈ s, ∀ a. reach≤(g)(s, n)(a) ↔ a ∈ s0, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ b. (∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ (∃ a. a ∈ s ∧ path(g)(a, b)) ↔ b ∈ s1 ∨ b ∈ s0, ∃ x. x.head = a ∧ # x = n + 1 ∧ pathp(g)(⌜x⌝ )

Rule argument

Additional information

Used simplifier rules: unc: ⊦ s ∪ s0 = s0 ∪ s; from specification set-union una: ⊦ (s ∪ s0) ∪ s1 = s ∪ s0 ∪ s1; from specification set-union ⊦ a ∈ s1 ∪ s2 ↔ a ∈ s1 ∨ a ∈ s2; (s)

Proof step 19 from proof hpal-reachset-set (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 20:

  # s ≠ 0, s ≠ ∅, a ∈ s, (∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ b. (∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. reach≤(g)(s, n)(a) ↔ a ∈ s0, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ (∃ a. a ∈ s ∧ path(g)(a, b)) ↔ b ∈ s1 ∨ b ∈ s0, ∃ x. x.head = a ∧ # x = n + 1 ∧ pathp(g)(⌜x⌝ )

Rule argument

Additional information

Used terms: b

Proof step 20 from proof hpal-reachset-set (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  # s ≠ 0, s ≠ ∅, a ∈ s, (∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ a. reach≤(g)(s, n)(a) ↔ a ∈ s0, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ b. (∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ (∃ a. a ∈ s ∧ path(g)(a, b)) ↔ b ∈ s1 ∨ b ∈ s0, ∃ x. x.head = a ∧ # x = n + 1 ∧ pathp(g)(⌜x⌝ )

Rule argument

Additional information

Proof step 21 from proof hpal-reachset-set (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 22:

  # s ≠ 0, s ≠ ∅, a ∈ s, ¬ b ∈ s1, ¬ b ∈ s0, (∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ b. (∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. reach≤(g)(s, n)(a) ↔ a ∈ s0, ∃ a. a ∈ s ∧ path(g)(a, b), ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ x. x.head = a ∧ # x = n + 1 ∧ pathp(g)(⌜x⌝ )

• Proof step 81:

  # s ≠ 0, s ≠ ∅, a ∈ s, (∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ b. (∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. reach≤(g)(s, n)(a) ↔ a ∈ s0, b ∈ s1 ∨ b ∈ s0, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ x. x.head = a ∧ # x = n + 1 ∧ pathp(g)(⌜x⌝ ), ∃ a. a ∈ s ∧ path(g)(a, b)

Rule argument

Additional information

Proof step 22 from proof hpal-reachset-set (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  # s ≠ 0, s ≠ ∅, path(g)(a0, b), a0 ∈ s, a ∈ s, ¬ b ∈ s1, ¬ b ∈ s0, ∀ a. reach≤(g)(s, n)(a) ↔ a ∈ s0, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ b. (∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ x. x.head = a ∧ # x = n + 1 ∧ pathp(g)(⌜x⌝ ), ∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, b)

Rule argument

Additional information

Proof step 23 from proof hpal-reachset-set (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 24:

  # s ≠ 0, s ≠ ∅, path(g)(a0, b), a ∈ s, a0 ∈ s, ¬ b ∈ s1, ¬ b ∈ s0, ∀ b. (∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. reach≤(g)(s, n)(a) ↔ a ∈ s0, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, b), ∃ x. x.head = a ∧ # x = n + 1 ∧ pathp(g)(⌜x⌝ ), a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, b)

Rule argument

Additional information

Used terms: a0

Proof step 24 from proof hpal-reachset-set (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  # s ≠ 0, s ≠ ∅, path(g)(a, b), a ∈ s, ¬ b ∈ s0, ¬ b ∈ s1, ∀ b. (∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. reach≤(g)(s, n)(a) ↔ a ∈ s0, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, b), ∃ x. x.head = a ∧ # x = n + 1 ∧ pathp(g)(⌜x⌝ )

Rule argument

Additional information

Proof step 25 from proof hpal-reachset-set (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 26:

  reach≤(g)(s, n)(b) ↔ b ∈ s0, # s ≠ 0, s ≠ ∅, path(g)(a, b), a ∈ s, ¬ b ∈ s0, ¬ b ∈ s1, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ b. (∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ x. x.head = a ∧ # x = n + 1 ∧ pathp(g)(⌜x⌝ ), ∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, b)

Rule argument

Additional information

Used terms: b

Proof step 26 from proof hpal-reachset-set (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  # s ≠ 0, s ≠ ∅, path(g)(a, b), a ∈ s, ¬ reach≤(g)(s, n)(b), ¬ b ∈ s0, ¬ b ∈ s1, ∀ b. (∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, b), ∃ x. x.head = a ∧ # x = n + 1 ∧ pathp(g)(⌜x⌝ )

Rule argument

Additional information

Proof step 27 from proof hpal-reachset-set (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 28:

  ⊦ path(g)(a, b) ↔ (∃ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ a = x.head ∧ b = x.last)

• Proof step 29:

  # s ≠ 0, s ≠ ∅, a ∈ s, ¬ reach≤(g)(s, n)(b), ¬ b ∈ s0, ¬ b ∈ s1, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ b. (∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∃ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ a = x.head ∧ b = x.last, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ x. x.head = a ∧ # x = n + 1 ∧ pathp(g)(⌜x⌝ ), ∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, b)

Rule argument

Additional information

Used terms: b, a, g

Proof step 28 from proof hpal-reachset-set (previous step) (back to tree)

A spec-lemma

Proof step 29 from proof hpal-reachset-set (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 30:

  # s ≠ 0, s ≠ ∅, x ≠ [], pathp(g)(⌜x⌝ ), x.head ∈ s, ¬ reach≤(g)(s, n)(x.last), ¬ x.last ∈ s0, ¬ x.last ∈ s1, ∀ b. (∃ a0. a0 ≠ x.head ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ a0. a0 ≠ x.head ∧ a0 ∈ s ∧ path(g)(a0, x.last), ∃ x0. x0.head = x.head ∧ # x0 = n + 1 ∧ pathp(g)(⌜x0⌝ )

Rule argument

Additional information

Proof step 30 from proof hpal-reachset-set (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 31:

  x = a1 + x1, # s ≠ 0, s ≠ ∅, x ≠ [], pathp(g)(⌜x⌝ ), a1 ∈ s, ¬ reach≤(g)(s, n)(x.last), ¬ x.last ∈ s0, ¬ x.last ∈ s1, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ b. (∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ x0. x0.head = a1 ∧ # x0 = n + 1 ∧ pathp(g)(⌜x0⌝ ), ∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, x.last)

Rule argument

Additional information

Used simplifier rules: x ≠ [] ⊦ a = x.head ∧ y = x.tail ↔ x = a + y; (elim) Used terms: x, a1, x1

Proof step 31 from proof hpal-reachset-set (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 32:

  # s ≠ 0, s ≠ ∅, pathp(g)(⌜a1 '⌝ + ⌜x1⌝ ), a1 ∈ s, ¬ reach≤(g)(s, n)((a1 ' + x1).last), ¬ (a1 ' + x1).last ∈ s0, ¬ (a1 ' + x1).last ∈ s1, ∀ b. (∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ x0. x0.head = a1 ∧ # x0 = n + 1 ∧ pathp(g)(⌜x0⌝ ), ∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, (a1 ' + x1).last)

Rule argument

Additional information

Used simplifier rules: ⊦ a + x = a ' + x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ ⌜x + y⌝ = ⌜x⌝ + ⌜y⌝ ; (s) ⊦ a ' ≠ []; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s)

Proof step 32 from proof hpal-reachset-set (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 33:

  ⊦ reach≤(g)(s, n)(b) ↔ (∃ m. m ≤ n ∧ reach(g)(s, m)(b))

• Proof step 34:

  # s ≠ 0, s ≠ ∅, pathp(g)(⌜a1 '⌝ + ⌜x1⌝ ), a1 ∈ s, ¬ (a1 ' + x1).last ∈ s0, ¬ (a1 ' + x1).last ∈ s1, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ b. (∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ m. ¬(m ≤ n ∧ reach(g)(s, m)((a1 ' + x1).last)), ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, (a1 ' + x1).last), ∃ x0. x0.head = a1 ∧ # x0 = n + 1 ∧ pathp(g)(⌜x0⌝ )

Rule argument

Additional information

Used terms: (a1 ' + x1).last, n, s, g

Proof step 33 from proof hpal-reachset-set (previous step) (back to tree)

Lemma reachle-def

Proof step 34 from proof hpal-reachset-set (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 35:

  # s ≠ 0, s ≠ ∅, pathp(g)(⌜a1 '⌝ + ⌜x1⌝ ), a1 ∈ s, ¬ (a1 ' + x1).last ∈ s0, ¬ (a1 ' + x1).last ∈ s1, ∀ b. (∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ x0. x0.head = a1 ∧ # x0 = n + 1 ∧ pathp(g)(⌜x0⌝ ), ∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, (a1 ' + x1).last), # x1 ≤ n ∧ reach(g)(s, # x1)((a1 ' + x1).last)

Rule argument

Additional information

Used terms: # x1

Proof step 35 from proof hpal-reachset-set (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 36:

  # s ≠ 0, s ≠ ∅, n < # x1, pathp(g)(⌜a1 '⌝ + ⌜x1⌝ ), a1 ∈ s, ¬ (a1 ' + x1).last ∈ s0, ¬ (a1 ' + x1).last ∈ s1, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ b. (∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, (a1 ' + x1).last), ∃ x0. x0.head = a1 ∧ # x0 = n + 1 ∧ pathp(g)(⌜x0⌝ ), # x1 ≤ n ∧ reach(g)(s, # x1)((a1 ' + x1).last)

• Proof step 74:

  # s ≠ 0, s ≠ ∅, pathp(g)(⌜a1 '⌝ + ⌜x1⌝ ), a1 ∈ s, ¬ n < # x1, ¬ (a1 ' + x1).last ∈ s0, ¬ (a1 ' + x1).last ∈ s1, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ b. (∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, (a1 ' + x1).last), ∃ x0. x0.head = a1 ∧ # x0 = n + 1 ∧ pathp(g)(⌜x0⌝ ), # x1 ≤ n ∧ reach(g)(s, # x1)((a1 ' + x1).last)

Rule argument

Additional information

Used formulas: n < # x1

Proof step 36 from proof hpal-reachset-set (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 37:

  # s ≠ 0, s ≠ ∅, x1 ≠ [], n < # x1, pathp(g)(⌜a1 '⌝ + ⌜x1⌝ ), a1 ∈ s, ¬ x1.last ∈ s1, ¬ x1.last ∈ s0, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ b. (∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ x0. x0.head = a1 ∧ # x0 = n + 1 ∧ pathp(g)(⌜x0⌝ ), ∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, x1.last)

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ x ≠ [] → (a ' + x).last = x.last; (s) ⊦ # x = 0 ↔ x = []; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ m < n → (n ≤ m ↔ false); (s)

Proof step 37 from proof hpal-reachset-set (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 38:

  # s ≠ 0, s ≠ ∅, x1 ≠ [], n < # x1, pathp(g)(⌜a1 '⌝ + ⌜x1⌝ ), a1 ∈ s, ¬ x1.last ∈ s1, ¬ x1.last ∈ s0, ∀ b. (∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, x1.last), ((a1 ' + x1).take(n + 1)).head = a1 ∧ # (a1 ' + x1).take(n + 1) = n + 1 ∧ pathp(g)(⌜(a1 ' + x1).take(n + 1)⌝ )

Rule argument

Additional information

Used terms: (a1 ' + x1).take(n + 1)

Proof step 38 from proof hpal-reachset-set (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 39:

  # s ≠ 0, s ≠ ∅, x1 ≠ [], n < # x1, pathp(g)(⌜a1 '⌝ + ⌜x1⌝ ), a1 ∈ s, ¬ pathp(g)(⌜a1 '⌝ + ⌜x1.take(n)⌝ ), ¬ x1.last ∈ s1, ¬ x1.last ∈ s0, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ b. (∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, x1.last)

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ ⌜x + y⌝ = ⌜x⌝ + ⌜y⌝ ; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ a + x = a ' + x; (s) ⊦ (a ' + x).take(n + 1) = a + x.take(n); (s) ⊦ m + n = m + n0 ↔ n = n0; (s) ⊦ m +1 = m + 1; (s) ⊦ n < # x → # x.take(n) = n; (s) ⊦ #(a ' + x) = (# x)+1; (s) ⊦ (a ' + x).head = a; (s)

Proof step 39 from proof hpal-reachset-set (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 40:

  ⊦ pathp(g)(σ) ↔ (∀ n. ⌜n⌝ < # σ → dom(g)(σ[n])) ∧ (∀ n. ⌜n + 1⌝ < # σ → edge(g)(σ[n], σ[n + 1]))

• Proof step 41:

  # s ≠ 0, s ≠ ∅, x1 ≠ [], n < # x1, a1 ∈ s, ¬ pathp(g)(⌜a1 '⌝ + ⌜x1.take(n)⌝ ), ¬ x1.last ∈ s1, ¬ x1.last ∈ s0, ∀ b. (∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ n. ⌜n⌝ < #(⌜a1 '⌝ + ⌜x1⌝ ) → dom(g)((⌜a1 '⌝ + ⌜x1⌝ )[n]), ∀ n. ⌜n + 1⌝ < #(⌜a1 '⌝ + ⌜x1⌝ ) → edge(g)((⌜a1 '⌝ + ⌜x1⌝ )[n], (⌜a1 '⌝ + ⌜x1⌝ )[n + 1]), ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, x1.last)

Rule argument

Additional information

Used terms: ⌜a1 '⌝ + ⌜x1⌝ , g

Proof step 40 from proof hpal-reachset-set (previous step) (back to tree)

A spec-lemma

Proof step 41 from proof hpal-reachset-set (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 42:

  # s ≠ 0, s ≠ ∅, x1 ≠ [], n < # x1, a1 ∈ s, ¬ pathp(g)(⌜a1 '⌝ + ⌜x1.take(n)⌝ ), ¬ x1.last ∈ s1, ¬ x1.last ∈ s0, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ b. (∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ n0. n0 < # x1 → edge(g)((a1 ' + x1)[n0], x1[n0]), ∀ n0. ¬ # x1 < n0 → dom(g)((a1 ' + x1)[n0]), ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, x1.last)

Rule argument

Additional information

Used simplifier rules: append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ (⌜x⌝ + ⌜x0⌝ )[m] = (x + x0)[m]; (s) add-comm: ⊦ n∞1 + n∞2 = n∞2 + n∞1; from specification nat-inf add-assoc: ⊦ (n∞ + n∞1) + n∞2 = n∞ + n∞1 + n∞2; from specification nat-inf ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) ⊦ ⌜n⌝ < ⌜1⌝ + n∞ ↔ ¬ n∞ < ⌜n⌝ ; (s) ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s) ⊦ # a ' = 0 +1; (s) ⊦ #(σ + σ1) = # σ + # σ1; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ ⌜x⌝ [n] = x[n]; (s) ⊦ (⌜a '⌝ + σ)[n + 1] = σ[n]; (s) ⊦ n∞ + ⌜0⌝ = n∞; (s) ⊦ m ≤ n → (⌜(* m)⌝ + n∞2 < ⌜(* n)⌝ + n∞1 ↔ n∞2 < ⌜n - m⌝ + n∞1); (s) ⊦ ⌜m + n⌝ = ⌜m⌝ + ⌜n⌝ ; (s)

Proof step 42 from proof hpal-reachset-set (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 43:

  ⊦ pathp(g)(σ) ↔ (∀ n. ⌜n⌝ < # σ → dom(g)(σ[n])) ∧ (∀ n. ⌜n + 1⌝ < # σ → edge(g)(σ[n], σ[n + 1]))

• Proof step 44:

  # s ≠ 0, s ≠ ∅, x1 ≠ [], n < # x1, a1 ∈ s, ¬ x1.last ∈ s1, ¬ x1.last ∈ s0, ∀ n0. ¬ # x1 < n0 → dom(g)((a1 ' + x1)[n0]), ∀ n0. n0 < # x1 → edge(g)((a1 ' + x1)[n0], x1[n0]), ∀ b. (∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, (∃ n0. ¬(⌜n0⌝ < #(⌜a1 '⌝ + ⌜x1.take(n)⌝ ) → dom(g)((⌜a1 '⌝ + ⌜x1.take(n)⌝ )[n0]))) ∨ (∃ n0. ¬(⌜n0 + 1⌝ < #(⌜a1 '⌝ + ⌜x1.take(n)⌝ ) → edge(g)((⌜a1 '⌝ + ⌜x1.take(n)⌝ )[n0], (⌜a1 '⌝ + ⌜x1.take(n)⌝ )[n0 + 1]))), ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, x1.last)

Rule argument

Additional information

Used terms: ⌜a1 '⌝ + ⌜x1.take(n)⌝ , g

Proof step 43 from proof hpal-reachset-set (previous step) (back to tree)

A spec-lemma

Proof step 44 from proof hpal-reachset-set (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 45:

  # s ≠ 0, s ≠ ∅, x1 ≠ [], n < # x1, a1 ∈ s, ¬ x1.last ∈ s1, ¬ x1.last ∈ s0, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ b. (∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ n0. n0 < # x1 → edge(g)((a1 ' + x1)[n0], x1[n0]), ∀ n0. ¬ # x1 < n0 → dom(g)((a1 ' + x1)[n0]), ¬(¬ n < n0 → dom(g)((a1 ' + x1.take(n))[n0])) ∨ ¬(n1 < n → edge(g)((a1 ' + x1.take(n))[n1], x1.take(n)[n1])), ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, x1.last)

Rule argument

Additional information

Used simplifier rules: append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ ⌜x⌝ [n] = x[n]; (s) ⊦ (⌜a '⌝ + σ)[n + 1] = σ[n]; (s) ⊦ (⌜x⌝ + ⌜x0⌝ )[m] = (x + x0)[m]; (s) add-comm: ⊦ n∞1 + n∞2 = n∞2 + n∞1; from specification nat-inf add-assoc: ⊦ (n∞ + n∞1) + n∞2 = n∞ + n∞1 + n∞2; from specification nat-inf ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) ⊦ n∞ + ⌜0⌝ = n∞; (s) ⊦ m ≤ n → (⌜(* m)⌝ + n∞2 < ⌜(* n)⌝ + n∞1 ↔ n∞2 < ⌜n - m⌝ + n∞1); (s) ⊦ n < # x → # x.take(n) = n; (s) ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s) ⊦ # a ' = 0 +1; (s) ⊦ #(σ + σ1) = # σ + # σ1; (s) ⊦ ⌜m + n⌝ = ⌜m⌝ + ⌜n⌝ ; (s) ⊦ ⌜n⌝ < ⌜1⌝ + n∞ ↔ ¬ n∞ < ⌜n⌝ ; (s)

Proof step 45 from proof hpal-reachset-set (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 46:

  # s ≠ 0, s ≠ ∅, x1 ≠ [], n < # x1, a1 ∈ s, ¬ n < n0, ¬ dom(g)((a1 ' + x1.take(n))[n0]), ¬ x1.last ∈ s1, ¬ x1.last ∈ s0, ∀ n0. ¬ # x1 < n0 → dom(g)((a1 ' + x1)[n0]), ∀ n0. n0 < # x1 → edge(g)((a1 ' + x1)[n0], x1[n0]), ∀ b. (∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, x1.last)

• Proof step 61:

  # s ≠ 0, s ≠ ∅, x1 ≠ [], n1 < n, n < # x1, a1 ∈ s, ¬ edge(g)((a1 ' + x1.take(n))[n1], x1.take(n)[n1]), ¬ x1.last ∈ s1, ¬ x1.last ∈ s0, ∀ n0. ¬ # x1 < n0 → dom(g)((a1 ' + x1)[n0]), ∀ n0. n0 < # x1 → edge(g)((a1 ' + x1)[n0], x1[n0]), ∀ b. (∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, x1.last)

Rule argument

Additional information

Proof step 46 from proof hpal-reachset-set (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 47:

  # s ≠ 0, s ≠ ∅, x1 ≠ [], n < # x1, n0 < # x1, a1 ∈ s, n0 ≤ n, ¬ dom(g)((a1 ' + x1.take(n))[n0]), ¬ x1.last ∈ s1, ¬ x1.last ∈ s0, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ b. (∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ n0. n0 < # x1 → edge(g)((a1 ' + x1)[n0], x1[n0]), ∀ n0. ¬ # x1 < n0 → dom(g)((a1 ' + x1)[n0]), ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, x1.last)

Rule argument

Additional information

Used simplifier rules: fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat ⊦ m < n ↔ ¬ n ≤ m; (ss)

Proof step 47 from proof hpal-reachset-set (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 48:

  ⊦ n < # x → (x + y)[n] = x[n]

• Proof step 49:

  # s ≠ 0, s ≠ ∅, x1 ≠ [], n0 < # x1, n < # x1, a1 ∈ s, n0 ≤ n, ¬ n0 < # a1 ', ¬ dom(g)((a1 ' + x1.take(n))[n0]), ¬ x1.last ∈ s1, ¬ x1.last ∈ s0, ∀ n0. ¬ # x1 < n0 → dom(g)((a1 ' + x1)[n0]), ∀ n0. n0 < # x1 → edge(g)((a1 ' + x1)[n0], x1[n0]), ∀ b. (∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, x1.last)

• Proof step 59:

  # s ≠ 0, s ≠ ∅, x1 ≠ [], n0 < # x1, n < # x1, n0 < # a1 ', a1 ∈ s, n0 ≤ n, ¬ dom(g)(a1 '[n0]), ¬ x1.last ∈ s1, ¬ x1.last ∈ s0, ∀ n0. ¬ # x1 < n0 → dom(g)((a1 ' + x1)[n0]), ∀ n0. n0 < # x1 → edge(g)((a1 ' + x1)[n0], x1[n0]), ∀ b. (∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, x1.last)

Rule argument

Additional information

Used terms: n0, x1.take(n), a1 '

Proof step 48 from proof hpal-reachset-set (previous step) (back to tree)

A spec-lemma

Proof step 49 from proof hpal-reachset-set (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 50:

  # s ≠ 0, n0 ≠ 0, s ≠ ∅, x1 ≠ [], n < # x1, n0 < # x1, a1 ∈ s, n0 ≤ n, ¬ dom(g)((a1 ' + x1.take(n))[n0]), ¬ x1.last ∈ s1, ¬ x1.last ∈ s0, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ b. (∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ n0. n0 < # x1 → edge(g)((a1 ' + x1)[n0], x1[n0]), ∀ n0. ¬ # x1 < n0 → dom(g)((a1 ' + x1)[n0]), ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, x1.last)

Rule argument

Additional information

Used simplifier rules: ⊦ m < 1 ↔ m = 0; (s) ⊦ # a ' = 0 +1; (s)

Proof step 50 from proof hpal-reachset-set (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 51:

  ⊦ ¬ n < # x → (x + y)[n] = y[n - # x]

• Proof step 52:

  # s ≠ 0, n0 ≠ 0, s ≠ ∅, x1 ≠ [], n0 < # x1, n < # x1, a1 ∈ s, n0 ≤ n, ¬ n0 < # a1 ', ¬ dom(g)(x1.take(n)[n0 - # a1 ']), ¬ x1.last ∈ s1, ¬ x1.last ∈ s0, ∀ n0. ¬ # x1 < n0 → dom(g)((a1 ' + x1)[n0]), ∀ n0. n0 < # x1 → edge(g)((a1 ' + x1)[n0], x1[n0]), ∀ b. (∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, x1.last)

Rule argument

Additional information

Used simplifier rules: ⊦ # a ' = 0 +1; (s) ⊦ m < 1 ↔ m = 0; (s) Used terms: a1 ', x1.take(n), n0

Proof step 51 from proof hpal-reachset-set (previous step) (back to tree)

A spec-lemma

Proof step 52 from proof hpal-reachset-set (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 53:

  # s ≠ 0, n0 ≠ 0, s ≠ ∅, x1 ≠ [], n < # x1, n0 < # x1, a1 ∈ s, n0 ≤ n, ¬ dom(g)(x1.take(n)[n0 - 1]), ¬ x1.last ∈ s1, ¬ x1.last ∈ s0, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ b. (∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ n0. n0 < # x1 → edge(g)((a1 ' + x1)[n0], x1[n0]), ∀ n0. ¬ # x1 < n0 → dom(g)((a1 ' + x1)[n0]), ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, x1.last)

Rule argument

Additional information

Used simplifier rules: ⊦ # a ' = 0 +1; (s) ⊦ m < 1 ↔ m = 0; (s)

Proof step 53 from proof hpal-reachset-set (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 54:

  n0 = m + 1, # s ≠ 0, n0 ≠ 0, s ≠ ∅, x1 ≠ [], n0 < # x1, n < # x1, a1 ∈ s, n0 ≤ n, ¬ dom(g)(x1.take(n)[m]), ¬ x1.last ∈ s1, ¬ x1.last ∈ s0, ∀ n0. ¬ # x1 < n0 → dom(g)((a1 ' + x1)[n0]), ∀ n0. n0 < # x1 → edge(g)((a1 ' + x1)[n0], x1[n0]), ∀ b. (∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, x1.last)

Rule argument

Additional information

Used simplifier rules: n ≠ 0 ⊦ m = n - 1 ↔ n = m + 1; (elim) Used terms: n0, m

Proof step 54 from proof hpal-reachset-set (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 55:

  # s ≠ 0, s ≠ ∅, x1 ≠ [], m < # x1, m < n, n < # x1, m + 1 < # x1, a1 ∈ s, ¬ dom(g)(x1.take(n)[m]), ¬ x1.last ∈ s0, ¬ x1.last ∈ s1, ∀ n0. ¬ # x1 < n0 → dom(g)((a1 ' + x1)[n0]), ∀ n0. n0 < # x1 → edge(g)((a1 ' + x1)[n0], x1[n0]), ∀ b. (∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, x1.last)

Rule argument

Additional information

Used simplifier rules: ⊦ m +1 = m + 1; (s) ⊦ m < n → n ≠ 0; (s) trans-nat: ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward) from specification nat-basic lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m + 1 ≤ n ↔ m < n; (s) ⊦ m + 1 ≠ 0; (s)

Proof step 55 from proof hpal-reachset-set (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 56:

  ⊦ n < m ∧ m ≤ # x → x.take(m)[n] = x[n]

• Proof step 57:

  # s ≠ 0, s ≠ ∅, x1 ≠ [], m + 1 < # x1, n < # x1, m < # x1, m < n, a1 ∈ s, n ≤ # x1, ¬ dom(g)(x1[m]), ¬ x1.last ∈ s0, ¬ x1.last ∈ s1, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ b. (∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ n0. n0 < # x1 → edge(g)((a1 ' + x1)[n0], x1[n0]), ∀ n0. ¬ # x1 < n0 → dom(g)((a1 ' + x1)[n0]), ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, x1.last)

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → m ≤ n; (s) Used terms: n, x1, m

Proof step 56 from proof hpal-reachset-set (previous step) (back to tree)

A spec-lemma

Proof step 57 from proof hpal-reachset-set (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 58:

  # s ≠ 0, s ≠ ∅, x1 ≠ [], m < n, m < # x1, n < # x1, m + 1 < # x1, a1 ∈ s, ¬ dom(g)(x1[m]), ¬ x1.last ∈ s0, ¬ x1.last ∈ s1, ∀ n0. ¬ # x1 < n0 → dom(g)((a1 ' + x1)[n0]), ∀ n0. n0 < # x1 → edge(g)((a1 ' + x1)[n0], x1[n0]), ∀ b. (∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, x1.last)

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → m ≤ n; (s)

Proof step 58 from proof hpal-reachset-set (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ (a ' + x)[n + 1] = x[n]; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: m + 1

Proof step 59 from proof hpal-reachset-set (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 60:

  # s ≠ 0, s ≠ ∅, x1 ≠ [], n < # x1, a1 ∈ s, ¬ dom(g)(a1), ¬ x1.last ∈ s0, ¬ x1.last ∈ s1, ∀ n0. ¬ # x1 < n0 → dom(g)((a1 ' + x1)[n0]), ∀ n0. n0 < # x1 → edge(g)((a1 ' + x1)[n0], x1[n0]), ∀ b. (∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, x1.last)

Rule argument

Additional information

Used simplifier rules: ⊦ a '[0] = a; (s) ⊦ # x = 0 ↔ x = []; (s) ⊦ 0 < m ↔ m ≠ 0; (s) ⊦ 0 ≤ m; (s) lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic ⊦ m < 1 ↔ m = 0; (s) ⊦ # a ' = 0 +1; (s)

Proof step 60 from proof hpal-reachset-set (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ n < 0; (s) ⊦ (a ' + x)[0] = a; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: 0

Proof step 61 from proof hpal-reachset-set (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 62:

  # s ≠ 0, s ≠ ∅, x1 ≠ [], n1 < # x1, n1 < n, n < # x1, n1 + 1 < # x1, a1 ∈ s, ¬ edge(g)((a1 ' + x1.take(n))[n1], x1.take(n)[n1]), ¬ x1.last ∈ s0, ¬ x1.last ∈ s1, ∀ n0. ¬ # x1 < n0 → dom(g)((a1 ' + x1)[n0]), ∀ n0. n0 < # x1 → edge(g)((a1 ' + x1)[n0], x1[n0]), ∀ b. (∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, x1.last)

Rule argument

Additional information

Used simplifier rules: ⊦ m +1 = m + 1; (s) ⊦ m < n → n ≠ 0; (s) trans-nat: ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward) from specification nat-basic lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic

Proof step 62 from proof hpal-reachset-set (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 63:

  ⊦ n < m ∧ m ≤ # x → x.take(m)[n] = x[n]

• Proof step 64:

  # s ≠ 0, s ≠ ∅, x1 ≠ [], n1 + 1 < # x1, n < # x1, n1 < # x1, n1 < n, a1 ∈ s, n ≤ # x1, ¬ edge(g)((a1 ' + x1.take(n))[n1], x1[n1]), ¬ x1.last ∈ s0, ¬ x1.last ∈ s1, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ b. (∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ n0. n0 < # x1 → edge(g)((a1 ' + x1)[n0], x1[n0]), ∀ n0. ¬ # x1 < n0 → dom(g)((a1 ' + x1)[n0]), ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, x1.last)

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → m ≤ n; (s) Used terms: n1, x1, n

Proof step 63 from proof hpal-reachset-set (previous step) (back to tree)

A spec-lemma

Proof step 64 from proof hpal-reachset-set (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 65:

  # s ≠ 0, s ≠ ∅, x1 ≠ [], n1 < n, n1 < # x1, n < # x1, n1 + 1 < # x1, a1 ∈ s, ¬ edge(g)((a1 ' + x1.take(n))[n1], x1[n1]), ¬ x1.last ∈ s0, ¬ x1.last ∈ s1, ∀ n0. ¬ # x1 < n0 → dom(g)((a1 ' + x1)[n0]), ∀ n0. n0 < # x1 → edge(g)((a1 ' + x1)[n0], x1[n0]), ∀ b. (∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, x1.last)

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → m ≤ n; (s)

Proof step 65 from proof hpal-reachset-set (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 66:

  # s ≠ 0, s ≠ ∅, x1 ≠ [], n1 + 1 < # x1, n < # x1, n1 < # x1, n1 < n, a1 ∈ s, ¬ edge(g)((a1 ' + x1.take(n))[n1], x1[n1]), ¬ x1.last ∈ s0, ¬ x1.last ∈ s1, n1 < # x1 → edge(g)((a1 ' + x1)[n1], x1[n1]), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ b. (∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ n0. ¬ # x1 < n0 → dom(g)((a1 ' + x1)[n0]), ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, x1.last)

Rule argument

Additional information

Used terms: n1

Proof step 66 from proof hpal-reachset-set (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 67:

  # s ≠ 0, s ≠ ∅, x1 ≠ [], n1 < n, n1 < # x1, n < # x1, n1 + 1 < # x1, edge(g)((a1 ' + x1)[n1], x1[n1]), a1 ∈ s, ¬ edge(g)((a1 ' + x1.take(n))[n1], x1[n1]), ¬ x1.last ∈ s0, ¬ x1.last ∈ s1, ∀ n0. ¬ # x1 < n0 → dom(g)((a1 ' + x1)[n0]), ∀ b. (∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, x1.last)

Rule argument

Additional information

Proof step 67 from proof hpal-reachset-set (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 68:

  ⊦ n < # x → (x + y)[n] = x[n]

• Proof step 69:

  # s ≠ 0, s ≠ ∅, x1 ≠ [], n1 + 1 < # x1, n < # x1, n1 < # x1, n1 < n, edge(g)((a1 ' + x1)[n1], x1[n1]), a1 ∈ s, ¬ n1 < # a1 ', ¬ edge(g)((a1 ' + x1.take(n))[n1], x1[n1]), ¬ x1.last ∈ s0, ¬ x1.last ∈ s1, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ b. (∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ n0. ¬ # x1 < n0 → dom(g)((a1 ' + x1)[n0]), ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, x1.last)

Rule argument

Additional information

Used simplifier rules: ⊦ n < # x → (x + y)[n] = x[n]; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: n1, x1.take(n), a1 '

Proof step 68 from proof hpal-reachset-set (previous step) (back to tree)

A spec-lemma

Proof step 69 from proof hpal-reachset-set (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 70:

  # s ≠ 0, n1 ≠ 0, s ≠ ∅, x1 ≠ [], n1 < n, n1 < # x1, n < # x1, n1 + 1 < # x1, edge(g)(x1[n1 - 1], x1[n1]), a1 ∈ s, ¬ edge(g)((a1 ' + x1.take(n))[n1], x1[n1]), ¬ x1.last ∈ s0, ¬ x1.last ∈ s1, ∀ n0. ¬ # x1 < n0 → dom(g)((a1 ' + x1)[n0]), ∀ b. (∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, x1.last)

Rule argument

Additional information

Used simplifier rules: ⊦ m < 1 ↔ m = 0; (s) ⊦ # a ' = 0 +1; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ ¬ n < # x → (x + y)[n] = y[n - # x]; (s)

Proof step 70 from proof hpal-reachset-set (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 71:

  n1 = m + 1, # s ≠ 0, n1 ≠ 0, s ≠ ∅, x1 ≠ [], n1 + 1 < # x1, n < # x1, n1 < # x1, n1 < n, edge(g)(x1[m], x1[n1]), a1 ∈ s, ¬ edge(g)((a1 ' + x1.take(n))[n1], x1[n1]), ¬ x1.last ∈ s0, ¬ x1.last ∈ s1, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ b. (∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ n0. ¬ # x1 < n0 → dom(g)((a1 ' + x1)[n0]), ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, x1.last)

Rule argument

Additional information

Used simplifier rules: n ≠ 0 ⊦ m = n - 1 ↔ n = m + 1; (elim) Used terms: n1, m

Proof step 71 from proof hpal-reachset-set (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 72:

  # s ≠ 0, s ≠ ∅, x1 ≠ [], m + 1 < # x1, n < # x1, m + 1 < n, 2 + m < # x1, edge(g)(x1[m], x1[m + 1]), a1 ∈ s, ¬ edge(g)(x1.take(n)[m], x1[m + 1]), ¬ x1.last ∈ s1, ¬ x1.last ∈ s0, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ b. (∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ n0. ¬ # x1 < n0 → dom(g)((a1 ' + x1)[n0]), ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, x1.last)

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m +1 = m + 1; (s) trans-nat: ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward) from specification nat-basic lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ (a ' + x)[n + 1] = x[n]; (s) ⊦ m + 1 ≠ 0; (s)

Proof step 72 from proof hpal-reachset-set (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 73:

  ⊦ n < m ∧ m ≤ # x → x.take(m)[n] = x[n]

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → m ≤ n; (s) ⊦ ¬ m < n → ¬ m + m0 < n; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: n, x1, m

Proof step 73 from proof hpal-reachset-set (previous step) (back to tree)

A spec-lemma

Proof step 74 from proof hpal-reachset-set (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 75:

  # s ≠ 0, s ≠ ∅, pathp(g)(⌜a1 '⌝ + ⌜x1⌝ ), a1 ∈ s, # x1 ≤ n, ¬ reach(g)(s, # x1)((a1 ' + x1).last), ¬ (a1 ' + x1).last ∈ s0, ¬ (a1 ' + x1).last ∈ s1, ∀ b. (∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ x0. x0.head = a1 ∧ # x0 = n + 1 ∧ pathp(g)(⌜x0⌝ ), ∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, (a1 ' + x1).last)

Rule argument

Additional information

Used simplifier rules: ⊦ m < n ↔ ¬ n ≤ m; (ss)

Proof step 75 from proof hpal-reachset-set (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And obtained the following new goals

• Proof step 76:

  # s ≠ 0, s ≠ ∅, pathp(g)(⌜a1 '⌝ + ⌜x1⌝ ), a1 ∈ s, # x1 ≤ n, ¬ reach(g)(s, # x1)((a1 ' + x1).last), ¬ (a1 ' + x1).last ∈ s0, ¬ (a1 ' + x1).last ∈ s1, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ b. (∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, (a1 ' + x1).last), ∃ x0. x0.head = a1 ∧ # x0 = n + 1 ∧ pathp(g)(⌜x0⌝ ), (a1 ' + x1).head = a1 ∧ #(a1 ' + x1) = n + 1 ∧ pathp(g)(⌜a1 ' + x1⌝ )

Rule argument

Additional information

Used terms: a1 ' + x1

Proof step 76 from proof hpal-reachset-set (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 77:

  # x1 ≠ n, # s ≠ 0, s ≠ ∅, # x1 < n, pathp(g)(⌜a1 '⌝ + ⌜x1⌝ ), a1 ∈ s, ¬ reach(g)(s, # x1)((a1 ' + x1).last), ¬ (a1 ' + x1).last ∈ s1, ¬ (a1 ' + x1).last ∈ s0, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ b. (∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, (a1 ' + x1).last), ∃ x0. x0.head = a1 ∧ # x0 = n + 1 ∧ pathp(g)(⌜x0⌝ )

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ m ≠ n → (m ≤ n ↔ m < n); (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ ⌜x + y⌝ = ⌜x⌝ + ⌜y⌝ ; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m + n = m + n0 ↔ n = n0; (s) ⊦ m +1 = m + 1; (s) ⊦ #(a ' + x) = (# x)+1; (s) ⊦ (a ' + x).head = a; (s)

Proof step 77 from proof hpal-reachset-set (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 78:

  ⊦ reach(g)(s, n)(b) ↔ (∃ x. x ≠ [] ∧ x.head ∈ s ∧ pathp(g)(⌜x⌝ ) ∧ b = x.last ∧ # x = n + 1)

• Proof step 79:

  # x1 ≠ n, # s ≠ 0, s ≠ ∅, # x1 < n, pathp(g)(⌜a1 '⌝ + ⌜x1⌝ ), a1 ∈ s, ¬ (a1 ' + x1).last ∈ s1, ¬ (a1 ' + x1).last ∈ s0, ∀ b. (∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ x. ¬(x ≠ [] ∧ x.head ∈ s ∧ pathp(g)(⌜x⌝ ) ∧ (a1 ' + x1).last = x.last ∧ # x = # x1 + 1), ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ x0. x0.head = a1 ∧ # x0 = n + 1 ∧ pathp(g)(⌜x0⌝ ), ∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, (a1 ' + x1).last)

Rule argument

Additional information

Used terms: g, s, # x1, (a1 ' + x1).last

Proof step 78 from proof hpal-reachset-set (previous step) (back to tree)

Lemma reach-def

Proof step 79 from proof hpal-reachset-set (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 80:

  # x1 ≠ n, # s ≠ 0, s ≠ ∅, # x1 < n, pathp(g)(⌜a1 '⌝ + ⌜x1⌝ ), a1 ∈ s, ¬ (a1 ' + x1).last ∈ s1, ¬ (a1 ' + x1).last ∈ s0, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ b. (∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ x. x = [] ∨ ¬ x.head ∈ s ∨ ¬ pathp(g)(⌜x⌝ ) ∨ (a1 ' + x1).last ≠ x.last ∨ # x ≠ # x1 + 1, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ a0. a0 ≠ a1 ∧ a0 ∈ s ∧ path(g)(a0, (a1 ' + x1).last), ∃ x0. x0.head = a1 ∧ # x0 = n + 1 ∧ pathp(g)(⌜x0⌝ )

Rule argument

Additional information

Proof step 80 from proof hpal-reachset-set (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ a ' ≠ []; (s) ⊦ (a ' + x).head = a; (s) ⊦ ⌜x + y⌝ = ⌜x⌝ + ⌜y⌝ ; (s) ⊦ #(a ' + x) = (# x)+1; (s) ⊦ m +1 = m + 1; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ m + n = m + n0 ↔ n = n0; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: a1 ' + x1

Proof step 81 from proof hpal-reachset-set (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 82:

  # s ≠ 0, s ≠ ∅, a ∈ s, (∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ a. reach≤(g)(s, n)(a) ↔ a ∈ s0, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ b. (∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, b ∈ s1 ∨ b ∈ s0, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ a. a ∈ s ∧ path(g)(a, b), ∃ x. x.head = a ∧ # x = n + 1 ∧ pathp(g)(⌜x⌝ )

Rule argument

Additional information

Proof step 82 from proof hpal-reachset-set (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 83:

  # s ≠ 0, s ≠ ∅, a ∈ s, ¬ b ∈ s1, ∀ b. (∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. reach≤(g)(s, n)(a) ↔ a ∈ s0, b ∈ s1 ∨ b ∈ s0, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ x. x.head = a ∧ # x = n + 1 ∧ pathp(g)(⌜x⌝ ), ∃ a. a ∈ s ∧ path(g)(a, b), ∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, b)

• Proof step 100:

  # s ≠ 0, s ≠ ∅, a ∈ s, b ∈ s1, ∀ b. (∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. reach≤(g)(s, n)(a) ↔ a ∈ s0, ∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, b), b ∈ s1 ∨ b ∈ s0, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ x. x.head = a ∧ # x = n + 1 ∧ pathp(g)(⌜x⌝ ), ∃ a. a ∈ s ∧ path(g)(a, b)

Rule argument

Additional information

Proof step 83 from proof hpal-reachset-set (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 84:

  # s ≠ 0, # s0 ≠ 0, s ≠ ∅, s0 ≠ ∅, b ∈ s0, a ∈ s, ¬ b ∈ s1, ∀ b. (∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. reach≤(g)(s, n)(a) ↔ a ∈ s0, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ x. x.head = a ∧ # x = n + 1 ∧ pathp(g)(⌜x⌝ ), ∃ a. a ∈ s ∧ path(g)(a, b), ∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, b)

Rule argument

Additional information

Used simplifier rules: size-zero-01: ⊦ s ≠ ∅ → # s ≠ 0; (forward) from specification set-basic ne-01: ⊦ a ∈ s → s ≠ ∅; (forward) from specification set-basic

Proof step 84 from proof hpal-reachset-set (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 85:

  reach≤(g)(s, n)(b) ↔ b ∈ s0, # s ≠ 0, # s0 ≠ 0, s ≠ ∅, s0 ≠ ∅, a ∈ s, b ∈ s0, ¬ b ∈ s1, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ b. (∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, b), ∃ a. a ∈ s ∧ path(g)(a, b), ∃ x. x.head = a ∧ # x = n + 1 ∧ pathp(g)(⌜x⌝ )

Rule argument

Additional information

Used terms: b

Proof step 85 from proof hpal-reachset-set (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 86:

  # s ≠ 0, # s0 ≠ 0, s ≠ ∅, s0 ≠ ∅, reach≤(g)(s, n)(b), b ∈ s0, a ∈ s, ¬ b ∈ s1, ∀ b. (∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ x. x.head = a ∧ # x = n + 1 ∧ pathp(g)(⌜x⌝ ), ∃ a. a ∈ s ∧ path(g)(a, b), ∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, b)

Rule argument

Additional information

Proof step 86 from proof hpal-reachset-set (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 87:

  ⊦ reach≤(g)(s, n)(b) ↔ (∃ m. m ≤ n ∧ reach(g)(s, m)(b))

• Proof step 88:

  # s ≠ 0, # s0 ≠ 0, s ≠ ∅, s0 ≠ ∅, a ∈ s, b ∈ s0, ¬ b ∈ s1, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ b. (∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∃ m. m ≤ n ∧ reach(g)(s, m)(b), ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, b), ∃ a. a ∈ s ∧ path(g)(a, b), ∃ x. x.head = a ∧ # x = n + 1 ∧ pathp(g)(⌜x⌝ )

Rule argument

Additional information

Used terms: b, n, s, g

Proof step 87 from proof hpal-reachset-set (previous step) (back to tree)

Lemma reachle-def

Proof step 88 from proof hpal-reachset-set (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 89:

  # s ≠ 0, # s0 ≠ 0, s ≠ ∅, s0 ≠ ∅, reach(g)(s, m)(b), b ∈ s0, a ∈ s, m ≤ n, ¬ b ∈ s1, ∀ b. (∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ x. x.head = a ∧ # x = n + 1 ∧ pathp(g)(⌜x⌝ ), ∃ a. a ∈ s ∧ path(g)(a, b), ∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, b)

Rule argument

Additional information

Proof step 89 from proof hpal-reachset-set (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 90:

  ⊦ reach(g)(s, n)(b) ↔ (∃ x. x ≠ [] ∧ x.head ∈ s ∧ pathp(g)(⌜x⌝ ) ∧ b = x.last ∧ # x = n + 1)

• Proof step 91:

  # s ≠ 0, # s0 ≠ 0, s ≠ ∅, s0 ≠ ∅, a ∈ s, b ∈ s0, m ≤ n, ¬ b ∈ s1, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ b. (∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∃ x. x ≠ [] ∧ x.head ∈ s ∧ pathp(g)(⌜x⌝ ) ∧ b = x.last ∧ # x = m + 1, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, b), ∃ a. a ∈ s ∧ path(g)(a, b), ∃ x. x.head = a ∧ # x = n + 1 ∧ pathp(g)(⌜x⌝ )

Rule argument

Additional information

Used terms: g, s, m, b

Proof step 90 from proof hpal-reachset-set (previous step) (back to tree)

Lemma reach-def

Proof step 91 from proof hpal-reachset-set (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 92:

  # x = m + 1, # s ≠ 0, # s0 ≠ 0, s ≠ ∅, s0 ≠ ∅, x ≠ [], pathp(g)(⌜x⌝ ), x.head ∈ s, x.last ∈ s0, a ∈ s, m ≤ n, ¬ x.last ∈ s1, ∀ b. (∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ x. x.head = a ∧ # x = n + 1 ∧ pathp(g)(⌜x⌝ ), ∃ a. a ∈ s ∧ path(g)(a, x.last), ∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, x.last)

Rule argument

Additional information

Proof step 92 from proof hpal-reachset-set (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 93:

  # x = m + 1, x = a1 + x0, # s ≠ 0, # s0 ≠ 0, s ≠ ∅, s0 ≠ ∅, x ≠ [], pathp(g)(⌜x⌝ ), a ∈ s, x.last ∈ s0, a1 ∈ s, m ≤ n, ¬ x.last ∈ s1, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ b. (∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, x.last), ∃ a. a ∈ s ∧ path(g)(a, x.last), ∃ x. x.head = a ∧ # x = n + 1 ∧ pathp(g)(⌜x⌝ )

Rule argument

Additional information

Used simplifier rules: ⊦ x ≠ [] → (head = x.head ∧ tail = x.tail ↔ x = head + tail); (elim) Used terms: x, a1, x0

Proof step 93 from proof hpal-reachset-set (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 94:

  # s0 ≠ 0, # s ≠ 0, s ≠ ∅, s0 ≠ ∅, pathp(g)(⌜a1 '⌝ + ⌜x0⌝ ), a ∈ s, (a1 ' + x0).last ∈ s0, a1 ∈ s, # x0 ≤ n, ¬ (a1 ' + x0).last ∈ s1, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ b. (∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, (a1 ' + x0).last), ∃ a0. a0 ∈ s ∧ path(g)(a0, (a1 ' + x0).last), ∃ x. x.head = a ∧ # x = n + 1 ∧ pathp(g)(⌜x⌝ )

Rule argument

Additional information

Used simplifier rules: ⊦ a + x = a ' + x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ ⌜x + y⌝ = ⌜x⌝ + ⌜y⌝ ; (s) ⊦ a ' ≠ []; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m + n = m + n0 ↔ n = n0; (s) ⊦ m +1 = m + 1; (s) ⊦ #(a ' + x) = (# x)+1; (s)

Proof step 94 from proof hpal-reachset-set (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 95:

  # s0 ≠ 0, # s ≠ 0, s ≠ ∅, s0 ≠ ∅, pathp(g)(⌜a1 '⌝ + ⌜x0⌝ ), a1 ∈ s, (a1 ' + x0).last ∈ s0, a ∈ s, # x0 ≤ n, ¬ (a1 ' + x0).last ∈ s1, ∀ b. (∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ x. x.head = a ∧ # x = n + 1 ∧ pathp(g)(⌜x⌝ ), ∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, (a1 ' + x0).last), a1 ∈ s ∧ path(g)(a1, (a1 ' + x0).last)

Rule argument

Additional information

Used terms: a1

Proof step 95 from proof hpal-reachset-set (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 96:

  # s0 ≠ 0, # s ≠ 0, s ≠ ∅, s0 ≠ ∅, pathp(g)(⌜a1 '⌝ + ⌜x0⌝ ), a ∈ s, (a1 ' + x0).last ∈ s0, a1 ∈ s, # x0 ≤ n, ¬ path(g)(a1, (a1 ' + x0).last), ¬ (a1 ' + x0).last ∈ s1, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ b. (∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, (a1 ' + x0).last), ∃ x. x.head = a ∧ # x = n + 1 ∧ pathp(g)(⌜x⌝ )

Rule argument

Additional information

Proof step 96 from proof hpal-reachset-set (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 97:

  ⊦ path(g)(a, b) ↔ (∃ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ a = x.head ∧ b = x.last)

• Proof step 98:

  # s0 ≠ 0, # s ≠ 0, s ≠ ∅, s0 ≠ ∅, pathp(g)(⌜a1 '⌝ + ⌜x0⌝ ), a1 ∈ s, (a1 ' + x0).last ∈ s0, a ∈ s, # x0 ≤ n, ¬ (a1 ' + x0).last ∈ s1, ∀ b. (∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ x. ¬(pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ a1 = x.head ∧ (a1 ' + x0).last = x.last), ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ x. x.head = a ∧ # x = n + 1 ∧ pathp(g)(⌜x⌝ ), ∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, (a1 ' + x0).last)

Rule argument

Additional information

Used terms: (a1 ' + x0).last, a1, g

Proof step 97 from proof hpal-reachset-set (previous step) (back to tree)

A spec-lemma

Proof step 98 from proof hpal-reachset-set (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 99:

  # s0 ≠ 0, # s ≠ 0, s ≠ ∅, s0 ≠ ∅, pathp(g)(⌜a1 '⌝ + ⌜x0⌝ ), a ∈ s, (a1 ' + x0).last ∈ s0, a1 ∈ s, # x0 ≤ n, ¬ (a1 ' + x0).last ∈ s1, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ b. (∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ x. ¬ pathp(g)(⌜x⌝ ) ∨ x = [] ∨ a1 ≠ x.head ∨ (x.head ' + x0).last ≠ x.last, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, (a1 ' + x0).last), ∃ x. x.head = a ∧ # x = n + 1 ∧ pathp(g)(⌜x⌝ )

Rule argument

Additional information

Proof step 99 from proof hpal-reachset-set (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜x + y⌝ = ⌜x⌝ + ⌜y⌝ ; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ a ' ≠ []; (s) ⊦ (a ' + x).head = a; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a + x = a ' + x; (s) Used terms: a1 + x0

Proof step 100 from proof hpal-reachset-set (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 101:

  # s ≠ 0, # s1 ≠ 0, a0 ≠ a, s ≠ ∅, s1 ≠ ∅, path(g)(a0, b), a ∈ s, b ∈ s1, a0 ∈ s, ∀ b. (∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ path(g)(a0, b)) ↔ b ∈ s1, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. reach≤(g)(s, n)(a) ↔ a ∈ s0, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ x. x.head = a ∧ # x = n + 1 ∧ pathp(g)(⌜x⌝ ), ∃ a. a ∈ s ∧ path(g)(a, b)

Rule argument

Additional information

Used simplifier rules: size-zero-01: ⊦ s ≠ ∅ → # s ≠ 0; (forward) from specification set-basic ne-01: ⊦ a ∈ s → s ≠ ∅; (forward) from specification set-basic

Proof step 101 from proof hpal-reachset-set (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: a0

Proof step 102 from proof hpal-reachset-set (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 103:

  ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∀ b. (∃ a. a ∈ s ∧ path(g)(a, b)) ↔ b ∈ ∅, ∃ a. a ∈ s

Rule argument

Additional information

Used terms: ∅

Proof step 103 from proof hpal-reachset-set (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 104:

  # s ≠ 0, s ≠ ∅, path(g)(a, b), a ∈ s, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ s0, g. # s0 < # s → finout(g) ∧ (∀ a. a ∈ s0 → ¬ haspathanylength(g)(a)) → (∃ s1. ∀ b. (∃ a. a ∈ s0 ∧ path(g)(a, b)) ↔ b ∈ s1) ⊦ ∃ a. a ∈ s

Rule argument

Additional information

Used simplifier rules: size-zero-01: ⊦ s ≠ ∅ → # s ≠ 0; (forward) from specification set-basic ne-01: ⊦ a ∈ s → s ≠ ∅; (forward) from specification set-basic ⊦ ¬ a ∈ ∅; (s)

Proof step 104 from proof hpal-reachset-set (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: a