Proof step 1 from proof finreach-fin (conclusion) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 2:

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

• Proof step 68:

  finout(g), ∀ g, s. finout(g) → (∃ s0. ∀ a. reach(g)(s, n0)(a) ↔ a ∈ s0) ⊦ ∃ s0. ∀ a. reach(g)(s, n0 +1)(a) ↔ a ∈ s0

Rule argument

Additional information

Used simplifier rules: Nat freely generated by 0, +1;;

Proof step 2 from proof finreach-fin (previous step) (back to tree)

User applied rule induction

And obtained the following new goals

• Proof step 3:

  finout(g), ∀ s0, g. # s0 < # s → finout(g) → (∃ s1. ∀ a. reach(g)(s0, 0)(a) ↔ a ∈ s1) ⊦ ∃ s0. ∀ a. reach(g)(s, 0)(a) ↔ a ∈ s0

Rule argument

Additional information

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

Proof step 3 from proof finreach-fin (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 4:

  finout(g), ∃ a. a ∈ s, ∀ s0, g. # s0 < # s → finout(g) → (∃ s1. ∀ a. reach(g)(s0, 0)(a) ↔ a ∈ s1) ⊦ ∃ s0. ∀ a. reach(g)(s, 0)(a) ↔ a ∈ s0

• Proof step 60:

  finout(g), ∀ s0, g. # s0 < # s → finout(g) → (∃ s1. ∀ a. reach(g)(s0, 0)(a) ↔ a ∈ s1) ⊦ ∃ s0. ∀ a. reach(g)(s, 0)(a) ↔ a ∈ s0, ∃ a. a ∈ s

Rule argument

Additional information

Used formulas: ∃ a. a ∈ s

Proof step 4 from proof finreach-fin (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, ∀ s0, g. # s0 < # s → finout(g) → (∃ s1. ∀ a. reach(g)(s0, 0)(a) ↔ a ∈ s1) ⊦ ∃ s0. ∀ a. reach(g)(s, 0)(a) ↔ a ∈ s0

Rule argument

Additional information

Used simplifier rules: finout-def: ⊦ finout(g) ↔ (∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s); 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 finreach-fin (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. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∃ s1. ∀ a0. reach(g)(s -- a, 0)(a0) ↔ a0 ∈ s1, ∀ s0, g. # s0 < # s → finout(g) → (∃ s1. ∀ a. reach(g)(s0, 0)(a) ↔ a ∈ s1) ⊦ ∃ s0. ∀ a. reach(g)(s, 0)(a) ↔ a ∈ s0

Rule argument

Additional information

Used simplifier rules: finout-def: ⊦ finout(g) ↔ (∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s); ⊦ 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 finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

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

Rule argument

Additional information

Proof step 7 from proof finreach-fin (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 8:

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

• Proof step 33:

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

Rule argument

Additional information

Used formulas: dom(g)(a)

Proof step 8 from proof finreach-fin (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 9:

  # s ≠ 0, s ≠ ∅, dom(g)(a), a ∈ s, ∀ a0. reach(g)(s -- a, 0)(a0) ↔ a0 ∈ s1, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ s0, g. # s0 < # s → finout(g) → (∃ s1. ∀ a. reach(g)(s0, 0)(a) ↔ a ∈ s1) ⊦ ∀ a0. reach(g)(s, 0)(a0) ↔ a0 ∈ s1 ++ a

Rule argument

Additional information

Used terms: s1 ++ a

Proof step 9 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  # s ≠ 0, ¬(reach(g)(s, 0)(a0) ↔ a0 = a ∨ a0 ∈ s1), s ≠ ∅, dom(g)(a), a ∈ s, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a0. reach(g)(s -- a, 0)(a0) ↔ a0 ∈ s1, ∀ s0, g. # s0 < # s → finout(g) → (∃ s1. ∀ a. reach(g)(s0, 0)(a) ↔ a ∈ s1) ⊦

Rule argument

Additional information

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

Proof step 10 from proof finreach-fin (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 11:

  reach(g)(s -- a, 0)(a0) ↔ a0 ∈ s1, # s ≠ 0, ¬(reach(g)(s, 0)(a0) ↔ a0 = a ∨ a0 ∈ s1), s ≠ ∅, dom(g)(a), a ∈ s, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ s0, g. # s0 < # s → finout(g) → (∃ s1. ∀ a. reach(g)(s0, 0)(a) ↔ a ∈ s1) ⊦

Rule argument

Additional information

Used terms: a0

Proof step 11 from proof finreach-fin (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

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

• Proof step 13:

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

Rule argument

Additional information

Used terms: a0, 0, s -- a, g

Proof step 12 from proof finreach-fin (previous step) (back to tree)

Lemma reach-def

Proof step 13 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

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

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 ⊦ a ∈ s -- a0 ↔ a ≠ a0 ∧ a ∈ s; (s)

Proof step 14 from proof finreach-fin (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

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

• Proof step 16:

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

Rule argument

Additional information

Used terms: a0, 0, s, g

Proof step 15 from proof finreach-fin (previous step) (back to tree)

Lemma reach-def

Proof step 16 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

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

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

Proof step 17 from proof finreach-fin (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 18:

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

• Proof step 23:

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

Rule argument

Additional information

Used formulas: a0 = a

Proof step 18 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

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

Rule argument

Additional information

Proof step 19 from proof finreach-fin (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 20:

  # s ≠ 0, s ≠ ∅, dom(g)(a), a ∈ s, (∃ x. x ≠ [] ∧ x.head ≠ x.last ∧ x.head ∈ s ∧ pathp(g)(⌜x⌝ ) ∧ a = x.last ∧ # x = 1) ↔ a ∈ s1, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ s0, g. # s0 < # s → finout(g) → (∃ s1. ∀ a. reach(g)(s0, 0)(a) ↔ a ∈ s1) ⊦ a ' ≠ [] ∧ a '.head ∈ s ∧ pathp(g)(⌜a '⌝ ) ∧ a = a '.last ∧ # a ' = 1

Rule argument

Additional information

Used terms: a '

Proof step 20 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

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

Rule argument

Additional information

Used simplifier rules: ⊦ # a ' = 0 +1; (s) ⊦ a '.last = a; (s) ⊦ a '.head = a; (s) ⊦ a ' ≠ []; (s)

Proof step 21 from proof finreach-fin (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 22:

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

Rule argument

Additional information

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

Proof step 22 from proof finreach-fin (previous step) (back to tree)

A spec-lemma

Proof step 23 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

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

Rule argument

Additional information

Proof step 24 from proof finreach-fin (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 25:

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

• Proof step 29:

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

Rule argument

Additional information

Proof step 25 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 26:

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

Rule argument

Additional information

Used simplifier rules: ⊦ x = x.head ' → x.last = x.head; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ x + [] = x; (s) ⊦ a + x = a ' + x; (s) ⊦ # x = 1 ↔ x = x.head + []; (as)

Proof step 26 from proof finreach-fin (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 27:

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

Rule argument

Additional information

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

Proof step 27 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

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

Rule argument

Additional information

Used simplifier rules: append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ σ + [] = σ; (s) ⊦ ⌜[]⌝ = []; (s) 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) ⊦ a ' = a0 ' + x ↔ a = a0 ∧ x = []; (ws)

Proof step 28 from proof finreach-fin (previous step) (back to tree)

User applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ a ' ≠ []; (s) ⊦ a '.head = a; (s) ⊦ a '.last = a; (s) ⊦ x + [] = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ # a ' = 0 +1; (s) Used terms: a0 ' + []

Proof step 29 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 30:

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

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 ⊦ x = x.head ' → x.last = x.head; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ x + [] = x; (s) ⊦ a + x = a ' + x; (s) ⊦ # x = 1 ↔ x = x.head + []; (as)

Proof step 30 from proof finreach-fin (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 31:

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

Rule argument

Additional information

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

Proof step 31 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 32:

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

Rule argument

Additional information

Used simplifier rules: append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ σ + [] = σ; (s) ⊦ ⌜[]⌝ = []; (s) 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) ⊦ a ' = a0 ' + x ↔ a = a0 ∧ x = []; (ws)

Proof step 32 from proof finreach-fin (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ a ' ≠ []; (s) ⊦ a '.head = a; (s) ⊦ a '.last = a; (s) ⊦ # a ' = 0 +1; (s) Used terms: a0 '

Proof step 33 from proof finreach-fin (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 34:

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

Rule argument

Additional information

Used terms: s1

Proof step 34 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 35:

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

Rule argument

Additional information

Proof step 35 from proof finreach-fin (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 36:

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

Rule argument

Additional information

Used terms: a0

Proof step 36 from proof finreach-fin (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 37:

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

• Proof step 50:

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

Rule argument

Additional information

Proof step 37 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 38:

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

Rule argument

Additional information

Proof step 38 from proof finreach-fin (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 39:

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

• Proof step 40:

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

Rule argument

Additional information

Used terms: a0, 0, s, g

Proof step 39 from proof finreach-fin (previous step) (back to tree)

Lemma reach-def

Proof step 40 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 41:

  x = x.head ', # s ≠ 0, s ≠ ∅, x ≠ [], pathp(g)(⌜x⌝ ), x.head ∈ s, a ∈ s, ¬ dom(g)(a), ¬ reach(g)(s -- a, 0)(x.head), ¬ x.head ∈ s1, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ s0, g. # s0 < # s → finout(g) → (∃ s1. ∀ a. reach(g)(s0, 0)(a) ↔ a ∈ s1) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ x = x.head ' → x.last = x.head; (s) 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 41 from proof finreach-fin (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 42:

  x = a0 ', x = a0 + x0, # s ≠ 0, s ≠ ∅, x ≠ [], pathp(g)(⌜x⌝ ), a ∈ s, a0 ∈ s, ¬ dom(g)(a), ¬ reach(g)(s -- a, 0)(a0), ¬ a0 ∈ s1, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ s0, g. # s0 < # s → finout(g) → (∃ s1. ∀ a. reach(g)(s0, 0)(a) ↔ a ∈ s1) ⊦

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 42 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 43:

  # s ≠ 0, s ≠ ∅, pathp(g)(⌜a0 '⌝ ), a ∈ s, a0 ∈ s, ¬ dom(g)(a), ¬ reach(g)(s -- a, 0)(a0), ¬ a0 ∈ s1, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ s0, g. # s0 < # s → finout(g) → (∃ s1. ∀ a. reach(g)(s0, 0)(a) ↔ a ∈ s1) ⊦

Rule argument

Additional information

Used simplifier rules: append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ σ + [] = σ; (s) ⊦ ⌜[]⌝ = []; (s) 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) ⊦ a ' = a0 ' + x ↔ a = a0 ∧ x = []; (ws)

Proof step 43 from proof finreach-fin (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 44:

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

• Proof step 45:

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

Rule argument

Additional information

Used terms: a0, 0, s -- a, g

Proof step 44 from proof finreach-fin (previous step) (back to tree)

Lemma reach-def

Proof step 45 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 46:

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

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 ⊦ a ∈ s -- a0 ↔ a ≠ a0 ∧ a ∈ s; (s)

Proof step 46 from proof finreach-fin (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 47:

  # s ≠ 0, s ≠ ∅, pathp(g)(⌜a0 '⌝ ), a0 ∈ s, a ∈ s, ¬ dom(g)(a), ¬ a0 ∈ s1, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, a0 ' = [] ∨ a0 '.head = a ∨ ¬ a0 '.head ∈ s ∨ ¬ pathp(g)(⌜a0 '⌝ ) ∨ a0 ≠ a0 '.last ∨ # a0 ' ≠ 1, ∀ s0, g. # s0 < # s → finout(g) → (∃ s1. ∀ a. reach(g)(s0, 0)(a) ↔ a ∈ s1) ⊦

Rule argument

Additional information

Used terms: a0 '

Proof step 47 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 48:

  # s ≠ 0, s ≠ ∅, pathp(g)(⌜a '⌝ ), a ∈ s, ¬ dom(g)(a), ¬ a ∈ s1, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ s0, g. # s0 < # s → finout(g) → (∃ s1. ∀ a. reach(g)(s0, 0)(a) ↔ a ∈ s1) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # a ' = 0 +1; (s) ⊦ a '.last = a; (s) ⊦ a '.head = a; (s) ⊦ a ' ≠ []; (s)

Proof step 48 from proof finreach-fin (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 49:

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

Rule argument

Additional information

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

Proof step 49 from proof finreach-fin (previous step) (back to tree)

A spec-lemma

Proof step 50 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 51:

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

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 51 from proof finreach-fin (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 52:

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

• Proof step 53:

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

Rule argument

Additional information

Used terms: a0, 0, s -- a, g

Proof step 52 from proof finreach-fin (previous step) (back to tree)

Lemma reach-def

Proof step 53 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 54:

  x = x.head ', # s ≠ 0, # s1 ≠ 0, x.head ≠ a, s ≠ ∅, s1 ≠ ∅, x ≠ [], pathp(g)(⌜x⌝ ), x.head ∈ s, a ∈ s, x.head ∈ s1, ¬ dom(g)(a), ¬ reach(g)(s, 0)(x.head), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ s0, g. # s0 < # s → finout(g) → (∃ s1. ∀ a. reach(g)(s0, 0)(a) ↔ a ∈ s1) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ x = x.head ' → x.last = x.head; (s) ⊦ a ∈ s -- a0 ↔ a ≠ a0 ∧ a ∈ s; (s) 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 54 from proof finreach-fin (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 55:

  x = a0 ', x = a0 + x0, # s ≠ 0, # s1 ≠ 0, a0 ≠ a, s ≠ ∅, s1 ≠ ∅, x ≠ [], pathp(g)(⌜x⌝ ), a0 ∈ s1, a ∈ s, a0 ∈ s, ¬ dom(g)(a), ¬ reach(g)(s, 0)(a0), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ s0, g. # s0 < # s → finout(g) → (∃ s1. ∀ a. reach(g)(s0, 0)(a) ↔ a ∈ s1) ⊦

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 56:

  # s1 ≠ 0, # s ≠ 0, a0 ≠ a, s ≠ ∅, s1 ≠ ∅, pathp(g)(⌜a0 '⌝ ), a0 ∈ s1, a ∈ s, a0 ∈ s, ¬ dom(g)(a), ¬ reach(g)(s, 0)(a0), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ s0, g. # s0 < # s → finout(g) → (∃ s1. ∀ a. reach(g)(s0, 0)(a) ↔ a ∈ s1) ⊦

Rule argument

Additional information

Used simplifier rules: append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ σ + [] = σ; (s) ⊦ ⌜[]⌝ = []; (s) 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) ⊦ a ' = a0 ' + x ↔ a = a0 ∧ x = []; (ws)

Proof step 56 from proof finreach-fin (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 57:

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

• Proof step 58:

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

Rule argument

Additional information

Used terms: a0, 0, s, g

Proof step 57 from proof finreach-fin (previous step) (back to tree)

Lemma reach-def

Proof step 58 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 59:

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

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

Proof step 59 from proof finreach-fin (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ a ' ≠ []; (s) ⊦ a '.head = a; (s) ⊦ a '.last = a; (s) ⊦ # a ' = 0 +1; (s) Used terms: a0 '

Proof step 60 from proof finreach-fin (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 61:

  finout(g), ∀ s0, g. # s0 < # s → finout(g) → (∃ s1. ∀ a. reach(g)(s0, 0)(a) ↔ a ∈ s1) ⊦ ∀ a. reach(g)(s, 0)(a) ↔ a ∈ ∅, ∃ a. a ∈ s

Rule argument

Additional information

Used terms: ∅

Proof step 61 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 62:

  reach(g)(s, 0)(a), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ s0, g. # s0 < # s → finout(g) → (∃ s1. ∀ a. reach(g)(s0, 0)(a) ↔ a ∈ s1) ⊦ ∃ a. a ∈ s

Rule argument

Additional information

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

Proof step 62 from proof finreach-fin (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 63:

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

• Proof step 64:

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

Rule argument

Additional information

Used terms: a, 0, s, g

Proof step 63 from proof finreach-fin (previous step) (back to tree)

Lemma reach-def

Proof step 64 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 65:

  x = x.head ', # s ≠ 0, s ≠ ∅, x ≠ [], pathp(g)(⌜x⌝ ), x.head ∈ s, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ s0, g. # s0 < # s → finout(g) → (∃ s1. ∀ a. reach(g)(s0, 0)(a) ↔ a ∈ 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: ⊦ (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 65 from proof finreach-fin (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 66:

  x = a0 ', x = a0 + x0, # s ≠ 0, s ≠ ∅, x ≠ [], pathp(g)(⌜x⌝ ), a0 ∈ s, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ s0, g. # s0 < # s → finout(g) → (∃ s1. ∀ a. reach(g)(s0, 0)(a) ↔ a ∈ s1) ⊦ ∃ a. a ∈ s

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 66 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 67:

  # s ≠ 0, s ≠ ∅, pathp(g)(⌜a0 '⌝ ), a0 ∈ s, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ s0, g. # s0 < # s → finout(g) → (∃ s1. ∀ a. reach(g)(s0, 0)(a) ↔ a ∈ s1) ⊦ ∃ a. a ∈ s

Rule argument

Additional information

Used simplifier rules: append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ σ + [] = σ; (s) ⊦ ⌜[]⌝ = []; (s) 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) ⊦ a ' = a0 ' + x ↔ a = a0 ∧ x = []; (ws)

Proof step 67 from proof finreach-fin (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 68 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 69:

  ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ g0, s0. (∀ a. ∃ s. ∀ b. edge(g0)(a, b) ↔ b ∈ s) → (∃ s1. ∀ a. reach(g0)(s0, n0)(a) ↔ a ∈ s1) ⊦ ∃ s0. ∀ a. reach(g)(s, n0 + 1)(a) ↔ a ∈ s0

Rule argument

Additional information

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

Proof step 69 from proof finreach-fin (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 70:

  (∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s) → (∃ s1. ∀ a. reach(g)(s, n0)(a) ↔ a ∈ s1), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s ⊦ ∃ s0. ∀ a. reach(g)(s, n0 + 1)(a) ↔ a ∈ s0

Rule argument

Additional information

Used terms: g, s

Proof step 70 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 71:

  ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. reach(g)(s, n0)(a) ↔ a ∈ s1 ⊦ ∃ s0. ∀ a. reach(g)(s, n0 + 1)(a) ↔ a ∈ s0

Rule argument

Additional information

Proof step 71 from proof finreach-fin (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 72:

  finout(g) ⊦ ∀ s. ∃ s0. ∀ b. b ∈ s0 ↔ (∃ a. a ∈ s ∧ edge(g)(a, b))

• Proof step 73:

  ∀ a. reach(g)(s, n0)(a) ↔ a ∈ s1, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ s. ∃ s0. ∀ b. b ∈ s0 ↔ (∃ a. a ∈ s ∧ edge(g)(a, b)) ⊦ ∃ s0. ∀ a. reach(g)(s, n0 + 1)(a) ↔ a ∈ s0

Rule argument

Additional information

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

Proof step 72 from proof finreach-fin (previous step) (back to tree)

Lemma finset-nextfin

Proof step 73 from proof finreach-fin (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 74:

  ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. reach(g)(s, n0)(a) ↔ a ∈ s1, ∃ s0. ∀ b. b ∈ s0 ↔ (∃ a. a ∈ s1 ∧ edge(g)(a, b)) ⊦ ∃ s0. ∀ a. reach(g)(s, n0 + 1)(a) ↔ a ∈ s0

Rule argument

Additional information

Used terms: s1

Proof step 74 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 75:

  ∀ b. b ∈ s0 ↔ (∃ a. a ∈ s1 ∧ edge(g)(a, b)), ∀ a. reach(g)(s, n0)(a) ↔ a ∈ s1, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s ⊦ ∃ s0. ∀ a. reach(g)(s, n0 + 1)(a) ↔ a ∈ s0

Rule argument

Additional information

Proof step 75 from proof finreach-fin (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 76:

  ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. reach(g)(s, n0)(a) ↔ a ∈ s1, ∀ b. b ∈ s0 ↔ (∃ a. a ∈ s1 ∧ edge(g)(a, b)) ⊦ ∀ a. reach(g)(s, n0 + 1)(a) ↔ a ∈ s0

Rule argument

Additional information

Used terms: s0

Proof step 76 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 77:

  ¬(reach(g)(s, n0 + 1)(a) ↔ a ∈ s0), ∀ b. b ∈ s0 ↔ (∃ a. a ∈ s1 ∧ edge(g)(a, b)), ∀ a. reach(g)(s, n0)(a) ↔ a ∈ s1, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s ⊦

Rule argument

Additional information

Proof step 77 from proof finreach-fin (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 78:

  ¬(reach(g)(s, n0 + 1)(a) ↔ a ∈ s0), a ∈ s0 ↔ (∃ a0. a0 ∈ s1 ∧ edge(g)(a0, a)), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. reach(g)(s, n0)(a) ↔ a ∈ s1 ⊦

Rule argument

Additional information

Used terms: a

Proof step 78 from proof finreach-fin (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 79:

  ¬(reach(g)(s, n0 + 1)(a) ↔ a ∈ s0), ¬ a ∈ s0, ∀ a. reach(g)(s, n0)(a) ↔ a ∈ s1, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s ⊦ ∃ a0. a0 ∈ s1 ∧ edge(g)(a0, a)

• Proof step 123:

  ¬(reach(g)(s, n0 + 1)(a) ↔ a ∈ s0), a ∈ s0, ∀ a. reach(g)(s, n0)(a) ↔ a ∈ s1, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∃ a0. a0 ∈ s1 ∧ edge(g)(a0, a) ⊦

Rule argument

Additional information

Proof step 79 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 80:

  reach(g)(s, n0 + 1)(a), ¬ a ∈ s0, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. reach(g)(s, n0)(a) ↔ a ∈ s1 ⊦ ∃ a0. a0 ∈ s1 ∧ edge(g)(a0, a)

Rule argument

Additional information

Proof step 80 from proof finreach-fin (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 81:

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

• Proof step 82:

  ¬ a ∈ s0, ∀ a. reach(g)(s, n0)(a) ↔ a ∈ s1, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∃ x. x ≠ [] ∧ x.head ∈ s ∧ pathp(g)(⌜x⌝ ) ∧ a = x.last ∧ # x = (n0 + 1) + 1 ⊦ ∃ a0. a0 ∈ s1 ∧ edge(g)(a0, a)

Rule argument

Additional information

Used terms: a, n0 + 1, s, g

Proof step 81 from proof finreach-fin (previous step) (back to tree)

Lemma reach-def

Proof step 82 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 83:

  # x = 2 + n0, # s ≠ 0, s ≠ ∅, x ≠ [], pathp(g)(⌜x⌝ ), x.head ∈ s, ¬ x.last ∈ s0, ∀ a. reach(g)(s, n0)(a) ↔ a ∈ s1, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s ⊦ ∃ a0. a0 ∈ s1 ∧ edge(g)(a0, x.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 a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic

Proof step 83 from proof finreach-fin (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 84:

  # x = 2 + n0, x = a1 + x0, # s ≠ 0, s ≠ ∅, x ≠ [], pathp(g)(⌜x⌝ ), a1 ∈ s, ¬ x.last ∈ s0, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. reach(g)(s, n0)(a) ↔ a ∈ s1 ⊦ ∃ a0. a0 ∈ s1 ∧ edge(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, x0

Proof step 84 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 85:

  # x0 = n0 + 1, # s ≠ 0, s ≠ ∅, pathp(g)(⌜a1 '⌝ + ⌜x0⌝ ), a1 ∈ s, ¬ (a1 ' + x0).last ∈ s0, ∀ a. reach(g)(s, n0)(a) ↔ a ∈ s1, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s ⊦ ∃ a0. a0 ∈ s1 ∧ edge(g)(a0, (a1 ' + x0).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) 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 85 from proof finreach-fin (previous step) (back to tree)

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 86:

  # x0 = n0 + 1, a1 ' + x0 = x1 + a2 ', # s ≠ 0, a1 ' + x0 ≠ [], s ≠ ∅, pathp(g)(⌜a1 '⌝ + ⌜x0⌝ ), a1 ∈ s, ¬ a2 ∈ s0, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. reach(g)(s, n0)(a) ↔ a ∈ s1 ⊦ ∃ a0. a0 ∈ s1 ∧ edge(g)(a0, a2)

Rule argument

Additional information

Used simplifier rules: ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ a ' ≠ []; (s) a: ⊦ (x + y) + z = x + y + z; from specification list x ≠ [] ⊦ a = x.last ∧ y = x.butlast ↔ x = y + a '; (elim) Used terms: a1 ' + x0, a2, x1

Proof step 86 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 87:

  # x0 = n0 + 1, a1 ' + x0 = x1 + a2 ', # s ≠ 0, s ≠ ∅, pathp(g)(⌜a1 '⌝ + ⌜x0⌝ ), a1 ∈ s, ¬ a2 ∈ s0, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. reach(g)(s, n0)(a) ↔ a ∈ s1, a1 ∈ x1 ∨ a1 = a2, a2 = a1 ∨ a2 ∈ x0 ⊦ ∃ a0. a0 ∈ s1 ∧ edge(g)(a0, a2)

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ∈ a0 ' + x ↔ a = a0 ∨ a ∈ x; (s) ⊦ a ∈ a0 ' ↔ a = a0; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) in-15: ⊦ x + a ' = y → a ∈ y; (forward) from specification list in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list ⊦ a ' ≠ []; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s)

Proof step 87 from proof finreach-fin (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 88:

  # x0 = n0 + 1, a1 ' + x0 = (a + x) + a2 ', # s ≠ 0, s ≠ ∅, pathp(g)(⌜a1 '⌝ + ⌜x0⌝ ), a1 ∈ s, ¬ a2 ∈ s0, ∀ a. reach(g)(s, n0)(a) ↔ a ∈ s1, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ x0, n0, a1, a2, s, g, s0, s1. # x0 = n0 + 1 ∧ a1 ' + x0 = x + a2 ' ∧ # s ≠ 0 ∧ s ≠ ∅ ∧ pathp(g)(⌜a1 '⌝ + ⌜x0⌝ ) ∧ a1 ∈ s ∧ ¬ a2 ∈ s0 ∧ (∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s) ∧ (∀ a. reach(g)(s, n0)(a) ↔ a ∈ s1) ∧ (a1 ∈ x ∨ a1 = a2) ∧ (a2 = a1 ∨ a2 ∈ x0) → (∃ a0. a0 ∈ s1 ∧ edge(g)(a0, a2)), a2 = a1 ∨ a2 ∈ x0, a1 ∈ a + x ∨ a1 = a2 ⊦ ∃ a0. a0 ∈ s1 ∧ edge(g)(a0, a2)

Rule argument

Additional information

Used simplifier rules: List('a) freely generated by [], +;; ⊦ [] + x = x; (s) ⊦ a ' = a0 ' + x ↔ a = a0 ∧ x = []; (ws) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ ¬ a ∈ []; (s) ⊦ # [] = 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

Proof step 88 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 89:

  # s ≠ 0, s ≠ ∅, pathp(g)(⌜a1 '⌝ + ⌜x⌝ + ⌜a2 '⌝ ), a1 ∈ s, ¬ a2 ∈ s0, ∀ x0, n0, a1, a2, s, g, s0, s1. # x0 = n0 + 1 ∧ a1 ' + x0 = x + a2 ' ∧ # s ≠ 0 ∧ s ≠ ∅ ∧ pathp(g)(⌜a1 '⌝ + ⌜x0⌝ ) ∧ a1 ∈ s ∧ ¬ a2 ∈ s0 ∧ (∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s) ∧ (∀ a. reach(g)(s, n0)(a) ↔ a ∈ s1) ∧ (a1 ∈ x ∨ a1 = a2) ∧ (a2 = a1 ∨ a2 ∈ x0) → (∃ a0. a0 ∈ s1 ∧ edge(g)(a0, a2)), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. reach(g)(s, # x)(a) ↔ a ∈ s1 ⊦ ∃ a0. a0 ∈ s1 ∧ edge(g)(a0, a2)

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ∈ a0 ' ↔ a = a0; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ 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 + n = m + n0 ↔ n = n0; (s) ⊦ # a ' = 0 +1; (s) ⊦ #(x + y) = # x + # y; (s) in-15: ⊦ x + a ' = y → a ∈ y; (forward) from specification list ⊦ a ∈ a0 ' + x ↔ a = a0 ∨ a ∈ x; (s) ⊦ a + x = a ' + x; (s) ⊦ a ' + x = a0 ' + y ↔ a = a0 ∧ x = y; (ws)

Proof step 89 from proof finreach-fin (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 90:

  # s ≠ 0, s ≠ ∅, pathp(g)(⌜a1 '⌝ + ⌜x⌝ + ⌜a2 '⌝ ), a1 ∈ s, ¬ a2 ∈ s0, ∀ a. reach(g)(s, # x)(a) ↔ a ∈ s1, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ x0, n0, a1, a2, s, g, s0, s1. # x0 = n0 + 1 ∧ a1 ' + x0 = x + a2 ' ∧ # s ≠ 0 ∧ s ≠ ∅ ∧ pathp(g)(⌜a1 '⌝ + ⌜x0⌝ ) ∧ a1 ∈ s ∧ ¬ a2 ∈ s0 ∧ (∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s) ∧ (∀ a. reach(g)(s, n0)(a) ↔ a ∈ s1) ∧ (a1 ∈ x ∨ a1 = a2) ∧ (a2 = a1 ∨ a2 ∈ x0) → (∃ a0. a0 ∈ s1 ∧ edge(g)(a0, a2)) ⊦ (a1 ' + x).last ∈ s1 ∧ edge(g)((a1 ' + x).last, a2)

Rule argument

Additional information

Used terms: (a1 ' + x).last

Proof step 90 from proof finreach-fin (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 91:

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

• Proof step 92:

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

Rule argument

Additional information

Used terms: ⌜a1 '⌝ + ⌜x⌝ + ⌜a2 '⌝ , g

Proof step 91 from proof finreach-fin (previous step) (back to tree)

A spec-lemma

Proof step 92 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 93:

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

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) ⊦ # a ' = 0 +1; (s) ⊦ # ⌜x⌝ = ⌜# x⌝ ; (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 93 from proof finreach-fin (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 94:

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

Rule argument

Additional information

Used terms: # x

Proof step 94 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 95:

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

Rule argument

Additional information

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

Proof step 95 from proof finreach-fin (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 96:

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

Rule argument

Additional information

Used terms: (a1 ' + x).last

Proof step 96 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 97:

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

Rule argument

Additional information

Proof step 97 from proof finreach-fin (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 98:

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

• Proof step 99:

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

Rule argument

Additional information

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

Proof step 98 from proof finreach-fin (previous step) (back to tree)

Lemma reach-def

Proof step 99 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 100:

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

Rule argument

Additional information

Proof step 100 from proof finreach-fin (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 101:

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

Rule argument

Additional information

Used terms: a1 ' + x

Proof step 101 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 102:

  # s ≠ 0, s ≠ ∅, edge(g)((a1 ' + x).last, a2), a1 ∈ s, ¬ pathp(g)(⌜a1 '⌝ + ⌜x⌝ ), ¬ a2 ∈ s0, ¬ (a1 ' + x).last ∈ s1, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ x0, n0, a1, a2, s, g, s0, s1. # x0 = n0 + 1 ∧ a1 ' + x0 = x + a2 ' ∧ # s ≠ 0 ∧ s ≠ ∅ ∧ pathp(g)(⌜a1 '⌝ + ⌜x0⌝ ) ∧ a1 ∈ s ∧ ¬ a2 ∈ s0 ∧ (∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s) ∧ (∀ a. reach(g)(s, n0)(a) ↔ a ∈ s1) ∧ (a1 ∈ x ∨ a1 = a2) ∧ (a2 = a1 ∨ a2 ∈ x0) → (∃ a0. a0 ∈ s1 ∧ edge(g)(a0, a2)), ∀ n. ¬ # x < n → edge(g)((a1 ' + x + a2 ')[n], (x + a2 ')[n]), ∀ n. n < 2 + # x → dom(g)((a1 ' + x + a2 ')[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 + 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) ⊦ ⌜x + y⌝ = ⌜x⌝ + ⌜y⌝ ; (s) ⊦ (a ' + x).head = a; (s) ⊦ a ' ≠ []; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s)

Proof step 102 from proof finreach-fin (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 103:

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

• Proof step 104:

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

Rule argument

Additional information

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

Proof step 103 from proof finreach-fin (previous step) (back to tree)

A spec-lemma

Proof step 104 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 105:

  # s ≠ 0, s ≠ ∅, edge(g)((a1 ' + x).last, a2), a1 ∈ s, ¬ a2 ∈ s0, ¬ (a1 ' + x).last ∈ s1, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ x0, n0, a1, a2, s, g, s0, s1. # x0 = n0 + 1 ∧ a1 ' + x0 = x + a2 ' ∧ # s ≠ 0 ∧ s ≠ ∅ ∧ pathp(g)(⌜a1 '⌝ + ⌜x0⌝ ) ∧ a1 ∈ s ∧ ¬ a2 ∈ s0 ∧ (∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s) ∧ (∀ a. reach(g)(s, n0)(a) ↔ a ∈ s1) ∧ (a1 ∈ x ∨ a1 = a2) ∧ (a2 = a1 ∨ a2 ∈ x0) → (∃ a0. a0 ∈ s1 ∧ edge(g)(a0, a2)), ∀ n. ¬ # x < n → edge(g)((a1 ' + x + a2 ')[n], (x + a2 ')[n]), ∀ n. n < 2 + # x → dom(g)((a1 ' + x + a2 ')[n]), ¬(¬ # x < n → dom(g)((a1 ' + x)[n])) ∨ ¬(n0 < # x → edge(g)((a1 ' + x)[n0], x[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 105 from proof finreach-fin (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 106:

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

• Proof step 113:

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

Rule argument

Additional information

Proof step 106 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 107:

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

Rule argument

Additional information

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

Proof step 107 from proof finreach-fin (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 108:

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

Rule argument

Additional information

Used terms: n

Proof step 108 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 109:

  # s ≠ 0, s ≠ ∅, n < 2 + # x, dom(g)((a1 ' + x + a2 ')[n]), edge(g)((a1 ' + x).last, a2), a1 ∈ s, n ≤ # x, ¬ dom(g)((a1 ' + x)[n]), ¬ a2 ∈ s0, ¬ (a1 ' + x).last ∈ s1, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ x0, n0, a1, a2, s, g, s0, s1. # x0 = n0 + 1 ∧ a1 ' + x0 = x + a2 ' ∧ # s ≠ 0 ∧ s ≠ ∅ ∧ pathp(g)(⌜a1 '⌝ + ⌜x0⌝ ) ∧ a1 ∈ s ∧ ¬ a2 ∈ s0 ∧ (∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s) ∧ (∀ a. reach(g)(s, n0)(a) ↔ a ∈ s1) ∧ (a1 ∈ x ∨ a1 = a2) ∧ (a2 = a1 ∨ a2 ∈ x0) → (∃ a0. a0 ∈ s1 ∧ edge(g)(a0, a2)), ∀ n. ¬ # x < n → edge(g)((a1 ' + x + a2 ')[n], (x + a2 ')[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 n < n0 ⊦ (* n) ≠ m0 + (* n0); (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ m + m0 ≤ m ↔ m0 = 0; (s) let: ⊦ n ≤ n0 ∧ n0 ≤ n1 → n ≤ n1; (forward) from specification nat ⊦ m < n ↔ ¬ n ≤ m; (ss)

Proof step 109 from proof finreach-fin (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 110:

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

• Proof step 111:

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

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) ⊦ 0 ≤ m; (s) ⊦ 0 < m ↔ m ≠ 0; (s) n < n0 ⊦ (* n) ≠ m0 + (* n0); (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ (a ' + x)[0] = a; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: a1 ', x + a2 ', n

Proof step 110 from proof finreach-fin (previous step) (back to tree)

A spec-lemma

Proof step 111 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 112:

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

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 112 from proof finreach-fin (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 + a ')[n] = x[n]; (s) n < n0 ⊦ m + (* n) < m0 + (* n0) ↔ m < m0 + (n0 - n); (s) ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ m < n → ¬ 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 n ≠ 0 ⊦ m = n - 1 ↔ n = m + 1; (elim) Used terms: n, m

Proof step 113 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 114:

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

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

Proof step 114 from proof finreach-fin (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 115:

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

Rule argument

Additional information

Used terms: n0

Proof step 115 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 116:

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

Rule argument

Additional information

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

Proof step 116 from proof finreach-fin (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 117:

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

• Proof step 118:

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

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) ⊦ 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: a1 ', x + a2 ', n0

Proof step 117 from proof finreach-fin (previous step) (back to tree)

A spec-lemma

Proof step 118 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 119:

  # s ≠ 0, n0 ≠ 0, s ≠ ∅, x ≠ [], n0 < # x, edge(g)(x.last, a2), edge(g)((x + a2 ')[n0 - 1], x[n0]), a1 ∈ s, ¬ edge(g)((a1 ' + x)[n0], x[n0]), ¬ a2 ∈ s0, ¬ x.last ∈ s1, ∀ n. n < 2 + # x → dom(g)((a1 ' + x + a2 ')[n]), ∀ x0, n0, a1, a2, s, g, s0, s1. # x0 = n0 + 1 ∧ a1 ' + x0 = x + a2 ' ∧ # s ≠ 0 ∧ s ≠ ∅ ∧ pathp(g)(⌜a1 '⌝ + ⌜x0⌝ ) ∧ a1 ∈ s ∧ ¬ a2 ∈ s0 ∧ (∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s) ∧ (∀ a. reach(g)(s, n0)(a) ↔ a ∈ s1) ∧ (a1 ∈ x ∨ a1 = a2) ∧ (a2 = a1 ∨ a2 ∈ x0) → (∃ a0. a0 ∈ s1 ∧ edge(g)(a0, a2)), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s ⊦

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 119 from proof finreach-fin (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 120:

  n0 = m + 1, # s ≠ 0, n0 ≠ 0, s ≠ ∅, x ≠ [], n0 < # x, edge(g)((x + a2 ')[m], x[n0]), edge(g)(x.last, a2), a1 ∈ s, ¬ edge(g)((a1 ' + x)[n0], x[n0]), ¬ a2 ∈ s0, ¬ x.last ∈ s1, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ x0, n0, a1, a2, s, g, s0, s1. # x0 = n0 + 1 ∧ a1 ' + x0 = x + a2 ' ∧ # s ≠ 0 ∧ s ≠ ∅ ∧ pathp(g)(⌜a1 '⌝ + ⌜x0⌝ ) ∧ a1 ∈ s ∧ ¬ a2 ∈ s0 ∧ (∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s) ∧ (∀ a. reach(g)(s, n0)(a) ↔ a ∈ s1) ∧ (a1 ∈ x ∨ a1 = a2) ∧ (a2 = a1 ∨ a2 ∈ x0) → (∃ a0. a0 ∈ s1 ∧ edge(g)(a0, a2)), ∀ n. n < 2 + # x → dom(g)((a1 ' + x + a2 ')[n]) ⊦

Rule argument

Additional information

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

Proof step 120 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 121:

  # s ≠ 0, s ≠ ∅, x ≠ [], m + 1 < # x, edge(g)(x.last, a2), edge(g)((x + a2 ')[m], x[m + 1]), a1 ∈ s, ¬ edge(g)(x[m], x[m + 1]), ¬ a2 ∈ s0, ¬ x.last ∈ s1, ∀ n. n < 2 + # x → dom(g)((a1 ' + x + a2 ')[n]), ∀ x0, n0, a1, a2, s, g, s0, s1. # x0 = n0 + 1 ∧ a1 ' + x0 = x + a2 ' ∧ # s ≠ 0 ∧ s ≠ ∅ ∧ pathp(g)(⌜a1 '⌝ + ⌜x0⌝ ) ∧ a1 ∈ s ∧ ¬ a2 ∈ s0 ∧ (∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s) ∧ (∀ a. reach(g)(s, n0)(a) ↔ a ∈ s1) ∧ (a1 ∈ x ∨ a1 = a2) ∧ (a2 = a1 ∨ a2 ∈ x0) → (∃ a0. a0 ∈ s1 ∧ edge(g)(a0, a2)), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s ⊦

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 + 1 ≠ 0; (s)

Proof step 121 from proof finreach-fin (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 122:

  ⊦ 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: x, a2 ', m

Proof step 122 from proof finreach-fin (previous step) (back to tree)

A spec-lemma

Proof step 123 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 124:

  # s0 ≠ 0, # s1 ≠ 0, s0 ≠ ∅, s1 ≠ ∅, edge(g)(a0, a), a ∈ s0, a0 ∈ s1, ¬ reach(g)(s, n0 + 1)(a), ∀ a. reach(g)(s, n0)(a) ↔ a ∈ s1, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ 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

Proof step 124 from proof finreach-fin (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 125:

  reach(g)(s, n0)(a0) ↔ a0 ∈ s1, # s0 ≠ 0, # s1 ≠ 0, s0 ≠ ∅, s1 ≠ ∅, edge(g)(a0, a), a0 ∈ s1, a ∈ s0, ¬ reach(g)(s, n0 + 1)(a), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s ⊦

Rule argument

Additional information

Used terms: a0

Proof step 125 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 126:

  # s0 ≠ 0, # s1 ≠ 0, s0 ≠ ∅, s1 ≠ ∅, edge(g)(a0, a), reach(g)(s, n0)(a0), a ∈ s0, a0 ∈ s1, ¬ reach(g)(s, n0 + 1)(a), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s ⊦

Rule argument

Additional information

Proof step 126 from proof finreach-fin (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 127:

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

• Proof step 128:

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

Rule argument

Additional information

Used terms: a, n0 + 1, s, g

Proof step 127 from proof finreach-fin (previous step) (back to tree)

Lemma reach-def

Proof step 128 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 129:

  # s0 ≠ 0, # s1 ≠ 0, s0 ≠ ∅, s1 ≠ ∅, edge(g)(a0, a), reach(g)(s, n0)(a0), a ∈ s0, a0 ∈ s1, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ x. x = [] ∨ ¬ x.head ∈ s ∨ ¬ pathp(g)(⌜x⌝ ) ∨ a ≠ x.last ∨ # x ≠ 2 + n0 ⊦

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 129 from proof finreach-fin (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 130:

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

• Proof step 131:

  # s0 ≠ 0, # s1 ≠ 0, s0 ≠ ∅, s1 ≠ ∅, edge(g)(a0, a), a0 ∈ s1, a ∈ s0, ∀ x. x = [] ∨ ¬ x.head ∈ s ∨ ¬ pathp(g)(⌜x⌝ ) ∨ a ≠ x.last ∨ # x ≠ 2 + n0, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∃ x. x ≠ [] ∧ x.head ∈ s ∧ pathp(g)(⌜x⌝ ) ∧ a0 = x.last ∧ # x = n0 + 1 ⊦

Rule argument

Additional information

Used terms: a0, n0, s, g

Proof step 130 from proof finreach-fin (previous step) (back to tree)

Lemma reach-def

Proof step 131 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 132:

  # x = n0 + 1, # s1 ≠ 0, # s0 ≠ 0, # s ≠ 0, s ≠ ∅, s0 ≠ ∅, s1 ≠ ∅, x ≠ [], edge(g)(x.last, a), pathp(g)(⌜x⌝ ), x.last ∈ s1, a ∈ s0, x.head ∈ s, ∀ x. x = [] ∨ ¬ x.head ∈ s ∨ ¬ pathp(g)(⌜x⌝ ) ∨ a ≠ x.last ∨ # x ≠ 2 + n0, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ 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

Proof step 132 from proof finreach-fin (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 133:

  # x = n0 + 1, x = a0 + x0, # s1 ≠ 0, # s0 ≠ 0, # s ≠ 0, s ≠ ∅, s0 ≠ ∅, s1 ≠ ∅, x ≠ [], edge(g)(x.last, a), pathp(g)(⌜x⌝ ), a0 ∈ s, a ∈ s0, x.last ∈ s1, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ x. x = [] ∨ ¬ x.head ∈ s ∨ ¬ pathp(g)(⌜x⌝ ) ∨ a ≠ x.last ∨ # x ≠ 2 + n0 ⊦

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 133 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 134:

  # s ≠ 0, # s0 ≠ 0, # s1 ≠ 0, s ≠ ∅, s0 ≠ ∅, s1 ≠ ∅, edge(g)((a0 ' + x0).last, a), pathp(g)(⌜a0 '⌝ + ⌜x0⌝ ), a0 ∈ s, a ∈ s0, (a0 ' + x0).last ∈ s1, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ x. x = [] ∨ ¬ x.head ∈ s ∨ ¬ pathp(g)(⌜x⌝ ) ∨ a ≠ x.last ∨ # x ≠ 2 + # x0 ⊦

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 134 from proof finreach-fin (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 135:

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

• Proof step 136:

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

Rule argument

Additional information

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

Proof step 135 from proof finreach-fin (previous step) (back to tree)

A spec-lemma

Proof step 136 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 137:

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

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 137 from proof finreach-fin (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 138:

  # s ≠ 0, # s0 ≠ 0, # s1 ≠ 0, s ≠ ∅, s0 ≠ ∅, s1 ≠ ∅, edge(g)((a0 ' + x0).last, a), (a0 ' + x0).last ∈ s1, a ∈ s0, a0 ∈ s, ∀ n. ¬ # x0 < n → dom(g)((a0 ' + x0)[n]), ∀ n. n < # x0 → edge(g)((a0 ' + x0)[n], x0[n]), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, a0 ' + (x0 + a) = [] ∨ ¬ (a0 ' + (x0 + a)).head ∈ s ∨ ¬ pathp(g)(⌜a0 ' + (x0 + a)⌝ ) ∨ a ≠ (a0 ' + (x0 + a)).last ∨ #(a0 ' + (x0 + a)) ≠ 2 + # x0 ⊦

Rule argument

Additional information

Used terms: a0 ' + (x0 + a)

Proof step 138 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 139:

  # s ≠ 0, # s0 ≠ 0, # s1 ≠ 0, s ≠ ∅, s0 ≠ ∅, s1 ≠ ∅, edge(g)((a0 ' + x0).last, a), a0 ∈ s, a ∈ s0, (a0 ' + x0).last ∈ s1, ¬ pathp(g)(⌜a0 '⌝ + ⌜x0⌝ + ⌜a '⌝ ), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ n. n < # x0 → edge(g)((a0 ' + x0)[n], x0[n]), ∀ n. ¬ # x0 < n → dom(g)((a0 ' + x0)[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 + n = m + n0 ↔ n = n0; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ m +1 = m + 1; (s) ⊦ # a ' = 0 +1; (s) ⊦ #(x + y) = # x + # y; (s) ⊦ #(a ' + x) = (# x)+1; (s) ⊦ x + a = x + a '; (s) ⊦ (a ' + x + b ').last = b; (s) ⊦ ⌜x + y⌝ = ⌜x⌝ + ⌜y⌝ ; (s) ⊦ (a ' + x).head = a; (s) ⊦ a ' ≠ []; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s)

Proof step 139 from proof finreach-fin (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 140:

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

• Proof step 141:

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

Rule argument

Additional information

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

Proof step 140 from proof finreach-fin (previous step) (back to tree)

A spec-lemma

Proof step 141 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 142:

  # s ≠ 0, # s0 ≠ 0, # s1 ≠ 0, s ≠ ∅, s0 ≠ ∅, s1 ≠ ∅, edge(g)((a0 ' + x0).last, a), a0 ∈ s, a ∈ s0, (a0 ' + x0).last ∈ s1, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ n. n < # x0 → edge(g)((a0 ' + x0)[n], x0[n]), ∀ n. ¬ # x0 < n → dom(g)((a0 ' + x0)[n]), ¬(n < 2 + # x0 → dom(g)((a0 ' + x0 + a ')[n])) ∨ ¬(¬ # x0 < n0 → edge(g)((a0 ' + x0 + a ')[n0], (x0 + a ')[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⌝ + ⌜x0⌝ )[m] = (x + x0)[m]; (s) ⊦ (⌜a '⌝ + σ)[n + 1] = σ[n]; (s) ⊦ (⌜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 ⊦ ⌜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) ⊦ ⌜(* n)⌝ + ⌜(* m)⌝ = ⌜n + m⌝ ; (s) ⊦ # a ' = 0 +1; (s) ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s) ⊦ #(σ + σ1) = # σ + # σ1; (s) ⊦ ⌜m + n⌝ = ⌜m⌝ + ⌜n⌝ ; (s) ⊦ ⌜n⌝ < ⌜m⌝ + ⌜n0⌝ ↔ n < m + n0; (s)

Proof step 142 from proof finreach-fin (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 143:

  # s ≠ 0, # s0 ≠ 0, # s1 ≠ 0, s ≠ ∅, s0 ≠ ∅, s1 ≠ ∅, n < 2 + # x0, edge(g)((a0 ' + x0).last, a), (a0 ' + x0).last ∈ s1, a ∈ s0, a0 ∈ s, ¬ dom(g)((a0 ' + x0 + a ')[n]), ∀ n. ¬ # x0 < n → dom(g)((a0 ' + x0)[n]), ∀ n. n < # x0 → edge(g)((a0 ' + x0)[n], x0[n]), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s ⊦

• Proof step 156:

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

Rule argument

Additional information

Proof step 143 from proof finreach-fin (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 144:

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

• Proof step 145:

  # s ≠ 0, # s0 ≠ 0, # s1 ≠ 0, s ≠ ∅, s0 ≠ ∅, s1 ≠ ∅, n < # a0 ', n < 2 + # x0, edge(g)((a0 ' + x0).last, a), a0 ∈ s, a ∈ s0, (a0 ' + x0).last ∈ s1, ¬ dom(g)((a0 ' + x0 + a ')[n]), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ n. n < # x0 → edge(g)((a0 ' + x0)[n], x0[n]), ∀ n. ¬ # x0 < n → dom(g)((a0 ' + x0)[n]) ⊦

• Proof step 147:

  # s ≠ 0, # s0 ≠ 0, # s1 ≠ 0, s ≠ ∅, s0 ≠ ∅, s1 ≠ ∅, n < 2 + # x0, edge(g)((a0 ' + x0).last, a), a0 ∈ s, a ∈ s0, (a0 ' + x0).last ∈ s1, ¬ n < # a0 ', ¬ dom(g)((x0 + a ')[n - # a0 ']), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ n. n < # x0 → edge(g)((a0 ' + x0)[n], x0[n]), ∀ n. ¬ # x0 < n → dom(g)((a0 ' + x0)[n]) ⊦

Rule argument

Additional information

Used terms: n, x0 + a ', a0 '

Proof step 144 from proof finreach-fin (previous step) (back to tree)

A spec-lemma

Proof step 145 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 146:

  # s1 ≠ 0, # s0 ≠ 0, # s ≠ 0, s ≠ ∅, s0 ≠ ∅, s1 ≠ ∅, edge(g)((a0 ' + x0).last, a), a0 ∈ s, a ∈ s0, (a0 ' + x0).last ∈ s1, ¬ dom(g)(a0), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ n. n < # x0 → edge(g)((a0 ' + x0)[n], x0[n]), ∀ n. ¬ # x0 < n → dom(g)((a0 ' + x0)[n]) ⊦

Rule argument

Additional information

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

Proof step 146 from proof finreach-fin (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 147 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 148:

  # s1 ≠ 0, # s0 ≠ 0, # s ≠ 0, n ≠ 0, s ≠ ∅, s0 ≠ ∅, s1 ≠ ∅, n < 2 + # x0, edge(g)((a0 ' + x0).last, a), a0 ∈ s, a ∈ s0, (a0 ' + x0).last ∈ s1, ¬ dom(g)((x0 + a ')[n - 1]), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ n. n < # x0 → edge(g)((a0 ' + x0)[n], x0[n]), ∀ n. ¬ # x0 < n → dom(g)((a0 ' + x0)[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 n < n0 ⊦ (* n) ≠ m0 + (* n0); (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ # a ' = 0 +1; (s) ⊦ m < 1 ↔ m = 0; (s)

Proof step 148 from proof finreach-fin (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 149:

  n = m + 1, # s1 ≠ 0, # s0 ≠ 0, # s ≠ 0, n ≠ 0, s ≠ ∅, s0 ≠ ∅, s1 ≠ ∅, n < 2 + # x0, edge(g)((a0 ' + x0).last, a), (a0 ' + x0).last ∈ s1, a ∈ s0, a0 ∈ s, ¬ dom(g)((x0 + a ')[m]), ∀ n. ¬ # x0 < n → dom(g)((a0 ' + x0)[n]), ∀ n. n < # x0 → edge(g)((a0 ' + x0)[n], x0[n]), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s ⊦

Rule argument

Additional information

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

Proof step 149 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 150:

  # s1 ≠ 0, # s0 ≠ 0, # s ≠ 0, s ≠ ∅, s0 ≠ ∅, s1 ≠ ∅, edge(g)((a0 ' + x0).last, a), a0 ∈ s, a ∈ s0, (a0 ' + x0).last ∈ s1, m ≤ # x0, ¬ dom(g)((x0 + a ')[m]), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ n. n < # x0 → edge(g)((a0 ' + x0)[n], x0[n]), ∀ n. ¬ # x0 < n → dom(g)((a0 ' + x0)[n]) ⊦

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 + 1 ↔ ¬ n < m; (s) n < n0 ⊦ m + (* n) < m0 + (* n0) ↔ m < m0 + (n0 - n); (s) ⊦ m + 1 ≠ 0; (s)

Proof step 150 from proof finreach-fin (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 151:

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

• Proof step 152:

  # s1 ≠ 0, # s0 ≠ 0, # s ≠ 0, s ≠ ∅, s0 ≠ ∅, s1 ≠ ∅, edge(g)((a0 ' + x0).last, a), (a0 ' + x0).last ∈ s1, a ∈ s0, a0 ∈ s, m ≤ # x0, ¬ m < # x0, ¬ dom(g)((x0 + a ')[m]), ∀ n. ¬ # x0 < n → dom(g)((a0 ' + x0)[n]), ∀ n. n < # x0 → edge(g)((a0 ' + x0)[n], x0[n]), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s ⊦

• Proof step 154:

  # s1 ≠ 0, # s0 ≠ 0, # s ≠ 0, s ≠ ∅, s0 ≠ ∅, s1 ≠ ∅, m < # x0, edge(g)((a0 ' + x0).last, a), (a0 ' + x0).last ∈ s1, a ∈ s0, a0 ∈ s, m ≤ # x0, ¬ dom(g)(x0[m]), ∀ n. ¬ # x0 < n → dom(g)((a0 ' + x0)[n]), ∀ n. n < # x0 → edge(g)((a0 ' + x0)[n], x0[n]), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s ⊦

Rule argument

Additional information

Used terms: m, a ', x0

Proof step 151 from proof finreach-fin (previous step) (back to tree)

A spec-lemma

Proof step 152 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 153:

  # s ≠ 0, # s0 ≠ 0, # s1 ≠ 0, s ≠ ∅, s0 ≠ ∅, s1 ≠ ∅, edge(g)((a0 ' + x0).last, a), (a0 ' + x0).last ∈ s1, a ∈ s0, a0 ∈ s, ¬ dom(g)(a), ∀ n. ¬ # x0 < n → dom(g)((a0 ' + x0)[n]), ∀ n. n < # x0 → edge(g)((a0 ' + x0)[n], x0[n]), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s ⊦

Rule argument

Additional information

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

Proof step 153 from proof finreach-fin (previous step) (back to tree)

User applied rule constructor cut

And closed the goal!

Rule argument

Additional information

Used simplifier rules: Graph('a) generated by ×;; ⊦ edge(vs × es)(a, b) ↔ es(a, b) ∧ vs(a) ∧ vs(b); (ws) ⊦ dom(vs × es) = vs; (s)

Proof step 154 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 155:

  # s ≠ 0, # s0 ≠ 0, # s1 ≠ 0, s ≠ ∅, s0 ≠ ∅, s1 ≠ ∅, x0 ≠ [], m < # x0, edge(g)(x0.last, a), a ∈ s0, a0 ∈ s, x0.last ∈ s1, ¬ dom(g)(x0[m]), ∀ n. ¬ # x0 < n → dom(g)((a0 ' + x0)[n]), ∀ n. n < # x0 → edge(g)((a0 ' + x0)[n], x0[n]), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s ⊦

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 → m ≤ n; (s)

Proof step 155 from proof finreach-fin (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 156 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 157:

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

Rule argument

Additional information

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

Proof step 157 from proof finreach-fin (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 158:

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

• Proof step 159:

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

Rule argument

Additional information

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

Proof step 158 from proof finreach-fin (previous step) (back to tree)

A spec-lemma

Proof step 159 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 160:

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

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 ⊦ n < # x → (x + a ')[n] = x[n]; (s) ⊦ m < n → m ≤ n; (s)

Proof step 160 from proof finreach-fin (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 161:

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

• Proof step 162:

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

• Proof step 172:

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

Rule argument

Additional information

Used terms: n0, x0 + a ', a0 '

Proof step 161 from proof finreach-fin (previous step) (back to tree)

A spec-lemma

Proof step 162 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 163:

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

Rule argument

Additional information

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

Proof step 163 from proof finreach-fin (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 164:

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

Rule argument

Additional information

Used terms: n0

Proof step 164 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 165:

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

Rule argument

Additional information

Proof step 165 from proof finreach-fin (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 166:

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

• Proof step 167:

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

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: a0 ', x0 + a ', n0

Proof step 166 from proof finreach-fin (previous step) (back to tree)

A spec-lemma

Proof step 167 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 168:

  # s1 ≠ 0, # s0 ≠ 0, # s ≠ 0, n0 ≠ 0, s ≠ ∅, s0 ≠ ∅, s1 ≠ ∅, x0 ≠ [], n0 < # x0, edge(g)(x0.last, a), edge(g)(x0[n0 - 1], x0[n0]), a ∈ s0, a0 ∈ s, x0.last ∈ s1, ¬ edge(g)((a0 ' + x0 + a ')[n0], x0[n0]), ∀ n. ¬ # x0 < n → dom(g)((a0 ' + x0)[n]), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s ⊦

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 168 from proof finreach-fin (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 169:

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

Rule argument

Additional information

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

Proof step 169 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 170:

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

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 + 1 ≠ 0; (s)

Proof step 170 from proof finreach-fin (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 171:

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

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ 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: x0, a ', m

Proof step 171 from proof finreach-fin (previous step) (back to tree)

A spec-lemma

Proof step 172 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 173:

  # s ≠ 0, # s0 ≠ 0, # s1 ≠ 0, s ≠ ∅, s0 ≠ ∅, s1 ≠ ∅, x0 ≠ [], edge(g)(x0.last, a), x0.last ∈ s1, a0 ∈ s, a ∈ s0, ¬ edge(g)(a0, x0.head), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ n. n < # x0 → edge(g)((a0 ' + x0)[n], x0[n]), ∀ n. ¬ # x0 < n → dom(g)((a0 ' + x0)[n]) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ x ≠ [] → x[0] = x.head; (s) ⊦ a '[0] = a; (s) ⊦ # x = 0 ↔ x = []; (s) ⊦ 0 < m ↔ m ≠ 0; (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 173 from proof finreach-fin (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 174:

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

Rule argument

Additional information

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

Proof step 174 from proof finreach-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 175:

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

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a + x = a ' + x; (s) ⊦ m +1 = m + 1; (s) ⊦ #(a ' + x) = (# x)+1; (s) 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 ' ≠ []; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s)

Proof step 175 from proof finreach-fin (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