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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 2:

  x ≠ [], haspathanylength(g)(x.last), pathp(g)(⌜x⌝ ), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s ⊦ ∃ y. (∃ b. y = x + b ') ∧ pathp(g)(⌜y⌝ ) ∧ haspathanylength(g)(y.last)

Rule argument

Additional information

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

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

User applied rule all left

And obtained the following new goals

• Proof step 3:

  x ≠ [], haspathanylength(g)(x.last), pathp(g)(⌜x⌝ ), ∃ s. ∀ b. edge(g)(x.last, b) ↔ b ∈ s ⊦ ∃ y. (∃ b. y = x + b ') ∧ pathp(g)(⌜y⌝ ) ∧ haspathanylength(g)(y.last)

Rule argument

Additional information

Used terms: x.last

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  x ≠ [], haspathanylength(g)(x.last), pathp(g)(⌜x⌝ ), ∀ b. edge(g)(x.last, b) ↔ b ∈ s ⊦ ∃ y. (∃ b. y = x + b ') ∧ pathp(g)(⌜y⌝ ) ∧ haspathanylength(g)(y.last)

Rule argument

Additional information

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

User applied rule cut formula

And obtained the following new goals

• Proof step 5:

  x ≠ [], haspathanylength(g)(x.last), pathp(g)(⌜x⌝ ), ∀ b. edge(g)(x.last, b) ↔ b ∈ s, ∀ a. a ∈ s → ¬ haspathanylength(g)(a) ⊦ ∃ y. (∃ b. y = x + b ') ∧ pathp(g)(⌜y⌝ ) ∧ haspathanylength(g)(y.last)

• Proof step 9:

  x ≠ [], haspathanylength(g)(x.last), pathp(g)(⌜x⌝ ), ∀ b. edge(g)(x.last, b) ↔ b ∈ s ⊦ ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∃ y. (∃ b. y = x + b ') ∧ pathp(g)(⌜y⌝ ) ∧ haspathanylength(g)(y.last)

Rule argument

Additional information

Used formulas: ∀ a. a ∈ s → ¬ haspathanylength(g)(a)

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 6:

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

• Proof step 7:

  x ≠ [], haspathanylength(g)(x.last), pathp(g)(⌜x⌝ ), ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ b. edge(g)(x.last, b) ↔ b ∈ s ⊦ ∀ b. b ∈ s → ¬ haspathanylength(g)(b), ∃ y. (∃ b. y = x + b ') ∧ pathp(g)(⌜y⌝ ) ∧ haspathanylength(g)(y.last)

Rule argument

Additional information

Used terms: g, x.last, s

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

Lemma hpal-next-aux

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  # s ≠ 0, s ≠ ∅, x ≠ [], haspathanylength(g)(x.last), haspathanylength(g)(b), pathp(g)(⌜x⌝ ), b ∈ s, ∀ a. a ∈ s → ¬ haspathanylength(g)(a), ∀ b. edge(g)(x.last, b) ↔ b ∈ s ⊦ ∃ y. (∃ b. y = x + b ') ∧ pathp(g)(⌜y⌝ ) ∧ haspathanylength(g)(y.last)

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 (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 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  # s ≠ 0, s ≠ ∅, x ≠ [], haspathanylength(g)(x.last), haspathanylength(g)(a), pathp(g)(⌜x⌝ ), a ∈ s, ∀ b. edge(g)(x.last, b) ↔ b ∈ s ⊦ ∃ y. (∃ b. y = x + b ') ∧ pathp(g)(⌜y⌝ ) ∧ haspathanylength(g)(y.last)

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

User applied rule exists right

And obtained the following new goals

• Proof step 11:

  # s ≠ 0, s ≠ ∅, x ≠ [], haspathanylength(g)(a), haspathanylength(g)(x.last), pathp(g)(⌜x⌝ ), a ∈ s, ∀ b. edge(g)(x.last, b) ↔ b ∈ s ⊦ (∃ b. x + a ' = x + b ') ∧ pathp(g)(⌜x + a '⌝ ) ∧ haspathanylength(g)((x + a ').last)

Rule argument

Additional information

Used terms: x + a '

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  # s ≠ 0, s ≠ ∅, x ≠ [], haspathanylength(g)(x.last), haspathanylength(g)(a), pathp(g)(⌜x⌝ ), a ∈ s, ¬ pathp(g)(⌜x⌝ + ⌜a '⌝ ), ∀ b. edge(g)(x.last, b) ↔ b ∈ s ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ (x + a ').last = a; (s) ⊦ ⌜x + y⌝ = ⌜x⌝ + ⌜y⌝ ; (s) ⊦ a ' = a0 ' ↔ a = a0; (s) ⊦ # x = # z → (x + y = z + y0 ↔ x = z ∧ y = y0); (ws)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 13:

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

• Proof step 14:

  # s ≠ 0, s ≠ ∅, x ≠ [], haspathanylength(g)(a), haspathanylength(g)(x.last), a ∈ s, ¬ pathp(g)(⌜x⌝ + ⌜a '⌝ ), ∀ b. edge(g)(x.last, b) ↔ b ∈ s, ∀ n. ⌜n⌝ < # ⌜x⌝ → dom(g)(⌜x⌝ [n]), ∀ n. ⌜n + 1⌝ < # ⌜x⌝ → edge(g)(⌜x⌝ [n], ⌜x⌝ [n + 1]) ⊦

Rule argument

Additional information

Used terms: ⌜x⌝ , g

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  # s ≠ 0, s ≠ ∅, x ≠ [], haspathanylength(g)(x.last), haspathanylength(g)(a), a ∈ s, ¬ pathp(g)(⌜x⌝ + ⌜a '⌝ ), ∀ b. edge(g)(x.last, b) ↔ b ∈ s, ∀ n. n + 1 < # x → edge(g)(x[n], x[n + 1]), ∀ n. n < # x → dom(g)(x[n]) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜x⌝ [n] = x[n]; (s) ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) ⊦ # ⌜x⌝ = ⌜# x⌝ ; (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 ⊦ ⌜m + n⌝ = ⌜m⌝ + ⌜n⌝ ; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 16:

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

• Proof step 17:

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

Rule argument

Additional information

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

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

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

Rule argument

Additional information

Used simplifier rules: append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ (⌜x⌝ + ⌜x0⌝ )[m] = (x + x0)[m]; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ n < # x → (x + a ')[n] = x[n]; (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) ⊦ # a ' = 0 +1; (s) ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s) ⊦ #(σ + σ1) = # σ + # σ1; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ ⌜m + n⌝ = ⌜m⌝ + ⌜n⌝ ; (s) ⊦ ⌜n⌝ < ⌜1⌝ + n∞ ↔ ¬ n∞ < ⌜n⌝ ; (s)

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

User applied rule case distinction

And obtained the following new goals

• Proof step 19:

  # s ≠ 0, s ≠ ∅, x ≠ [], haspathanylength(g)(a), haspathanylength(g)(x.last), a ∈ s, ¬ # x < n, ¬ dom(g)((x + a ')[n]), ∀ n. n < # x → dom(g)(x[n]), ∀ n. n + 1 < # x → edge(g)(x[n], x[n + 1]), ∀ b. edge(g)(x.last, b) ↔ b ∈ s ⊦

• Proof step 33:

  # s ≠ 0, s ≠ ∅, x ≠ [], n0 < # x, haspathanylength(g)(a), haspathanylength(g)(x.last), a ∈ s, ¬ edge(g)(x[n0], (x + a ')[n0 + 1]), ∀ n. n < # x → dom(g)(x[n]), ∀ n. n + 1 < # x → edge(g)(x[n], x[n + 1]), ∀ b. edge(g)(x.last, b) ↔ b ∈ s ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  # s ≠ 0, s ≠ ∅, x ≠ [], haspathanylength(g)(x.last), haspathanylength(g)(a), a ∈ s, n ≤ # x, ¬ dom(g)((x + a ')[n]), ∀ b. edge(g)(x.last, b) ↔ b ∈ s, ∀ n. n + 1 < # x → edge(g)(x[n], x[n + 1]), ∀ n. n < # x → dom(g)(x[n]) ⊦

Rule argument

Additional information

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

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

User applied rule all left

And obtained the following new goals

• Proof step 21:

  # s ≠ 0, s ≠ ∅, x ≠ [], haspathanylength(g)(a), haspathanylength(g)(x.last), a ∈ s, n ≤ # x, ¬ dom(g)((x + a ')[n]), n < # x → dom(g)(x[n]), ∀ n. n + 1 < # x → edge(g)(x[n], x[n + 1]), ∀ b. edge(g)(x.last, b) ↔ b ∈ s ⊦

Rule argument

Additional information

Used terms: n

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 22:

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

• Proof step 23:

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

Rule argument

Additional information

Used terms: a, g

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

Lemma haspathanylength-def

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

User applied rule all left

And obtained the following new goals

• Proof step 24:

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

Rule argument

Additional information

Used terms: 0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

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

Rule argument

Additional information

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

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 26:

  x0 = a ', x0 = a + x1, # s ≠ 0, s ≠ ∅, x ≠ [], x0 ≠ [], haspathanylength(g)(x.last), pathp(g)(⌜x0⌝ ), a ∈ s, n ≤ # x, ¬ dom(g)((x + x0)[n]), n < # x → dom(g)(x[n]), ∀ n. n + 1 < # x → edge(g)(x[n], x[n + 1]), ∀ b. edge(g)(x.last, b) ↔ b ∈ s ⊦

Rule argument

Additional information

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

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

User applied rule all left

And obtained the following new goals

• Proof step 27:

  edge(g)(x.last, a) ↔ a ∈ s, x0 = a + x1, x0 = a ', # s ≠ 0, s ≠ ∅, x ≠ [], x0 ≠ [], haspathanylength(g)(x.last), pathp(g)(⌜x0⌝ ), a ∈ s, n ≤ # x, ¬ dom(g)((x + x0)[n]), n < # x → dom(g)(x[n]), ∀ n. n + 1 < # x → edge(g)(x[n], x[n + 1]) ⊦

Rule argument

Additional information

Used terms: a

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

  # s ≠ 0, s ≠ ∅, x ≠ [], edge(g)(x.last, a), haspathanylength(g)(x.last), pathp(g)(⌜a '⌝ ), a ∈ s, n ≤ # x, ¬ dom(g)((x + a ')[n]), n < # x → dom(g)(x[n]), ∀ n. n + 1 < # x → edge(g)(x[n], x[n + 1]) ⊦

Rule argument

Additional information

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

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

  # s ≠ 0, s ≠ ∅, x ≠ [], edge(g)(x.last, a), haspathanylength(g)(x.last), a ∈ s, n ≤ # x, ¬ dom(g)((x + a ')[n]), n < # x → dom(g)(x[n]), ∀ n. n + 1 < # x → edge(g)(x[n], x[n + 1]), ∀ n. ⌜n⌝ < # ⌜a '⌝ → dom(g)(⌜a '⌝ [n]), ∀ n. ⌜n + 1⌝ < # ⌜a '⌝ → edge(g)(⌜a '⌝ [n], ⌜a '⌝ [n + 1]) ⊦

Rule argument

Additional information

Used terms: g, ⌜a '⌝

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

  # s ≠ 0, s ≠ ∅, x ≠ [], dom(g)(a), edge(g)(x.last, a), haspathanylength(g)(x.last), a ∈ s, n ≤ # x, ¬ dom(g)((x + a ')[n]), n < # x → dom(g)(x[n]), ∀ n. n + 1 < # x → edge(g)(x[n], x[n + 1]) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a '[0] = a; (s) ⊦ ⌜x⌝ [n] = x[n]; (s) ⊦ m < 1 ↔ m = 0; (s) ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) ⊦ # a ' = 0 +1; (s) ⊦ # ⌜x⌝ = ⌜# x⌝ ; (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 < 0; (s) ⊦ m ≤ n → (⌜(* m)⌝ + n∞2 < ⌜(* n)⌝ ↔ n∞2 < ⌜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⌝ + ⌜n⌝ ; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 32:

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

Rule argument

Additional information

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

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

A spec-lemma

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

User applied rule all left

And obtained the following new goals

• Proof step 34:

  # s ≠ 0, s ≠ ∅, x ≠ [], n0 < # x, haspathanylength(g)(x.last), haspathanylength(g)(a), a ∈ s, ¬ edge(g)(x[n0], (x + a ')[n0 + 1]), n0 + 1 < # x → edge(g)(x[n0], x[n0 + 1]), ∀ b. edge(g)(x.last, b) ↔ b ∈ s, ∀ n. n < # x → dom(g)(x[n]) ⊦

Rule argument

Additional information

Used terms: n0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 35:

  # s ≠ 0, s ≠ ∅, x ≠ [], n0 < # x, haspathanylength(g)(x.last), haspathanylength(g)(a), a ∈ s, ¬ edge(g)(x[n0], (x + a ')[n0 + 1]), n0 + 1 < # x → edge(g)(x[n0], x[n0 + 1]), ∀ b. edge(g)(x.last, b) ↔ b ∈ s, ∀ n. n < # x → dom(g)(x[n]) ⊦

Rule argument

Additional information

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

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

  # s ≠ 0, s ≠ ∅, x ≠ [], n0 < # x, haspathanylength(g)(a), haspathanylength(g)(x.last), a ∈ s, ¬ n0 + 1 < # x, ¬ edge(g)(x[n0], (x + a ')[n0 + 1]), n0 + 1 < # x → edge(g)(x[n0], x[n0 + 1]), ∀ n. n < # x → dom(g)(x[n]), ∀ b. edge(g)(x.last, b) ↔ b ∈ s ⊦

Rule argument

Additional information

Used terms: x, a ', n0 + 1

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 38:

  # x = n0 + 1, # s ≠ 0, s ≠ ∅, x ≠ [], haspathanylength(g)(x.last), haspathanylength(g)(a), a ∈ s, ¬ edge(g)(x[n0], a), ∀ n. ¬ n0 < n → dom(g)(x[n]), ∀ b. edge(g)(x.last, b) ↔ b ∈ s ⊦

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

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

User applied rule all left

And obtained the following new goals

• Proof step 39:

  # x = n0 + 1, edge(g)(x.last, a) ↔ a ∈ s, # s ≠ 0, s ≠ ∅, x ≠ [], haspathanylength(g)(a), haspathanylength(g)(x.last), a ∈ s, ¬ edge(g)(x[n0], a), ∀ n. ¬ n0 < n → dom(g)(x[n]) ⊦

Rule argument

Additional information

Used terms: a

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 40:

  # x = n0 + 1, # s ≠ 0, s ≠ ∅, x ≠ [], edge(g)(x.last, a), haspathanylength(g)(x.last), haspathanylength(g)(a), a ∈ s, ¬ edge(g)(x[n0], a), ∀ n. ¬ n0 < n → dom(g)(x[n]) ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 41:

  ⊦ n = # x - 1 ∧ 0 < # x → x[n] = x.last

Rule argument

Additional information

Used simplifier rules: ⊦ 0 < m ↔ m ≠ 0; (s) ⊦ # x = 0 ↔ x = []; (s) ⊦ n ≤ m → m + n0 - n = (m - n) + n0; (s) ⊦ n + 0 = n; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: x, n0

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

A spec-lemma