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, a, b) ↔ (∃ c. rtc(n - 1, a, c) ∧ p(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, a, b) ↔ (∃ c. rtc(n - 1, a, c) ∧ p(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, a, b) ↔ (∃ c. rtc(n0, a, c) ∧ p(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. p(a, c) ∧ rtc(n0, c, b)) ↔ (∃ c. rtc(n0, a, c) ∧ p(c, b))

Rule argument

Additional information

Used simplifier rules: rtc-rec: ⊦ rtc(n + 1, a, b) ↔ (∃ c. p(a, c) ∧ rtc(n, 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. p(a, c) ∧ rtc(n0, c, b) ⊦ ∃ c. rtc(n0, a, c) ∧ p(c, b)

• Proof step 14:

  ∃ c. rtc(n0, a, c) ∧ p(c, b) ⊦ ∃ c. p(a, c) ∧ rtc(n0, 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:

  p(a, b0), rtc(n0, b0, b) ⊦ ∃ c. rtc(n0, a, c) ∧ p(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:

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

Rule argument

Additional information

Used simplifier rules: rtc-base: ⊦ rtc(0, 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:

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

Rule argument

Additional information

Used simplifier rules: rtc-rec: ⊦ rtc(n + 1, a, b) ↔ (∃ c. p(a, c) ∧ rtc(n, 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:

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

Rule argument

Additional information

Used terms: 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:

  p(a, b0), p(b0, a0), p(a1, b), rtc(n, a0, b), rtc(n, b0, a1), ∀ a, b0, b. p(a, b0) ∧ rtc(n, b0, b) → (∃ c. rtc(n, a, c) ∧ p(c, b)) ⊦ ∃ c. (∃ c0. p(a, c0) ∧ rtc(n, c0, c)) ∧ p(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:

  p(a1, b), p(b0, a0), p(a, b0), rtc(n, b0, a1), rtc(n, a0, b), ∀ a, b0, b. p(a, b0) ∧ rtc(n, b0, b) → (∃ c. rtc(n, a, c) ∧ p(c, b)) ⊦ (∃ c0. p(a, c0) ∧ rtc(n, c0, a1)) ∧ p(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:

  p(a, b0), p(b0, a0), p(a1, b), rtc(n, a0, b), rtc(n, b0, a1), ∀ a, b0, b. p(a, b0) ∧ rtc(n, b0, b) → (∃ c. rtc(n, a, c) ∧ p(c, b)) ⊦ ∃ c0. p(a, c0) ∧ rtc(n, 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:

  p(b0, b), rtc(n0, a, b0) ⊦ ∃ c. p(a, c) ∧ rtc(n0, 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:

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

Rule argument

Additional information

Used simplifier rules: rtc-base: ⊦ rtc(0, 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:

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

Rule argument

Additional information

Used simplifier rules: rtc-rec: ⊦ rtc(n + 1, a, b) ↔ (∃ c. p(a, c) ∧ rtc(n, 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:

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

Rule argument

Additional information

Used terms: 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:

  p(b0, b), p(a, b1), p(b1, a0), rtc(n, b1, b0), rtc(n, a0, b), ∀ b0, b, a. p(b0, b) ∧ rtc(n, a, b0) → (∃ c. p(a, c) ∧ rtc(n, c, b)) ⊦ ∃ c. p(a, c) ∧ (∃ c0. p(c, c0) ∧ rtc(n, 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:

  p(b1, a0), p(a, b1), p(b0, b), rtc(n, a0, b), rtc(n, b1, b0), ∀ b0, b, a. p(b0, b) ∧ rtc(n, a, b0) → (∃ c. p(a, c) ∧ rtc(n, c, b)) ⊦ ∃ c. p(a, c) ∧ (∃ c0. p(c, c0) ∧ rtc(n, c0, b)), p(a, b1) ∧ (∃ c0. p(b1, c0) ∧ rtc(n, 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:

  p(b0, b), p(a, b1), p(b1, a0), rtc(n, b1, b0), rtc(n, a0, b), ∀ b0, b, a. p(b0, b) ∧ rtc(n, a, b0) → (∃ c. p(a, c) ∧ rtc(n, c, b)) ⊦ ∃ c. p(a, c) ∧ (∃ c0. p(c, c0) ∧ rtc(n, c0, b)), ∃ c0. p(b1, c0) ∧ rtc(n, 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