Proof step 1 from proof rtc-last (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  n ≠ 0 ⊦ rtc(n, pelem)(a, b) ↔ (∃ c. rtc(n - 1, pelem)(a, c) ∧ pelem(c, b))

Rule argument

Additional information

Proof step 2 from proof rtc-last (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  n ≠ 0 ⊦ rtc(n, pelem)(a, b) ↔ (∃ c. rtc(n - 1, pelem)(a, c) ∧ pelem(c, b))

Rule argument

Additional information

Proof step 3 from proof rtc-last (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 4:

  n = n0 + 1, n ≠ 0 ⊦ rtc(n, pelem)(a, b) ↔ (∃ c. rtc(n0, pelem)(a, c) ∧ pelem(c, b))

Rule argument

Additional information

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

Proof step 4 from proof rtc-last (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  ⊦ (∃ c. pelem(a, c) ∧ rtc(n0, pelem)(c, b)) ↔ (∃ c. rtc(n0, pelem)(a, c) ∧ pelem(c, b))

Rule argument

Additional information

Used simplifier rules: rtc-rec: ⊦ rtc(n + 1, pelem)(a, b) ↔ (∃ c. pelem(a, c) ∧ rtc(n, pelem)(c, b)); c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m + 1 ≠ 0; (s)

Proof step 5 from proof rtc-last (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 6:

  ∃ c. pelem(a, c) ∧ rtc(n0, pelem)(c, b) ⊦ ∃ c. rtc(n0, pelem)(a, c) ∧ pelem(c, b)

• Proof step 14:

  ∃ c. rtc(n0, pelem)(a, c) ∧ pelem(c, b) ⊦ ∃ c. pelem(a, c) ∧ rtc(n0, pelem)(c, b)

Rule argument

Additional information

Proof step 6 from proof rtc-last (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  pelem(a, b0), rtc(n0, pelem)(b0, b) ⊦ ∃ c. rtc(n0, pelem)(a, c) ∧ pelem(c, b)

Rule argument

Additional information

Proof step 7 from proof rtc-last (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 8:

  pelem(a, b0), rtc(n +1, pelem)(b0, b), ∀ pelem, a, b0, b. pelem(a, b0) ∧ rtc(n, pelem)(b0, b) → (∃ c. rtc(n, pelem)(a, c) ∧ pelem(c, b)) ⊦ ∃ c. rtc(n +1, pelem)(a, c) ∧ pelem(c, b)

Rule argument

Additional information

Used simplifier rules: rtc-base: ⊦ rtc(0, pelem)(a, b) ↔ a = b; nat freely generated by 0, +1;;

Proof step 8 from proof rtc-last (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  pelem(a, b0), pelem(b0, a0), rtc(n, pelem)(a0, b), ∀ pelem, a, b0, b. pelem(a, b0) ∧ rtc(n, pelem)(b0, b) → (∃ c. rtc(n, pelem)(a, c) ∧ pelem(c, b)) ⊦ ∃ c. (∃ c0. pelem(a, c0) ∧ rtc(n, pelem)(c0, c)) ∧ pelem(c, b)

Rule argument

Additional information

Used simplifier rules: rtc-rec: ⊦ rtc(n + 1, pelem)(a, b) ↔ (∃ c. pelem(a, c) ∧ rtc(n, pelem)(c, b)); c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m +1 = m + 1; (s)

Proof step 9 from proof rtc-last (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 10:

  pelem(b0, a0), pelem(a, b0), rtc(n, pelem)(a0, b), pelem(b0, a0) ∧ rtc(n, pelem)(a0, b) → (∃ c. rtc(n, pelem)(b0, c) ∧ pelem(c, b)), ∀ pelem, a, b0, b. pelem(a, b0) ∧ rtc(n, pelem)(b0, b) → (∃ c. rtc(n, pelem)(a, c) ∧ pelem(c, b)) ⊦ ∃ c. (∃ c0. pelem(a, c0) ∧ rtc(n, pelem)(c0, c)) ∧ pelem(c, b)

Rule argument

Additional information

Used terms: pelem, b0, a0, b

Proof step 10 from proof rtc-last (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  pelem(a, b0), pelem(b0, a0), pelem(a1, b), rtc(n, pelem)(a0, b), rtc(n, pelem)(b0, a1), ∀ pelem, a, b0, b. pelem(a, b0) ∧ rtc(n, pelem)(b0, b) → (∃ c. rtc(n, pelem)(a, c) ∧ pelem(c, b)) ⊦ ∃ c. (∃ c0. pelem(a, c0) ∧ rtc(n, pelem)(c0, c)) ∧ pelem(c, b)

Rule argument

Additional information

Proof step 11 from proof rtc-last (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 12:

  pelem(a1, b), pelem(b0, a0), pelem(a, b0), rtc(n, pelem)(b0, a1), rtc(n, pelem)(a0, b), ∀ pelem, a, b0, b. pelem(a, b0) ∧ rtc(n, pelem)(b0, b) → (∃ c. rtc(n, pelem)(a, c) ∧ pelem(c, b)) ⊦ ∃ c. (∃ c0. pelem(a, c0) ∧ rtc(n, pelem)(c0, c)) ∧ pelem(c, b), (∃ c0. pelem(a, c0) ∧ rtc(n, pelem)(c0, a1)) ∧ pelem(a1, b)

Rule argument

Additional information

Used terms: a1

Proof step 12 from proof rtc-last (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  pelem(a, b0), pelem(b0, a0), pelem(a1, b), rtc(n, pelem)(a0, b), rtc(n, pelem)(b0, a1), ∀ pelem, a, b0, b. pelem(a, b0) ∧ rtc(n, pelem)(b0, b) → (∃ c. rtc(n, pelem)(a, c) ∧ pelem(c, b)) ⊦ ∃ c. (∃ c0. pelem(a, c0) ∧ rtc(n, pelem)(c0, c)) ∧ pelem(c, b), ∃ c0. pelem(a, c0) ∧ rtc(n, pelem)(c0, a1)

Rule argument

Additional information

Proof step 13 from proof rtc-last (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: b0

Proof step 14 from proof rtc-last (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  pelem(b0, b), rtc(n0, pelem)(a, b0) ⊦ ∃ c. pelem(a, c) ∧ rtc(n0, pelem)(c, b)

Rule argument

Additional information

Proof step 15 from proof rtc-last (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 16:

  pelem(b0, b), rtc(n +1, pelem)(a, b0), ∀ pelem, b0, b, a. pelem(b0, b) ∧ rtc(n, pelem)(a, b0) → (∃ c. pelem(a, c) ∧ rtc(n, pelem)(c, b)) ⊦ ∃ c. pelem(a, c) ∧ rtc(n +1, pelem)(c, b)

Rule argument

Additional information

Used simplifier rules: rtc-base: ⊦ rtc(0, pelem)(a, b) ↔ a = b; nat freely generated by 0, +1;;

Proof step 16 from proof rtc-last (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  pelem(b0, b), pelem(a, b1), rtc(n, pelem)(b1, b0), ∀ pelem, b0, b, a. pelem(b0, b) ∧ rtc(n, pelem)(a, b0) → (∃ c. pelem(a, c) ∧ rtc(n, pelem)(c, b)) ⊦ ∃ c. pelem(a, c) ∧ (∃ c0. pelem(c, c0) ∧ rtc(n, pelem)(c0, b))

Rule argument

Additional information

Used simplifier rules: rtc-rec: ⊦ rtc(n + 1, pelem)(a, b) ↔ (∃ c. pelem(a, c) ∧ rtc(n, pelem)(c, b)); c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m +1 = m + 1; (s)

Proof step 17 from proof rtc-last (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 18:

  pelem(a, b1), pelem(b0, b), rtc(n, pelem)(b1, b0), pelem(b0, b) ∧ rtc(n, pelem)(b1, b0) → (∃ c. pelem(b1, c) ∧ rtc(n, pelem)(c, b)), ∀ pelem, b0, b, a. pelem(b0, b) ∧ rtc(n, pelem)(a, b0) → (∃ c. pelem(a, c) ∧ rtc(n, pelem)(c, b)) ⊦ ∃ c. pelem(a, c) ∧ (∃ c0. pelem(c, c0) ∧ rtc(n, pelem)(c0, b))

Rule argument

Additional information

Used terms: pelem, b0, b, b1

Proof step 18 from proof rtc-last (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  pelem(b0, b), pelem(a, b1), pelem(b1, a0), rtc(n, pelem)(b1, b0), rtc(n, pelem)(a0, b), ∀ pelem, b0, b, a. pelem(b0, b) ∧ rtc(n, pelem)(a, b0) → (∃ c. pelem(a, c) ∧ rtc(n, pelem)(c, b)) ⊦ ∃ c. pelem(a, c) ∧ (∃ c0. pelem(c, c0) ∧ rtc(n, pelem)(c0, b))

Rule argument

Additional information

Proof step 19 from proof rtc-last (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 20:

  pelem(b1, a0), pelem(a, b1), pelem(b0, b), rtc(n, pelem)(a0, b), rtc(n, pelem)(b1, b0), ∀ pelem, b0, b, a. pelem(b0, b) ∧ rtc(n, pelem)(a, b0) → (∃ c. pelem(a, c) ∧ rtc(n, pelem)(c, b)) ⊦ ∃ c. pelem(a, c) ∧ (∃ c0. pelem(c, c0) ∧ rtc(n, pelem)(c0, b)), pelem(a, b1) ∧ (∃ c0. pelem(b1, c0) ∧ rtc(n, pelem)(c0, b))

Rule argument

Additional information

Used terms: b1

Proof step 20 from proof rtc-last (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  pelem(b0, b), pelem(a, b1), pelem(b1, a0), rtc(n, pelem)(b1, b0), rtc(n, pelem)(a0, b), ∀ pelem, b0, b, a. pelem(b0, b) ∧ rtc(n, pelem)(a, b0) → (∃ c. pelem(a, c) ∧ rtc(n, pelem)(c, b)) ⊦ ∃ c. pelem(a, c) ∧ (∃ c0. pelem(c, c0) ∧ rtc(n, pelem)(c0, b)), ∃ c0. pelem(b1, c0) ∧ rtc(n, pelem)(c0, b)

Rule argument

Additional information

Proof step 21 from proof rtc-last (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: a0