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)(a1, a2) ↔ (∃ a. rtc(n - 1, pelem)(a1, a) ∧ pelem(a, a2))

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)(a1, a2) ↔ (∃ a. rtc(n - 1, pelem)(a1, a) ∧ pelem(a, a2))

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)(a1, a2) ↔ (∃ a. rtc(n0, pelem)(a1, a) ∧ pelem(a, a2))

Rule argument

Additional information

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

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:

  ⊦ (∃ a. pelem(a1, a) ∧ rtc(n0, pelem)(a, a2)) ↔ (∃ a. rtc(n0, pelem)(a1, a) ∧ pelem(a, a2))

Rule argument

Additional information

Used simplifier rules: rtc-rec: ⊦ rtc(n + 1, pelem)(a1, a2) ↔ (∃ a. pelem(a1, a) ∧ rtc(n, pelem)(a, a2)); 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, a1, a2. (∃ a. pelem(a1, a) ∧ rtc(n, pelem)(a, a2)) ↔ (∃ a. rtc(n, pelem)(a1, a) ∧ pelem(a, a2)) ⊦ (∃ a. pelem(a1, a) ∧ rtc(n.+1, pelem)(a, a2)) ↔ (∃ a. rtc(n.+1, pelem)(a1, a) ∧ pelem(a, a2))

Rule argument

Additional information

Used simplifier rules: rtc-base: ⊦ rtc(0, pelem)(a1, a2) ↔ a1 = a2; 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, a1, a2. (∃ a. pelem(a1, a) ∧ rtc(n, pelem)(a, a2)) ↔ (∃ a. rtc(n, pelem)(a1, a) ∧ pelem(a, a2)) ⊦ (∃ a. pelem(a1, a) ∧ (∃ a0. pelem(a, a0) ∧ rtc(n, pelem)(a0, a2))) ↔ (∃ a. (∃ a0. pelem(a1, a0) ∧ rtc(n, pelem)(a0, a)) ∧ pelem(a, a2))

Rule argument

Additional information

Used simplifier rules: rtc-rec: ⊦ rtc(n + 1, pelem)(a1, a2) ↔ (∃ a. pelem(a1, a) ∧ rtc(n, pelem)(a, a2)); 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, a1, a2. (∃ a. pelem(a1, a) ∧ rtc(n, pelem)(a, a2)) ↔ (∃ a. rtc(n, pelem)(a1, a) ∧ pelem(a, a2)), ∃ a. pelem(a1, a) ∧ (∃ a0. pelem(a, a0) ∧ rtc(n, pelem)(a0, a2)) ⊦ ∃ a. (∃ a0. pelem(a1, a0) ∧ rtc(n, pelem)(a0, a)) ∧ pelem(a, a2)

• Proof step 16:

  ∀ pelem, a1, a2. (∃ a. pelem(a1, a) ∧ rtc(n, pelem)(a, a2)) ↔ (∃ a. rtc(n, pelem)(a1, a) ∧ pelem(a, a2)), ∃ a. (∃ a0. pelem(a1, a0) ∧ rtc(n, pelem)(a0, a)) ∧ pelem(a, a2) ⊦ ∃ a. pelem(a1, a) ∧ (∃ a0. pelem(a, a0) ∧ rtc(n, pelem)(a0, a2))

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(a1, a), pelem(a, a0), rtc(n, pelem)(a0, a2), ∀ pelem, a1, a2. (∃ a. pelem(a1, a) ∧ rtc(n, pelem)(a, a2)) ↔ (∃ a. rtc(n, pelem)(a1, a) ∧ pelem(a, a2)) ⊦ ∃ a. (∃ a0. pelem(a1, a0) ∧ rtc(n, pelem)(a0, a)) ∧ pelem(a, a2)

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(a, a0), pelem(a1, a), rtc(n, pelem)(a0, a2), (∃ a0. pelem(a, a0) ∧ rtc(n, pelem)(a0, a2)) ↔ (∃ a0. rtc(n, pelem)(a, a0) ∧ pelem(a0, a2)) ⊦ ∃ a. (∃ a0. pelem(a1, a0) ∧ rtc(n, pelem)(a0, a)) ∧ pelem(a, a2)

Rule argument

Additional information

Used terms: pelem, a, a2

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(a1, a), pelem(a, a0), rtc(n, pelem)(a0, a2) ⊦ ∃ a. (∃ a0. pelem(a1, a0) ∧ rtc(n, pelem)(a0, a)) ∧ pelem(a, a2), ∃ a0. rtc(n, pelem)(a, a0) ∧ pelem(a0, a2), ∃ a0. pelem(a, a0) ∧ rtc(n, pelem)(a0, a2)

