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 structural induction

And obtained the following new goals

• Proof step 6:

  ∀ pelem, a, b. (∃ c. pelem(a, c) ∧ rtc(n, pelem)(c, b)) ↔ (∃ c. rtc(n, pelem)(a, c) ∧ pelem(c, b)) ⊦ (∃ c. pelem(a, c) ∧ rtc(n +1, 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 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, b. (∃ c. pelem(a, c) ∧ rtc(n, pelem)(c, b)) ↔ (∃ c. rtc(n, pelem)(a, c) ∧ pelem(c, b)) ⊦ (∃ c. pelem(a, c) ∧ (∃ c0. pelem(c, c0) ∧ rtc(n, pelem)(c0, 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 7 from proof rtc-last (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 8:

  ∀ pelem, a, b. (∃ c. pelem(a, c) ∧ rtc(n, pelem)(c, b)) ↔ (∃ c. rtc(n, pelem)(a, c) ∧ pelem(c, b)), ∃ c. pelem(a, c) ∧ (∃ c0. pelem(c, c0) ∧ rtc(n, pelem)(c0, b)) ⊦ ∃ c. (∃ c0. pelem(a, c0) ∧ rtc(n, pelem)(c0, c)) ∧ pelem(c, b)

• Proof step 16:

  ∀ pelem, a, b. (∃ c. pelem(a, c) ∧ rtc(n, pelem)(c, b)) ↔ (∃ c. rtc(n, pelem)(a, c) ∧ pelem(c, b)), ∃ c. (∃ c0. pelem(a, c0) ∧ rtc(n, pelem)(c0, c)) ∧ pelem(c, b) ⊦ ∃ c. pelem(a, c) ∧ (∃ c0. pelem(c, c0) ∧ rtc(n, pelem)(c0, b))

Rule argument

Additional information

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, c), pelem(c, c0), rtc(n, pelem)(c0, b), ∀ pelem, a, b. (∃ c. pelem(a, c) ∧ rtc(n, pelem)(c, 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 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(c, c0), pelem(a, c), rtc(n, pelem)(c0, b), (∃ c0. pelem(c, c0) ∧ rtc(n, pelem)(c0, b)) ↔ (∃ c0. rtc(n, pelem)(c, c0) ∧ pelem(c0, b)) ⊦ ∃ c. (∃ c0. pelem(a, c0) ∧ rtc(n, pelem)(c0, c)) ∧ pelem(c, b)

Rule argument

Additional information

Used terms: pelem, c, b

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

User applied rule case distinction

And obtained the following new goals

• Proof step 11:

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

• Proof step 12:

  pelem(a, c), pelem(c, c0), rtc(n, pelem)(c0, b), ∃ c0. rtc(n, pelem)(c, c0) ∧ pelem(c0, b), ∃ c0. pelem(c, c0) ∧ rtc(n, pelem)(c0, 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)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: c0

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(c, c2), pelem(c1, b), pelem(c, c0), pelem(a, c), rtc(n, pelem)(c2, b), rtc(n, pelem)(c, c1), rtc(n, pelem)(c0, b) ⊦ ∃ c. (∃ c0. pelem(a, c0) ∧ rtc(n, pelem)(c0, c)) ∧ pelem(c, b)

Rule argument

Additional information

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

User applied rule exists right

And obtained the following new goals

• Proof step 14:

  pelem(a, c), pelem(c, c0), pelem(c1, b), pelem(c, c2), rtc(n, pelem)(c0, b), rtc(n, pelem)(c, c1), rtc(n, pelem)(c2, b) ⊦ (∃ c0. pelem(a, c0) ∧ rtc(n, pelem)(c0, c1)) ∧ pelem(c1, b)

Rule argument

Additional information

Used terms: c1

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(c, c2), pelem(c1, b), pelem(c, c0), pelem(a, c), rtc(n, pelem)(c2, b), rtc(n, pelem)(c, c1), rtc(n, pelem)(c0, b) ⊦ ∃ c0. pelem(a, c0) ∧ rtc(n, pelem)(c0, c1)

Rule argument

Additional information

Proof step 15 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: c

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(a, c0), pelem(c, b), rtc(n, pelem)(c0, c), ∀ pelem, a, b. (∃ c. pelem(a, c) ∧ rtc(n, pelem)(c, b)) ↔ (∃ c. rtc(n, pelem)(a, c) ∧ pelem(c, b)) ⊦ ∃ c. pelem(a, c) ∧ (∃ c0. pelem(c, c0) ∧ rtc(n, pelem)(c0, b))

Rule argument

Additional information

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(c, b), pelem(a, c0), rtc(n, pelem)(c0, c), (∃ c. pelem(c0, c) ∧ rtc(n, pelem)(c, b)) ↔ (∃ c. rtc(n, pelem)(c0, c) ∧ pelem(c, b)) ⊦ ∃ c. pelem(a, c) ∧ (∃ c0. pelem(c, c0) ∧ rtc(n, pelem)(c0, b))

Rule argument

Additional information

Used terms: pelem, c0, b

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

User applied rule case distinction

And obtained the following new goals

• Proof step 19:

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

• Proof step 20:

  pelem(a, c0), pelem(c, b), rtc(n, pelem)(c0, c), ∃ c. rtc(n, pelem)(c0, c) ∧ pelem(c, b), ∃ c. pelem(c0, 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)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: c

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(c0, c2), pelem(c1, b), pelem(c, b), pelem(a, c0), rtc(n, pelem)(c2, b), rtc(n, pelem)(c0, c1), rtc(n, pelem)(c0, c) ⊦ ∃ c. pelem(a, c) ∧ (∃ c0. pelem(c, c0) ∧ rtc(n, pelem)(c0, b))

Rule argument

Additional information

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

User applied rule exists right

And obtained the following new goals

• Proof step 22:

  pelem(a, c0), pelem(c, b), pelem(c1, b), pelem(c0, c2), rtc(n, pelem)(c0, c), rtc(n, pelem)(c0, c1), rtc(n, pelem)(c2, b) ⊦ pelem(a, c0) ∧ (∃ c1. pelem(c0, c1) ∧ rtc(n, pelem)(c1, b))

Rule argument

Additional information

Used terms: c0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  pelem(c0, c2), pelem(c1, b), pelem(c, b), pelem(a, c0), rtc(n, pelem)(c2, b), rtc(n, pelem)(c0, c1), rtc(n, pelem)(c0, c) ⊦ ∃ c1. pelem(c0, c1) ∧ rtc(n, pelem)(c1, b)

Rule argument

Additional information

Proof step 23 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: c2