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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 2:

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

Rule argument

Additional information

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

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

User applied rule structural induction

And obtained the following new goals

• Proof step 3:

  ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s ⊦ ∃ s0. ∀ a. reach≤(g)(s, 0)(a) ↔ a ∈ s0

• Proof step 12:

  ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ g, s. (∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s) → (∃ 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 3 from proof finreachle-fin (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 4:

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

• Proof step 5:

  ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∃ s0. ∀ a. reach(g)(s, 0)(a) ↔ a ∈ s0 ⊦ ∃ 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); Used terms: g, s, 0

Proof step 4 from proof finreachle-fin (previous step) (back to tree)

Lemma finreach-fin

Proof step 5 from proof finreachle-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  ∀ a. reach(g)(s, 0)(a) ↔ a ∈ s0, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s ⊦ ∃ s0. ∀ a. reach≤(g)(s, 0)(a) ↔ a ∈ s0

Rule argument

Additional information

Proof step 6 from proof finreachle-fin (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 7:

  ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. reach(g)(s, 0)(a) ↔ a ∈ s0 ⊦ ∀ a. reach≤(g)(s, 0)(a) ↔ a ∈ s0

Rule argument

Additional information

Used terms: s0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  ¬(reach≤(g)(s, 0)(a) ↔ a ∈ s0), ∀ a. reach(g)(s, 0)(a) ↔ a ∈ s0, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

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

• Proof step 10:

  ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. reach(g)(s, 0)(a) ↔ a ∈ s0 ⊦ (∃ m. m ≤ 0 ∧ reach(g)(s, m)(a)) ↔ a ∈ s0

Rule argument

Additional information

Used terms: a, 0, s, g

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

Lemma reachle-def

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  ¬(reach(g)(s, 0)(a) ↔ a ∈ s0), ∀ a. reach(g)(s, 0)(a) ↔ a ∈ s0, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m ≤ 0 ↔ m = 0; (s)

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

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: a

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

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

Rule argument

Additional information

Used simplifier rules: ⊦ m +1 = m + 1; (s)

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

User applied rule all left

And obtained the following new goals

• Proof step 14:

  (∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s) → (∃ s0. ∀ a. reach≤(g)(s, n0)(a) ↔ a ∈ s0), ∀ 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 14 from proof finreachle-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

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

Rule argument

Additional information

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 16:

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

• Proof step 17:

  ∀ a. reach≤(g)(s, n0)(a) ↔ a ∈ s0, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∃ s0. ∀ a. reach(g)(s, n0 + 1)(a) ↔ a ∈ s0 ⊦ ∃ 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, s, n0 + 1

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

Lemma finreach-fin

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

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

Rule argument

Additional information

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

User applied rule exists right

And obtained the following new goals

• Proof step 19:

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

Rule argument

Additional information

Used terms: s0 ∪ s1

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

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

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 21:

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

• Proof step 22:

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

Rule argument

Additional information

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

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

Lemma reachle-def

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

User applied rule all left

And obtained the following new goals

• Proof step 23:

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

Rule argument

Additional information

Used terms: a

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

User applied rule all left

And obtained the following new goals

• Proof step 24:

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

Rule argument

Additional information

Used terms: a

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 25:

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

• Proof step 26:

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

Rule argument

Additional information

Used terms: a, n0, s, g

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

Lemma reachle-def

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

User applied rule case distinction

And obtained the following new goals

• Proof step 27:

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

• Proof step 29:

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

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

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

Rule argument

Additional information

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

User applied rule exists right

And closed the goal!

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 30:

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

Rule argument

Additional information

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

User applied rule case distinction

And obtained the following new goals

• Proof step 31:

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

• Proof step 33:

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

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 32:

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

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

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 34:

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

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

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

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