• Proof step 12:

  pelem(a1, a), pelem(a, a0), rtc(n, pelem)(a0, a2), ∃ a0. rtc(n, pelem)(a, a0) ∧ pelem(a0, a2), ∃ a0. pelem(a, a0) ∧ rtc(n, pelem)(a0, a2) ⊦ ∃ a. (∃ a0. pelem(a1, a0) ∧ rtc(n, pelem)(a0, a)) ∧ pelem(a, a2)

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: a0

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, a4), pelem(a3, a2), pelem(a, a0), pelem(a1, a), rtc(n, pelem)(a4, a2), rtc(n, pelem)(a, a3), rtc(n, pelem)(a0, a2) ⊦ ∃ a. (∃ a0. pelem(a1, a0) ∧ rtc(n, pelem)(a0, a)) ∧ pelem(a, a2)

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(a1, a), pelem(a, a0), pelem(a3, a2), pelem(a, a4), rtc(n, pelem)(a0, a2), rtc(n, pelem)(a, a3), rtc(n, pelem)(a4, a2) ⊦ (∃ a0. pelem(a1, a0) ∧ rtc(n, pelem)(a0, a3)) ∧ pelem(a3, a2)

Rule argument

Additional information

Used terms: a3

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(a, a4), pelem(a3, a2), pelem(a, a0), pelem(a1, a), rtc(n, pelem)(a4, a2), rtc(n, pelem)(a, a3), rtc(n, pelem)(a0, a2) ⊦ ∃ a0. pelem(a1, a0) ∧ rtc(n, pelem)(a0, a3)

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: a

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(a1, a0), pelem(a, a2), rtc(n, pelem)(a0, a), ∀ pelem, a1, a2. (∃ a. pelem(a1, a) ∧ rtc(n, pelem)(a, a2)) ↔ (∃ a. rtc(n, pelem)(a1, a) ∧ pelem(a, a2)) ⊦ ∃ a. pelem(a1, a) ∧ (∃ a0. pelem(a, a0) ∧ rtc(n, pelem)(a0, a2))

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(a, a2), pelem(a1, a0), rtc(n, pelem)(a0, a), (∃ a. pelem(a0, a) ∧ rtc(n, pelem)(a, a2)) ↔ (∃ a. rtc(n, pelem)(a0, a) ∧ pelem(a, a2)) ⊦ ∃ a. pelem(a1, a) ∧ (∃ a0. pelem(a, a0) ∧ rtc(n, pelem)(a0, a2))

Rule argument

Additional information

Used terms: pelem, a0, a2

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(a1, a0), pelem(a, a2), rtc(n, pelem)(a0, a) ⊦ ∃ a. pelem(a1, a) ∧ (∃ a0. pelem(a, a0) ∧ rtc(n, pelem)(a0, a2)), ∃ a. rtc(n, pelem)(a0, a) ∧ pelem(a, a2), ∃ a. pelem(a0, a) ∧ rtc(n, pelem)(a, a2)

• Proof step 20:

  pelem(a1, a0), pelem(a, a2), rtc(n, pelem)(a0, a), ∃ a. rtc(n, pelem)(a0, a) ∧ pelem(a, a2), ∃ a. pelem(a0, a) ∧ rtc(n, pelem)(a, a2) ⊦ ∃ a. pelem(a1, a) ∧ (∃ a0. pelem(a, a0) ∧ rtc(n, pelem)(a0, a2))

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: a

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(a0, a4), pelem(a3, a2), pelem(a, a2), pelem(a1, a0), rtc(n, pelem)(a4, a2), rtc(n, pelem)(a0, a3), rtc(n, pelem)(a0, a) ⊦ ∃ a. pelem(a1, a) ∧ (∃ a0. pelem(a, a0) ∧ rtc(n, pelem)(a0, a2))

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(a1, a0), pelem(a, a2), pelem(a3, a2), pelem(a0, a4), rtc(n, pelem)(a0, a), rtc(n, pelem)(a0, a3), rtc(n, pelem)(a4, a2) ⊦ pelem(a1, a0) ∧ (∃ a1. pelem(a0, a1) ∧ rtc(n, pelem)(a1, a2))

Rule argument

Additional information

Used terms: a0

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(a0, a4), pelem(a3, a2), pelem(a, a2), pelem(a1, a0), rtc(n, pelem)(a4, a2), rtc(n, pelem)(a0, a3), rtc(n, pelem)(a0, a) ⊦ ∃ a1. pelem(a0, a1) ∧ rtc(n, pelem)(a1, a2)

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: a4