Proof step 1 from proof hpal-next-auxh (conclusion) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 2:

  ∀ b. b ∈ s → ¬ haspathanylength(g)(b) ⊦ ∃ n. ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s → # x < n

Rule argument

Additional information

Proof step 2 from proof hpal-next-auxh (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 3:

  ∀ b. b ∈ s0 ++ a → ¬ haspathanylength(g)(b), ∀ g. (∀ b. b ∈ s0 → ¬ haspathanylength(g)(b)) → (∃ n. ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n) ⊦ ∃ n. ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 ++ a → # x < n

Rule argument

Additional information

Used simplifier rules: Set('a) generated by ∅, ++;; ⊦ ¬ a ∈ ∅; (s)

Proof step 3 from proof hpal-next-auxh (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  ∀ g. (∀ b. b ∈ s0 → ¬ haspathanylength(g)(b)) → (∃ n. ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n), ∀ b. b = a ∨ b ∈ s0 → ¬ haspathanylength(g)(b) ⊦ ∃ n. ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ (x.head = a ∨ x.head ∈ s0) → # x < n

Rule argument

Additional information

Used simplifier rules: ⊦ a ∈ s ++ b ↔ a = b ∨ a ∈ s; (s)

Proof step 4 from proof hpal-next-auxh (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 5:

  (∀ b. b ∈ s0 → ¬ haspathanylength(g)(b)) → (∃ n. ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n), ∀ b. b = a ∨ b ∈ s0 → ¬ haspathanylength(g)(b) ⊦ ∃ n. ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ (x.head = a ∨ x.head ∈ s0) → # x < n

Rule argument

Additional information

Used terms: g

Proof step 5 from proof hpal-next-auxh (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  (b ∈ s0 → ¬ haspathanylength(g)(b)) → (∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n), ∀ b. b = a ∨ b ∈ s0 → ¬ haspathanylength(g)(b) ⊦ ∃ n. ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ (x.head = a ∨ x.head ∈ s0) → # x < n

Rule argument

Additional information

Proof step 6 from proof hpal-next-auxh (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 7:

  haspathanylength(g)(b), b ∈ s0, ∀ b. b = a ∨ b ∈ s0 → ¬ haspathanylength(g)(b) ⊦ ∃ n. ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ (x.head = a ∨ x.head ∈ s0) → # x < n

• Proof step 9:

  ∀ b. b = a ∨ b ∈ s0 → ¬ haspathanylength(g)(b), ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n ⊦ ∃ n. ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ (x.head = a ∨ x.head ∈ s0) → # x < n

Rule argument

Additional information

Proof step 7 from proof hpal-next-auxh (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  # s0 ≠ 0, s0 ≠ ∅, haspathanylength(g)(b), b ∈ s0, ∀ b. b = a ∨ b ∈ s0 → ¬ haspathanylength(g)(b) ⊦ ∃ n. ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ (x.head = a ∨ x.head ∈ s0) → # x < n

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 8 from proof hpal-next-auxh (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: b

Proof step 9 from proof hpal-next-auxh (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 10:

  a = a ∨ a ∈ s0 → ¬ haspathanylength(g)(a), ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n, ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b) ⊦ ∃ n. ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ (x.head = a ∨ x.head ∈ s0) → # x < n

Rule argument

Additional information

Used terms: a

Proof step 10 from proof hpal-next-auxh (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  ¬ haspathanylength(g)(a), ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b), ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n ⊦ ∃ n. ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ (x.head = a ∨ x.head ∈ s0) → # x < n

Rule argument

Additional information

Proof step 11 from proof hpal-next-auxh (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:

  ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n, ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b), ∃ n. ¬(∃ x. x.head = a ∧ # x = n + 1 ∧ pathp(g)(⌜x⌝ )) ⊦ ∃ n. ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ (x.head = a ∨ x.head ∈ s0) → # x < n

Rule argument

Additional information

Used terms: a, g

Proof step 12 from proof hpal-next-auxh (previous step) (back to tree)

Lemma haspathanylength-def

Proof step 13 from proof hpal-next-auxh (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b), ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n ⊦ ∃ n. ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ (x.head = a ∨ x.head ∈ s0) → # x < n, ∃ x. x.head = a ∧ # x = n0 + 1 ∧ pathp(g)(⌜x⌝ )

Rule argument

Additional information

Proof step 14 from proof hpal-next-auxh (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 15:

  n < n0, ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n, ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b) ⊦ ∃ x. x.head = a ∧ # x = n0 + 1 ∧ pathp(g)(⌜x⌝ ), ∃ n. ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ (x.head = a ∨ x.head ∈ s0) → # x < n

• Proof step 51:

  ¬ n < n0, ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n, ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b) ⊦ ∃ x. x.head = a ∧ # x = n0 + 1 ∧ pathp(g)(⌜x⌝ ), ∃ n. ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ (x.head = a ∨ x.head ∈ s0) → # x < n

Rule argument

Additional information

Used formulas: n < n0

Proof step 15 from proof hpal-next-auxh (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 16:

  n < n0, ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b), ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n ⊦ ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ (x.head = a ∨ x.head ∈ s0) → # x < n0 + 1, ∃ x. x.head = a ∧ # x = n0 + 1 ∧ pathp(g)(⌜x⌝ )

Rule argument

Additional information

Used terms: n0 + 1

Proof step 16 from proof hpal-next-auxh (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  x ≠ [], n < # x, n0 < # x, n < n0, n + 1 < # x, pathp(g)(⌜x⌝ ), ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b), ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n, x.head = a ∨ x.head ∈ s0 ⊦ ∃ x. x.head = a ∧ # x = n0 + 1 ∧ pathp(g)(⌜x⌝ )

Rule argument

Additional information

Used simplifier rules: ⊦ m +1 = m + 1; (s) ⊦ m < n → n ≠ 0; (s) ⊦ # x = 0 ↔ x = []; (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 < n + 1 ↔ ¬ n < m; (s)

Proof step 17 from proof hpal-next-auxh (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 18:

  x = a0 + x0, x ≠ [], n + 1 < # x, n < n0, n0 < # x, n < # x, pathp(g)(⌜x⌝ ), ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n, ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b), a0 = a ∨ a0 ∈ s0 ⊦ ∃ x. x.head = a ∧ # x = n0 + 1 ∧ pathp(g)(⌜x⌝ )

Rule argument

Additional information

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

Proof step 18 from proof hpal-next-auxh (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  x0 ≠ [], n < # x0, n < n0, pathp(g)(⌜a0 '⌝ + ⌜x0⌝ ), n0 ≤ # x0, ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n, ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b), a0 = a ∨ a0 ∈ s0 ⊦ ∃ x. x.head = a ∧ # x = n0 + 1 ∧ pathp(g)(⌜x⌝ )

Rule argument

Additional information

Used simplifier rules: ⊦ # x = 0 ↔ x = []; (s) fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m < n → ¬ n < m; (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) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ m +1 = m + 1; (s) ⊦ #(a ' + x) = (# x)+1; (s) ⊦ a + x = a ' + x; (s) ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ ⌜x + y⌝ = ⌜x⌝ + ⌜y⌝ ; (s) ⊦ a ' ≠ []; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s)

Proof step 19 from proof hpal-next-auxh (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 20:

  a0 = a, x0 ≠ [], n < n0, n < # x0, pathp(g)(⌜a0 '⌝ + ⌜x0⌝ ), n0 ≤ # x0, ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b), ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n ⊦ ∃ x. x.head = a ∧ # x = n0 + 1 ∧ pathp(g)(⌜x⌝ )

• Proof step 49:

  x0 ≠ [], n < n0, n < # x0, pathp(g)(⌜a0 '⌝ + ⌜x0⌝ ), a0 ∈ s0, n0 ≤ # x0, ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b), ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n ⊦ ∃ x. x.head = a ∧ # x = n0 + 1 ∧ pathp(g)(⌜x⌝ )

Rule argument

Additional information

Proof step 20 from proof hpal-next-auxh (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  x0 ≠ [], n < # x0, n < n0, pathp(g)(⌜a '⌝ + ⌜x0⌝ ), n0 ≤ # x0, ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n, ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b) ⊦ ∃ x. x.head = a ∧ # x = n0 + 1 ∧ pathp(g)(⌜x⌝ )

Rule argument

Additional information

Proof step 21 from proof hpal-next-auxh (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 22:

  x0 ≠ [], n < n0, n < # x0, pathp(g)(⌜a '⌝ + ⌜x0⌝ ), n0 ≤ # x0, ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b), ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n ⊦ ((a ' + x0).take(n0 + 1)).head = a ∧ # (a ' + x0).take(n0 + 1) = n0 + 1 ∧ pathp(g)(⌜(a ' + x0).take(n0 + 1)⌝ )

Rule argument

Additional information

Used terms: (a ' + x0).take(n0 + 1)

Proof step 22 from proof hpal-next-auxh (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  x0 ≠ [], n < # x0, n < n0, pathp(g)(⌜a '⌝ + ⌜x0⌝ ), n0 ≤ # x0, ¬ pathp(g)(⌜a '⌝ + ⌜x0.take(n0)⌝ ), ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n, ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b) ⊦

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 23 from proof hpal-next-auxh (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 24:

  # x1 = n0, x0 = x1 + x2, x0 ≠ [], n < n0, n < # x0, pathp(g)(⌜a '⌝ + ⌜x0⌝ ), n0 ≤ # x0, ¬ pathp(g)(⌜a '⌝ + ⌜x1⌝ ), ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b), ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ n ≤ # x → (y = x.take(n) ∧ z = x.drop(n) ↔ x = y + z ∧ # y = n); (elim) Used terms: n0, x0, x1, x2

Proof step 24 from proof hpal-next-auxh (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  x1 ≠ [], n < # x1 + # x2, n < # x1, pathp(g)(⌜a '⌝ + ⌜x1⌝ + ⌜x2⌝ ), ¬ pathp(g)(⌜a '⌝ + ⌜x1⌝ ), ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b), ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # x = 0 ↔ x = []; (s) ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ #(x + y) = # x + # y; (s) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ ⌜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 ≤ m + n; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s)

Proof step 25 from proof hpal-next-auxh (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 26:

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

• Proof step 27:

  x1 ≠ [], n < # x1, n < # x1 + # x2, pathp(g)(⌜a '⌝ + ⌜x1⌝ + ⌜x2⌝ ), ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n, ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b), (∃ n. ¬(⌜n⌝ < #(⌜a '⌝ + ⌜x1⌝ ) → dom(g)((⌜a '⌝ + ⌜x1⌝ )[n]))) ∨ (∃ n. ¬(⌜n + 1⌝ < #(⌜a '⌝ + ⌜x1⌝ ) → edge(g)((⌜a '⌝ + ⌜x1⌝ )[n], (⌜a '⌝ + ⌜x1⌝ )[n + 1]))) ⊦

Rule argument

Additional information

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

Proof step 26 from proof hpal-next-auxh (previous step) (back to tree)

A spec-lemma

Proof step 27 from proof hpal-next-auxh (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

  x1 ≠ [], n < # x1 + # x2, n < # x1, pathp(g)(⌜a '⌝ + ⌜x1⌝ + ⌜x2⌝ ), ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b), ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n, ¬(¬ # x1 < n0 → dom(g)((a ' + x1)[n0])) ∨ ¬(n1 < # x1 → edge(g)((a ' + x1)[n1], x1[n1])) ⊦

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) ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s) ⊦ # a ' = 0 +1; (s) ⊦ #(σ + σ1) = # σ + # σ1; (s) ⊦ ⌜m + n⌝ = ⌜m⌝ + ⌜n⌝ ; (s) ⊦ ⌜n⌝ < ⌜1⌝ + n∞ ↔ ¬ n∞ < ⌜n⌝ ; (s)

Proof step 28 from proof hpal-next-auxh (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 29:

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

• Proof step 30:

  x1 ≠ [], n < # x1, n < # x1 + # x2, ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n, ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b), ∀ n. ⌜n⌝ < #(⌜a '⌝ + ⌜x1⌝ + ⌜x2⌝ ) → dom(g)((⌜a '⌝ + ⌜x1⌝ + ⌜x2⌝ )[n]), ∀ n. ⌜n + 1⌝ < #(⌜a '⌝ + ⌜x1⌝ + ⌜x2⌝ ) → edge(g)((⌜a '⌝ + ⌜x1⌝ + ⌜x2⌝ )[n], (⌜a '⌝ + ⌜x1⌝ + ⌜x2⌝ )[n + 1]), ¬(¬ # x1 < n0 → dom(g)((a ' + x1)[n0])) ∨ ¬(n1 < # x1 → edge(g)((a ' + x1)[n1], x1[n1])) ⊦

Rule argument

Additional information

Used terms: ⌜a '⌝ + ⌜x1⌝ + ⌜x2⌝ , g

Proof step 29 from proof hpal-next-auxh (previous step) (back to tree)

A spec-lemma

Proof step 30 from proof hpal-next-auxh (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

  x1 ≠ [], n < # x1 + # x2, n < # x1, ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b), ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n, ∀ n2. n2 < # x1 + # x2 → edge(g)((a ' + x1 + x2)[n2], (x1 + x2)[n2]), ∀ n2. ¬ # x1 + # x2 < n2 → dom(g)((a ' + x1 + x2)[n2]), ¬(¬ # x1 < n0 → dom(g)((a ' + x1)[n0])) ∨ ¬(n1 < # x1 → edge(g)((a ' + x1)[n1], x1[n1])) ⊦

Rule argument

Additional information

Used simplifier rules: append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ (⌜x⌝ + ⌜x0⌝ + ⌜x1⌝ )[m] = (x + x0 + x1)[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 ⊦ ⌜n⌝ + ⌜m⌝ < ⌜n0⌝ ↔ n + m < n0; (s) ⊦ ⌜n⌝ < ⌜1⌝ + n∞ ↔ ¬ n∞ < ⌜n⌝ ; (s) ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s) ⊦ #(σ + σ1) = # σ + # σ1; (s) ⊦ # a ' = 0 +1; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ (⌜x⌝ + ⌜x0⌝ )[m] = (x + x0)[m]; (s) ⊦ (⌜a '⌝ + σ)[n + 1] = σ[n]; (s) ⊦ ⌜n⌝ < ⌜m⌝ + ⌜n0⌝ ↔ n < m + n0; (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 31 from proof hpal-next-auxh (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 32:

  x1 ≠ [], n < # x1, n < # x1 + # x2, ¬ # x1 < n0, ¬ dom(g)((a ' + x1)[n0]), ∀ n2. ¬ # x1 + # x2 < n2 → dom(g)((a ' + x1 + x2)[n2]), ∀ n2. n2 < # x1 + # x2 → edge(g)((a ' + x1 + x2)[n2], (x1 + x2)[n2]), ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n, ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b) ⊦

• Proof step 39:

  x1 ≠ [], n1 < # x1, n < # x1, n < # x1 + # x2, ¬ edge(g)((a ' + x1)[n1], x1[n1]), ∀ n2. ¬ # x1 + # x2 < n2 → dom(g)((a ' + x1 + x2)[n2]), ∀ n2. n2 < # x1 + # x2 → edge(g)((a ' + x1 + x2)[n2], (x1 + x2)[n2]), ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n, ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b) ⊦

Rule argument

Additional information

Proof step 32 from proof hpal-next-auxh (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 33:

  x1 ≠ [], n < # x1 + # x2, n < # x1, n0 ≤ # x1, ¬ dom(g)((a ' + x1)[n0]), ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b), ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n, ∀ n2. n2 < # x1 + # x2 → edge(g)((a ' + x1 + x2)[n2], (x1 + x2)[n2]), ∀ n2. ¬ # x1 + # x2 < n2 → dom(g)((a ' + x1 + x2)[n2]) ⊦

Rule argument

Additional information

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

Proof step 33 from proof hpal-next-auxh (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 34:

  x1 ≠ [], n < # x1, n < # x1 + # x2, n0 ≤ # x1, ¬ dom(g)((a ' + x1)[n0]), ¬ # x1 + # x2 < n0 → dom(g)((a ' + x1 + x2)[n0]), ∀ n2. n2 < # x1 + # x2 → edge(g)((a ' + x1 + x2)[n2], (x1 + x2)[n2]), ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n, ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b) ⊦

Rule argument

Additional information

Used terms: n0

Proof step 34 from proof hpal-next-auxh (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 35:

  x1 ≠ [], n < # x1, n < # x1 + # x2, dom(g)((a ' + x1 + x2)[n0]), n0 ≤ # x1, n0 ≤ # x1 + # x2, ¬ dom(g)((a ' + x1)[n0]), ∀ n2. n2 < # x1 + # x2 → edge(g)((a ' + x1 + x2)[n2], (x1 + x2)[n2]), ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n, ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n ↔ ¬ n ≤ m; (ss) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ ¬ m + n < m; (s) ⊦ m +1 = m + 1; (s) ⊦ m < n → n ≠ 0; (s) fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic 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

Proof step 35 from proof hpal-next-auxh (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 36:

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

• Proof step 37:

  x1 ≠ [], n < # x1 + # x2, n < # x1, dom(g)((a ' + x1 + x2)[n0]), n0 ≤ # x1 + # x2, n0 ≤ # x1, ¬ n0 < # a ', ¬ dom(g)((a ' + x1)[n0]), ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b), ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n, ∀ n2. n2 < # x1 + # x2 → edge(g)((a ' + x1 + x2)[n2], (x1 + x2)[n2]) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # a ' = 0 +1; (s) ⊦ m < 1 ↔ m = 0; (s) ⊦ a '[0] = a; (s) ⊦ 0 ≤ m; (s) ⊦ (a ' + x)[0] = a; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: a ', x1 + x2, n0

Proof step 36 from proof hpal-next-auxh (previous step) (back to tree)

A spec-lemma

Proof step 37 from proof hpal-next-auxh (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 38:

  n0 ≠ 0, x1 ≠ [], n < # x1, n < # x1 + # x2, dom(g)((x1 + x2)[n0 - 1]), n0 ≤ # x1, n0 ≤ # x1 + # x2, ¬ dom(g)((a ' + x1)[n0]), ∀ n2. n2 < # x1 + # x2 → edge(g)((a ' + x1 + x2)[n2], (x1 + x2)[n2]), ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n, ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b) ⊦

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 38 from proof hpal-next-auxh (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m + 1 ≠ 0; (s) ⊦ m + 1 ≤ n ↔ m < n; (s) ⊦ n < # x → (x + y)[n] = x[n]; (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 n ≠ 0 ⊦ m = n - 1 ↔ n = m + 1; (elim) Used terms: n0, m

Proof step 39 from proof hpal-next-auxh (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 40:

  x1 ≠ [], n < # x1 + # x2, n < # x1, n1 < # x1, ¬ edge(g)((a ' + x1)[n1], x1[n1]), ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b), ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n, ∀ n2. n2 < # x1 + # x2 → edge(g)((a ' + x1 + x2)[n2], (x1 + x2)[n2]), ∀ n2. ¬ # x1 + # x2 < n2 → dom(g)((a ' + x1 + x2)[n2]) ⊦

Rule argument

Additional information

Proof step 40 from proof hpal-next-auxh (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 41:

  x1 ≠ [], n1 < # x1, n < # x1, n < # x1 + # x2, ¬ edge(g)((a ' + x1)[n1], x1[n1]), n1 < # x1 + # x2 → edge(g)((a ' + x1 + x2)[n1], (x1 + x2)[n1]), ∀ n2. ¬ # x1 + # x2 < n2 → dom(g)((a ' + x1 + x2)[n2]), ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n, ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b) ⊦

Rule argument

Additional information

Used terms: n1

Proof step 41 from proof hpal-next-auxh (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 42:

  x1 ≠ [], n1 < # x1, n < # x1, n < # x1 + # x2, n1 < # x1 + # x2, edge(g)((a ' + x1 + x2)[n1], x1[n1]), ¬ edge(g)((a ' + x1)[n1], x1[n1]), ∀ n2. ¬ # x1 + # x2 < n2 → dom(g)((a ' + x1 + x2)[n2]), ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n, ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b) ⊦

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 + n < m; (s) fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat ⊦ m < n ↔ ¬ n ≤ m; (ss) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ n < # x → (x + y)[n] = x[n]; (s)

Proof step 42 from proof hpal-next-auxh (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 43:

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

• Proof step 44:

  x1 ≠ [], n1 < # x1 + # x2, n < # x1 + # x2, n < # x1, n1 < # x1, edge(g)((a ' + x1 + x2)[n1], x1[n1]), ¬ n1 < # a ', ¬ edge(g)((a ' + x1)[n1], x1[n1]), ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b), ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n, ∀ n2. ¬ # x1 + # x2 < n2 → dom(g)((a ' + x1 + x2)[n2]) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # a ' = 0 +1; (s) ⊦ m < 1 ↔ m = 0; (s) lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic ⊦ a '[0] = a; (s) ⊦ m < n → n ≠ 0; (s) ⊦ 0 < m ↔ m ≠ 0; (s) ⊦ # x = 0 ↔ x = []; (s) ⊦ (a ' + x)[0] = a; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ x ≠ [] → x[0] = x.head; (s) Used terms: a ', x1 + x2, n1

Proof step 43 from proof hpal-next-auxh (previous step) (back to tree)

A spec-lemma

Proof step 44 from proof hpal-next-auxh (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 45:

  n1 ≠ 0, x1 ≠ [], n1 < # x1, n < # x1, n < # x1 + # x2, n1 < # x1 + # x2, edge(g)((x1 + x2)[n1 - 1], x1[n1]), ¬ edge(g)((a ' + x1)[n1], x1[n1]), ∀ n2. ¬ # x1 + # x2 < n2 → dom(g)((a ' + x1 + x2)[n2]), ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n, ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b) ⊦

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 45 from proof hpal-next-auxh (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 46:

  n1 = m + 1, n1 ≠ 0, x1 ≠ [], n1 < # x1 + # x2, n < # x1 + # x2, n < # x1, n1 < # x1, edge(g)((x1 + x2)[m], x1[n1]), ¬ edge(g)((a ' + x1)[n1], x1[n1]), ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b), ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n, ∀ n2. ¬ # x1 + # x2 < n2 → dom(g)((a ' + x1 + x2)[n2]) ⊦

Rule argument

Additional information

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

Proof step 46 from proof hpal-next-auxh (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 47:

  x1 ≠ [], m + 1 < # x1, n < # x1, n < # x1 + # x2, edge(g)((x1 + x2)[m], x1[m + 1]), ¬ edge(g)(x1[m], x1[m + 1]), ∀ n2. ¬ # x1 + # x2 < n2 → dom(g)((a ' + x1 + x2)[n2]), ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n, ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b) ⊦

Rule argument

Additional information

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

Proof step 47 from proof hpal-next-auxh (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]

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ n < # x → (x + y)[n] = y[n - # x]; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ ¬ 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: x1, x2, m

Proof step 48 from proof hpal-next-auxh (previous step) (back to tree)

A spec-lemma

Proof step 49 from proof hpal-next-auxh (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 50:

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

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 50 from proof hpal-next-auxh (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) = (# x)+1; (s) a: ⊦ (x + y) + z = x + y + z; from specification list f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic trans-nat: ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward) from specification nat-basic ⊦ m < n → n ≠ 0; (s) ⊦ m +1 = m + 1; (s) ⊦ m + m0 < n → ¬ n + n0 < m; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: a0 ' + x0

Proof step 51 from proof hpal-next-auxh (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 52:

  n0 ≤ n, ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b), ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n ⊦ ∃ n. ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ (x.head = a ∨ x.head ∈ s0) → # x < n, ∃ x. x.head = a ∧ # x = n0 + 1 ∧ pathp(g)(⌜x⌝ )

Rule argument

Additional information

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

Proof step 52 from proof hpal-next-auxh (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 53:

  n0 ≤ n, ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n, ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b) ⊦ ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ (x.head = a ∨ x.head ∈ s0) → # x < n + 1, ∃ x. x.head = a ∧ # x = n0 + 1 ∧ pathp(g)(⌜x⌝ )

Rule argument

Additional information

Used terms: n + 1

Proof step 53 from proof hpal-next-auxh (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 54:

  x ≠ [], n0 < # x, n < # x, pathp(g)(⌜x⌝ ), n0 ≤ n, ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n, ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b), x.head = a ∨ x.head ∈ s0 ⊦ ∃ x. x.head = a ∧ # x = n0 + 1 ∧ pathp(g)(⌜x⌝ )

Rule argument

Additional information

Used simplifier rules: ⊦ # x = 0 ↔ x = []; (s) fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat 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 < n + 1 ↔ ¬ n < m; (s)

Proof step 54 from proof hpal-next-auxh (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 55:

  x = a0 + x0, x ≠ [], n < # x, n0 < # x, pathp(g)(⌜x⌝ ), n0 ≤ n, ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b), ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n, a0 = a ∨ a0 ∈ s0 ⊦ ∃ x. x.head = a ∧ # x = n0 + 1 ∧ pathp(g)(⌜x⌝ )

Rule argument

Additional information

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

Proof step 55 from proof hpal-next-auxh (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 56:

  pathp(g)(⌜a0 '⌝ + ⌜x0⌝ ), n0 ≤ n, n ≤ # x0, n0 ≤ # x0, ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n, ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b), a0 = a ∨ a0 ∈ s0 ⊦ ∃ x. x.head = a ∧ # x = n0 + 1 ∧ pathp(g)(⌜x⌝ )

Rule argument

Additional information

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

Proof step 56 from proof hpal-next-auxh (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 57:

  pathp(g)(⌜a0 '⌝ + ⌜x0⌝ ), n0 ≤ # x0, n ≤ # x0, n0 ≤ n, ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b), ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n, a0 = a ∨ a0 ∈ s0 ⊦ ((a0 ' + x0).take(n0 + 1)).head = a ∧ # (a0 ' + x0).take(n0 + 1) = n0 + 1 ∧ pathp(g)(⌜(a0 ' + x0).take(n0 + 1)⌝ )

Rule argument

Additional information

Used terms: (a0 ' + x0).take(n0 + 1)

Proof step 57 from proof hpal-next-auxh (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 58:

  pathp(g)(⌜a0 '⌝ + ⌜x0⌝ ), n0 ≤ n, n ≤ # x0, n0 ≤ # x0, ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n, ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b), a0 = a ∨ a0 ∈ s0 ⊦ a0 = a ∧ pathp(g)(⌜a '⌝ + ⌜x0.take(n0)⌝ )

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 58 from proof hpal-next-auxh (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 59:

  a0 = a, pathp(g)(⌜a0 '⌝ + ⌜x0⌝ ), n0 ≤ # x0, n ≤ # x0, n0 ≤ n, ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b), ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n ⊦ a0 = a ∧ pathp(g)(⌜a '⌝ + ⌜x0.take(n0)⌝ )

• Proof step 88:

  pathp(g)(⌜a0 '⌝ + ⌜x0⌝ ), a0 ∈ s0, n0 ≤ # x0, n ≤ # x0, n0 ≤ n, ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b), ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n ⊦ a0 = a ∧ pathp(g)(⌜a '⌝ + ⌜x0.take(n0)⌝ )

Rule argument

Additional information

Proof step 59 from proof hpal-next-auxh (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 60:

  pathp(g)(⌜a '⌝ + ⌜x0⌝ ), n0 ≤ n, n ≤ # x0, n0 ≤ # x0, ¬ pathp(g)(⌜a '⌝ + ⌜x0.take(n0)⌝ ), ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n, ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b) ⊦

Rule argument

Additional information

Proof step 60 from proof hpal-next-auxh (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 61:

  # x1 = n0, x0 = x1 + x2, pathp(g)(⌜a '⌝ + ⌜x0⌝ ), n0 ≤ # x0, n ≤ # x0, n0 ≤ n, ¬ pathp(g)(⌜a '⌝ + ⌜x1⌝ ), ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b), ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ n ≤ # x → (y = x.take(n) ∧ z = x.drop(n) ↔ x = y + z ∧ # y = n); (elim) Used terms: n0, x0, x1, x2

Proof step 61 from proof hpal-next-auxh (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 62:

  pathp(g)(⌜a '⌝ + ⌜x1⌝ + ⌜x2⌝ ), n ≤ # x1 + # x2, # x1 ≤ n, ¬ pathp(g)(⌜a '⌝ + ⌜x1⌝ ), ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b), ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n ⊦

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 ≤ m + n; (s) let: ⊦ n ≤ n0 ∧ n0 ≤ n1 → n ≤ n1; (forward) from specification nat append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ ⌜x + y⌝ = ⌜x⌝ + ⌜y⌝ ; (s) ⊦ #(x + y) = # x + # y; (s)

Proof step 62 from proof hpal-next-auxh (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 63:

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

• Proof step 64:

  # x1 ≤ n, n ≤ # x1 + # x2, ¬ pathp(g)(⌜a '⌝ + ⌜x1⌝ ), ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n, ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b), ∀ n. ⌜n⌝ < #(⌜a '⌝ + ⌜x1⌝ + ⌜x2⌝ ) → dom(g)((⌜a '⌝ + ⌜x1⌝ + ⌜x2⌝ )[n]), ∀ n. ⌜n + 1⌝ < #(⌜a '⌝ + ⌜x1⌝ + ⌜x2⌝ ) → edge(g)((⌜a '⌝ + ⌜x1⌝ + ⌜x2⌝ )[n], (⌜a '⌝ + ⌜x1⌝ + ⌜x2⌝ )[n + 1]) ⊦

Rule argument

Additional information

Used terms: ⌜a '⌝ + ⌜x1⌝ + ⌜x2⌝ , g

Proof step 63 from proof hpal-next-auxh (previous step) (back to tree)

A spec-lemma

Proof step 64 from proof hpal-next-auxh (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 65:

  n ≤ # x1 + # x2, # x1 ≤ n, ¬ pathp(g)(⌜a '⌝ + ⌜x1⌝ ), ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b), ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n, ∀ n0. n0 < # x1 + # x2 → edge(g)((a ' + x1 + x2)[n0], (x1 + x2)[n0]), ∀ n0. ¬ # x1 + # x2 < n0 → dom(g)((a ' + x1 + x2)[n0]) ⊦

Rule argument

Additional information

Used simplifier rules: append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ (⌜x⌝ + ⌜x0⌝ + ⌜x1⌝ )[m] = (x + x0 + x1)[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 ⊦ ⌜n⌝ + ⌜m⌝ < ⌜n0⌝ ↔ n + m < n0; (s) ⊦ ⌜n⌝ < ⌜1⌝ + n∞ ↔ ¬ n∞ < ⌜n⌝ ; (s) ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s) ⊦ #(σ + σ1) = # σ + # σ1; (s) ⊦ # a ' = 0 +1; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ (⌜x⌝ + ⌜x0⌝ )[m] = (x + x0)[m]; (s) ⊦ (⌜a '⌝ + σ)[n + 1] = σ[n]; (s) ⊦ ⌜n⌝ < ⌜m⌝ + ⌜n0⌝ ↔ n < m + n0; (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 65 from proof hpal-next-auxh (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 66:

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

• Proof step 67:

  # x1 ≤ n, n ≤ # x1 + # x2, ∀ n0. ¬ # x1 + # x2 < n0 → dom(g)((a ' + x1 + x2)[n0]), ∀ n0. n0 < # x1 + # x2 → edge(g)((a ' + x1 + x2)[n0], (x1 + x2)[n0]), ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n, ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b), (∃ n. ¬(⌜n⌝ < #(⌜a '⌝ + ⌜x1⌝ ) → dom(g)((⌜a '⌝ + ⌜x1⌝ )[n]))) ∨ (∃ n. ¬(⌜n + 1⌝ < #(⌜a '⌝ + ⌜x1⌝ ) → edge(g)((⌜a '⌝ + ⌜x1⌝ )[n], (⌜a '⌝ + ⌜x1⌝ )[n + 1]))) ⊦

Rule argument

Additional information

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

Proof step 66 from proof hpal-next-auxh (previous step) (back to tree)

A spec-lemma

Proof step 67 from proof hpal-next-auxh (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 68:

  n ≤ # x1 + # x2, # x1 ≤ n, ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b), ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n, ∀ n0. n0 < # x1 + # x2 → edge(g)((a ' + x1 + x2)[n0], (x1 + x2)[n0]), ∀ n0. ¬ # x1 + # x2 < n0 → dom(g)((a ' + x1 + x2)[n0]), ¬(¬ # x1 < n0 → dom(g)((a ' + x1)[n0])) ∨ ¬(n1 < # x1 → edge(g)((a ' + x1)[n1], x1[n1])) ⊦

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) ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s) ⊦ # a ' = 0 +1; (s) ⊦ #(σ + σ1) = # σ + # σ1; (s) ⊦ ⌜m + n⌝ = ⌜m⌝ + ⌜n⌝ ; (s) ⊦ ⌜n⌝ < ⌜1⌝ + n∞ ↔ ¬ n∞ < ⌜n⌝ ; (s)

Proof step 68 from proof hpal-next-auxh (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 69:

  # x1 ≤ n, n ≤ # x1 + # x2, ¬ # x1 < n0, ¬ dom(g)((a ' + x1)[n0]), ∀ n0. ¬ # x1 + # x2 < n0 → dom(g)((a ' + x1 + x2)[n0]), ∀ n0. n0 < # x1 + # x2 → edge(g)((a ' + x1 + x2)[n0], (x1 + x2)[n0]), ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n, ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b) ⊦

• Proof step 78:

  n1 < # x1, # x1 ≤ n, n ≤ # x1 + # x2, ¬ edge(g)((a ' + x1)[n1], x1[n1]), ∀ n0. ¬ # x1 + # x2 < n0 → dom(g)((a ' + x1 + x2)[n0]), ∀ n0. n0 < # x1 + # x2 → edge(g)((a ' + x1 + x2)[n0], (x1 + x2)[n0]), ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n, ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b) ⊦

Rule argument

Additional information

Proof step 69 from proof hpal-next-auxh (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 70:

  n0 ≤ n, n0 ≤ # x1, # x1 ≤ n, n ≤ # x1 + # x2, n0 ≤ # x1 + # x2, ¬ dom(g)((a ' + x1)[n0]), ∀ n0. ¬ # x1 + # x2 < n0 → dom(g)((a ' + x1 + x2)[n0]), ∀ n0. n0 < # x1 + # x2 → edge(g)((a ' + x1 + x2)[n0], (x1 + x2)[n0]), ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n, ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b) ⊦

Rule argument

Additional information

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

Proof step 70 from proof hpal-next-auxh (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 71:

  n0 ≤ # x1 + # x2, n ≤ # x1 + # x2, # x1 ≤ n, n0 ≤ # x1, n0 ≤ n, ¬ dom(g)((a ' + x1)[n0]), ¬ # x1 + # x2 < n0 → dom(g)((a ' + x1 + x2)[n0]), ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b), ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n, ∀ n0. n0 < # x1 + # x2 → edge(g)((a ' + x1 + x2)[n0], (x1 + x2)[n0]) ⊦

Rule argument

Additional information

Used terms: n0

Proof step 71 from proof hpal-next-auxh (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 72:

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

• Proof step 73:

  n0 ≤ n, n0 ≤ # x1, # x1 ≤ n, n ≤ # x1 + # x2, n0 ≤ # x1 + # x2, ¬ n0 < # a ', ¬ dom(g)((a ' + x1)[n0]), ¬ # x1 + # x2 < n0 → dom(g)((a ' + x1 + x2)[n0]), ∀ n0. n0 < # x1 + # x2 → edge(g)((a ' + x1 + x2)[n0], (x1 + x2)[n0]), ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n, ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # a ' = 0 +1; (s) ⊦ m < 1 ↔ m = 0; (s) ⊦ m ≤ n → (n < m ↔ false); (s) ⊦ a '[0] = a; (s) ⊦ 0 ≤ m; (s) ⊦ (a ' + x)[0] = a; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: a ', x1 + x2, n0

Proof step 72 from proof hpal-next-auxh (previous step) (back to tree)

A spec-lemma

Proof step 73 from proof hpal-next-auxh (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 74:

  n0 ≠ 0, dom(g)((a ' + x1 + x2)[n0]), n0 ≤ # x1 + # x2, n ≤ # x1 + # x2, # x1 ≤ n, n0 ≤ # x1, n0 ≤ n, ¬ dom(g)((a ' + x1)[n0]), ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b), ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n, ∀ n0. n0 < # x1 + # x2 → edge(g)((a ' + x1 + x2)[n0], (x1 + x2)[n0]) ⊦

Rule argument

Additional information

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

Proof step 74 from proof hpal-next-auxh (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 75:

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

• Proof step 76:

  n0 ≠ 0, dom(g)((a ' + x1 + x2)[n0]), n0 ≤ n, n0 ≤ # x1, # x1 ≤ n, n ≤ # x1 + # x2, n0 ≤ # x1 + # x2, ¬ n0 < # a ', ¬ dom(g)((a ' + x1)[n0]), ∀ n0. n0 < # x1 + # x2 → edge(g)((a ' + x1 + x2)[n0], (x1 + x2)[n0]), ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n, ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b) ⊦

Rule argument

Additional information

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

Proof step 75 from proof hpal-next-auxh (previous step) (back to tree)

A spec-lemma

Proof step 76 from proof hpal-next-auxh (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 77:

  n0 ≠ 0, dom(g)((x1 + x2)[n0 - 1]), n0 ≤ # x1 + # x2, n ≤ # x1 + # x2, # x1 ≤ n, n0 ≤ # x1, n0 ≤ n, ¬ dom(g)((a ' + x1)[n0]), ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b), ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n, ∀ n0. n0 < # x1 + # x2 → edge(g)((a ' + x1 + x2)[n0], (x1 + x2)[n0]) ⊦

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 77 from proof hpal-next-auxh (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m + 1 ≠ 0; (s) ⊦ m + 1 ≤ n ↔ m < n; (s) ⊦ n < # x → (x + y)[n] = x[n]; (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 n ≠ 0 ⊦ m = n - 1 ↔ n = m + 1; (elim) Used terms: n0, m

Proof step 78 from proof hpal-next-auxh (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 79:

  x1 ≠ [], n1 < n, n1 < # x1, n1 < # x1 + # x2, # x1 ≤ n, n ≤ # x1 + # x2, ¬ edge(g)((a ' + x1)[n1], x1[n1]), ∀ n0. ¬ # x1 + # x2 < n0 → dom(g)((a ' + x1 + x2)[n0]), ∀ n0. n0 < # x1 + # x2 → edge(g)((a ' + x1 + x2)[n0], (x1 + x2)[n0]), ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n, ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat ⊦ # x = 0 ↔ x = []; (s)

Proof step 79 from proof hpal-next-auxh (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 80:

  x1 ≠ [], n1 < # x1 + # x2, n1 < # x1, n1 < n, n ≤ # x1 + # x2, # x1 ≤ n, ¬ edge(g)((a ' + x1)[n1], x1[n1]), n1 < # x1 + # x2 → edge(g)((a ' + x1 + x2)[n1], (x1 + x2)[n1]), ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b), ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n, ∀ n0. ¬ # x1 + # x2 < n0 → dom(g)((a ' + x1 + x2)[n0]) ⊦

Rule argument

Additional information

Used terms: n1

Proof step 80 from proof hpal-next-auxh (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 81:

  x1 ≠ [], n1 < n, n1 < # x1, n1 < # x1 + # x2, edge(g)((a ' + x1 + x2)[n1], x1[n1]), # x1 ≤ n, n ≤ # x1 + # x2, ¬ edge(g)((a ' + x1)[n1], x1[n1]), ∀ n0. ¬ # x1 + # x2 < n0 → dom(g)((a ' + x1 + x2)[n0]), ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n, ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ n < # x → (x + y)[n] = x[n]; (s)

Proof step 81 from proof hpal-next-auxh (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 82:

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

• Proof step 83:

  x1 ≠ [], n1 < # x1 + # x2, n1 < # x1, n1 < n, edge(g)((a ' + x1 + x2)[n1], x1[n1]), n ≤ # x1 + # x2, # x1 ≤ n, ¬ n1 < # a ', ¬ edge(g)((a ' + x1)[n1], x1[n1]), ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b), ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n, ∀ n0. ¬ # x1 + # x2 < n0 → dom(g)((a ' + x1 + x2)[n0]) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # a ' = 0 +1; (s) ⊦ m < 1 ↔ m = 0; (s) lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic ⊦ m < n → n ≠ 0; (s) ⊦ a '[0] = a; (s) ⊦ # x = 0 ↔ x = []; (s) ⊦ 0 < m ↔ m ≠ 0; (s) ⊦ (a ' + x)[0] = a; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ x ≠ [] → x[0] = x.head; (s) Used terms: a ', x1 + x2, n1

Proof step 82 from proof hpal-next-auxh (previous step) (back to tree)

A spec-lemma

Proof step 83 from proof hpal-next-auxh (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 84:

  n1 ≠ 0, x1 ≠ [], n1 < n, n1 < # x1, n1 < # x1 + # x2, edge(g)((x1 + x2)[n1 - 1], x1[n1]), # x1 ≤ n, n ≤ # x1 + # x2, ¬ edge(g)((a ' + x1)[n1], x1[n1]), ∀ n0. ¬ # x1 + # x2 < n0 → dom(g)((a ' + x1 + x2)[n0]), ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n, ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b) ⊦

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 84 from proof hpal-next-auxh (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 85:

  n1 = m + 1, n1 ≠ 0, x1 ≠ [], n1 < # x1 + # x2, n1 < # x1, n1 < n, edge(g)((x1 + x2)[m], x1[n1]), n ≤ # x1 + # x2, # x1 ≤ n, ¬ edge(g)((a ' + x1)[n1], x1[n1]), ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b), ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n, ∀ n0. ¬ # x1 + # x2 < n0 → dom(g)((a ' + x1 + x2)[n0]) ⊦

Rule argument

Additional information

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

Proof step 85 from proof hpal-next-auxh (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 86:

  x1 ≠ [], m + 1 < n, m + 1 < # x1, edge(g)((x1 + x2)[m], x1[m + 1]), n ≤ # x1 + # x2, # x1 ≤ n, ¬ edge(g)(x1[m], x1[m + 1]), ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b), ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n, ∀ n0. ¬ # x1 + # x2 < n0 → dom(g)((a ' + x1 + x2)[n0]) ⊦

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 + n < m0 → m + n < m0 + n0; (s) fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ (a ' + x)[n + 1] = x[n]; (s) ⊦ m + 1 ≠ 0; (s)

Proof step 86 from proof hpal-next-auxh (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 87:

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

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ n < # x → (x + y)[n] = y[n - # x]; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ ¬ 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: x1, x2, m

Proof step 87 from proof hpal-next-auxh (previous step) (back to tree)

A spec-lemma

Proof step 88 from proof hpal-next-auxh (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 89:

  # s0 ≠ 0, s0 ≠ ∅, pathp(g)(⌜a0 '⌝ + ⌜x0⌝ ), a0 ∈ s0, n0 ≤ # x0, n ≤ # x0, n0 ≤ n, ∀ b. b ∈ s0 → ¬ haspathanylength(g)(b), ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s0 → # x < n ⊦ a0 = a ∧ pathp(g)(⌜a '⌝ + ⌜x0.take(n0)⌝ )

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 89 from proof hpal-next-auxh (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) = (# x)+1; (s) ⊦ m +1 = m + 1; (s) a: ⊦ (x + y) + z = x + y + z; from specification list f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat ⊦ m < n → n ≠ 0; (s) ⊦ ¬ m + n < m; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: a0 ' + x0