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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  haspathanylength(g)(a), ∀ b. b ∈ s → ¬ haspathanylength(g)(b), ∀ b. edge(g)(a, b) ↔ b ∈ s ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  haspathanylength(g)(a), ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ b. b ∈ s → ¬ haspathanylength(g)(b) ⊦

Rule argument

Additional information

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 4:

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

• Proof step 5:

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

Rule argument

Additional information

Used terms: s, g

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

Lemma hpal-next-auxh

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

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

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

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

• Proof step 8:

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

Rule argument

Additional information

Used terms: a, g

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

Lemma haspathanylength-def

Proof step 8 from proof hpal-next-aux (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 9:

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

Rule argument

Additional information

Used terms: n + 1

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  # x = 2 + n, pathp(g)(⌜x⌝ ), ∀ b. b ∈ s → ¬ haspathanylength(g)(b), ∀ b. edge(g)(x.head, b) ↔ b ∈ s, ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s → # x < n ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 11:

  # x = 2 + n, x = a + x0, x ≠ [], pathp(g)(⌜x⌝ ), ∀ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ x.head ∈ s → # x < n, ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ b. b ∈ s → ¬ haspathanylength(g)(b) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # [] = 0; (s) ⊦ m + n = 0 ↔ m = 0 ∧ n = 0; (ws) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic x ≠ [] ⊦ a = x.head ∧ y = x.tail ↔ x = a + y; (elim) Used terms: x, a, x0

Proof step 11 from proof hpal-next-aux (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

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

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ ⌜x + y⌝ = ⌜x⌝ + ⌜y⌝ ; (s) ⊦ a + x = a ' + x; (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 n < n0 ⊦ m + (* n) = m0 + (* n0) ↔ m = m0 + (n0 - n); (s) ⊦ m +1 = m + 1; (s) ⊦ #(a ' + x) = (# x)+1; (s)

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

User applied rule all left

And obtained the following new goals

• Proof step 13:

  # x0 = n + 1, pathp(g)(⌜a '⌝ + ⌜x0⌝ ), pathp(g)(⌜x0⌝ ) ∧ x0 ≠ [] ∧ x0.head ∈ s → # x0 < n, ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ b. b ∈ s → ¬ haspathanylength(g)(b) ⊦

Rule argument

Additional information

Used terms: x0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  # x0 = n + 1, x0 ≠ [], pathp(g)(⌜a '⌝ + ⌜x0⌝ ), ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ b. b ∈ s → ¬ haspathanylength(g)(b) ⊦ x0.head ∈ s ∧ pathp(g)(⌜x0⌝ )

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 = 0 ↔ m = 0 ∧ n = 0; (ws) ⊦ # [] = 0; (s) ⊦ ¬ m + n < m; (s)

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 15:

  # x0 = n + 1, x0 = a0 + x1, x0 ≠ [], pathp(g)(⌜a '⌝ + ⌜x0⌝ ), ∀ b. b ∈ s → ¬ haspathanylength(g)(b), ∀ b. edge(g)(a, b) ↔ b ∈ s ⊦ a0 ∈ s ∧ pathp(g)(⌜x0⌝ )

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  pathp(g)(⌜a '⌝ + ⌜a0 '⌝ + ⌜x1⌝ ), ∀ b. b ∈ s → ¬ haspathanylength(g)(b), ∀ b. edge(g)(a, b) ↔ b ∈ s ⊦ a0 ∈ s ∧ pathp(g)(⌜a0 '⌝ + ⌜x1⌝ )

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ ⌜x + y⌝ = ⌜x⌝ + ⌜y⌝ ; (s) ⊦ a + x = a ' + x; (s) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ 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 16 from proof hpal-next-aux (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 17:

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

• Proof step 18:

  ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ b. b ∈ s → ¬ haspathanylength(g)(b), ∀ n. ⌜n⌝ < #(⌜a '⌝ + ⌜a0 '⌝ + ⌜x1⌝ ) → dom(g)((⌜a '⌝ + ⌜a0 '⌝ + ⌜x1⌝ )[n]), ∀ n. ⌜n + 1⌝ < #(⌜a '⌝ + ⌜a0 '⌝ + ⌜x1⌝ ) → edge(g)((⌜a '⌝ + ⌜a0 '⌝ + ⌜x1⌝ )[n], (⌜a '⌝ + ⌜a0 '⌝ + ⌜x1⌝ )[n + 1]) ⊦ a0 ∈ s ∧ pathp(g)(⌜a0 '⌝ + ⌜x1⌝ )

Rule argument

Additional information

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

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  ∀ b. b ∈ s → ¬ haspathanylength(g)(b), ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ n. ¬ # x1 < n → edge(g)((a ' + a0 ' + x1)[n], (a0 ' + x1)[n]), ∀ n. n < 2 + # x1 → dom(g)((a ' + a0 ' + x1)[n]) ⊦ a0 ∈ s ∧ pathp(g)(⌜a0 '⌝ + ⌜x1⌝ )

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) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ ⌜(* n)⌝ + ⌜(* m)⌝ = ⌜n + m⌝ ; (s) ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s) ⊦ # a ' = 0 +1; (s) ⊦ #(σ + σ1) = # σ + # σ1; (s) ⊦ (⌜x⌝ + ⌜x0⌝ )[m] = (x + x0)[m]; (s) ⊦ (⌜a '⌝ + σ)[n + 1] = σ[n]; (s) ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) ⊦ ⌜n⌝ < ⌜1⌝ + n∞ ↔ ¬ n∞ < ⌜n⌝ ; (s) ⊦ m ≤ n → (⌜(* m)⌝ + n∞2 < ⌜(* n)⌝ + n∞1 ↔ n∞2 < ⌜n - m⌝ + n∞1); (s) ⊦ ⌜m + n⌝ = ⌜m⌝ + ⌜n⌝ ; (s)

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

User applied rule all left

And obtained the following new goals

• Proof step 20:

  ¬ # x1 < 0 → edge(g)((a ' + a0 ' + x1)[0], (a0 ' + x1)[0]), ∀ n. n < 2 + # x1 → dom(g)((a ' + a0 ' + x1)[n]), ∀ n. ¬ # x1 < n → edge(g)((a ' + a0 ' + x1)[n], (a0 ' + x1)[n]), ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ b. b ∈ s → ¬ haspathanylength(g)(b) ⊦ a0 ∈ s ∧ pathp(g)(⌜a0 '⌝ + ⌜x1⌝ )

Rule argument

Additional information

Used terms: 0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  edge(g)(a, a0), ∀ b. b ∈ s → ¬ haspathanylength(g)(b), ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ n. ¬ # x1 < n → edge(g)((a ' + a0 ' + x1)[n], (a0 ' + x1)[n]), ∀ n. n < 2 + # x1 → dom(g)((a ' + a0 ' + x1)[n]) ⊦ a0 ∈ s ∧ pathp(g)(⌜a0 '⌝ + ⌜x1⌝ )

Rule argument

Additional information

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

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

User applied rule all left

And obtained the following new goals

• Proof step 22:

  edge(g)(a, a0) ↔ a0 ∈ s, edge(g)(a, a0), ∀ n. n < 2 + # x1 → dom(g)((a ' + a0 ' + x1)[n]), ∀ n. ¬ # x1 < n → edge(g)((a ' + a0 ' + x1)[n], (a0 ' + x1)[n]), ∀ b. b ∈ s → ¬ haspathanylength(g)(b) ⊦ a0 ∈ s ∧ pathp(g)(⌜a0 '⌝ + ⌜x1⌝ )

Rule argument

Additional information

Used terms: a0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  # s ≠ 0, s ≠ ∅, edge(g)(a, a0), a0 ∈ s, ¬ pathp(g)(⌜a0 '⌝ + ⌜x1⌝ ), ∀ n. n < 2 + # x1 → dom(g)((a ' + a0 ' + x1)[n]), ∀ n. ¬ # x1 < n → edge(g)((a ' + a0 ' + x1)[n], (a0 ' + x1)[n]), ∀ b. b ∈ s → ¬ haspathanylength(g)(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 23 from proof hpal-next-aux (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 24:

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

• Proof step 25:

  # s ≠ 0, s ≠ ∅, edge(g)(a, a0), a0 ∈ s, ∀ b. b ∈ s → ¬ haspathanylength(g)(b), ∀ n. ¬ # x1 < n → edge(g)((a ' + a0 ' + x1)[n], (a0 ' + x1)[n]), ∀ n. n < 2 + # x1 → dom(g)((a ' + a0 ' + x1)[n]), (∃ n. ¬(⌜n⌝ < #(⌜a0 '⌝ + ⌜x1⌝ ) → dom(g)((⌜a0 '⌝ + ⌜x1⌝ )[n]))) ∨ (∃ n. ¬(⌜n + 1⌝ < #(⌜a0 '⌝ + ⌜x1⌝ ) → edge(g)((⌜a0 '⌝ + ⌜x1⌝ )[n], (⌜a0 '⌝ + ⌜x1⌝ )[n + 1]))) ⊦

Rule argument

Additional information

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

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 26:

  # s ≠ 0, s ≠ ∅, edge(g)(a, a0), a0 ∈ s, ∀ n. n < 2 + # x1 → dom(g)((a ' + a0 ' + x1)[n]), ∀ n. ¬ # x1 < n → edge(g)((a ' + a0 ' + x1)[n], (a0 ' + x1)[n]), ∀ b. b ∈ s → ¬ haspathanylength(g)(b), ¬(¬ # x1 < n → dom(g)((a0 ' + x1)[n])) ∨ ¬(n0 < # x1 → edge(g)((a0 ' + x1)[n0], x1[n0])) ⊦

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

User applied rule case distinction

And obtained the following new goals

• Proof step 27:

  # s ≠ 0, s ≠ ∅, edge(g)(a, a0), a0 ∈ s, ¬ # x1 < n, ¬ dom(g)((a0 ' + x1)[n]), ∀ b. b ∈ s → ¬ haspathanylength(g)(b), ∀ n. ¬ # x1 < n → edge(g)((a ' + a0 ' + x1)[n], (a0 ' + x1)[n]), ∀ n. n < 2 + # x1 → dom(g)((a ' + a0 ' + x1)[n]) ⊦

• Proof step 29:

  # s ≠ 0, s ≠ ∅, n0 < # x1, edge(g)(a, a0), a0 ∈ s, ¬ edge(g)((a0 ' + x1)[n0], x1[n0]), ∀ b. b ∈ s → ¬ haspathanylength(g)(b), ∀ n. ¬ # x1 < n → edge(g)((a ' + a0 ' + x1)[n], (a0 ' + x1)[n]), ∀ n. n < 2 + # x1 → dom(g)((a ' + a0 ' + x1)[n]) ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

  # s ≠ 0, s ≠ ∅, edge(g)(a, a0), a0 ∈ s, n ≤ # x1, ¬ dom(g)((a0 ' + x1)[n]), ∀ n. n < 2 + # x1 → dom(g)((a ' + a0 ' + x1)[n]), ∀ n. ¬ # x1 < n → edge(g)((a ' + a0 ' + x1)[n], (a0 ' + x1)[n]), ∀ b. b ∈ s → ¬ haspathanylength(g)(b) ⊦

Rule argument

Additional information

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

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

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: n < n0 ⊦ m + (* n) < m0 + (* n0) ↔ m < m0 + (n0 - n); (s) ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ m ≤ n → (n < m ↔ false); (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: n + 1

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 30:

  # s ≠ 0, s ≠ ∅, x1 ≠ [], n0 < # x1, edge(g)(a, a0), a0 ∈ s, ¬ edge(g)((a0 ' + x1)[n0], x1[n0]), ∀ b. b ∈ s → ¬ haspathanylength(g)(b), ∀ n. ¬ # x1 < n → edge(g)((a ' + a0 ' + x1)[n], (a0 ' + x1)[n]), ∀ n. n < 2 + # x1 → dom(g)((a ' + a0 ' + x1)[n]) ⊦

Rule argument

Additional information

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

Proof step 30 from proof hpal-next-aux (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: n0 + 1