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

User applied rule case distinction

And obtained the following new goals

• Proof step 2:

  p+(a, b) ⊦ ∃ c. p*(a, c) ∧ p(c, b)

• Proof step 17:

  ¬ p+(a, b), ∃ c. p*(a, c) ∧ p(c, b) ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 3:

  ⊦ p+(a, b) ↔ (∃ n. n ≠ 0 ∧ rtc(n, a, b))

• Proof step 4:

  ∃ n. n ≠ 0 ∧ rtc(n, a, b) ⊦ ∃ c. p*(a, c) ∧ p(c, b)

Rule argument

Additional information

Used terms: b, a

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

Lemma rtc+

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  n ≠ 0, rtc(n, a, b) ⊦ ∃ c. p*(a, c) ∧ p(c, b)

Rule argument

Additional information

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

User applied rule structural induction

And obtained the following new goals

• Proof step 6:

  n0 +1 ≠ 0, rtc(n0 +1, a, b), ∀ a, b. n0 ≠ 0 ∧ rtc(n0, a, b) → (∃ c. p*(a, c) ∧ p(c, b)) ⊦ ∃ c. p*(a, c) ∧ p(c, b)

Rule argument

Additional information

Used simplifier rules: nat freely generated by 0, +1;;

Proof step 6 from proof rtc+-unfold-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), ∀ a, b. n0 ≠ 0 ∧ rtc(n0, a, b) → (∃ c. p*(a, c) ∧ p(c, b)) ⊦ ∃ c. p*(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 = m + 1; (s) ⊦ m + 1 ≠ 0; (s)

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

User applied rule all left

And obtained the following new goals

• Proof step 8:

  p(a, b0), rtc(n0, b0, b), n0 ≠ 0 ∧ rtc(n0, b0, b) → (∃ c. p*(b0, c) ∧ p(c, b)) ⊦ ∃ c. p*(a, c) ∧ p(c, b)

Rule argument

Additional information

Used terms: b0, b

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  p(a, b0), rtc(n0, b0, b), n0 ≠ 0 → p*(b0, a0) ∧ p(a0, b) ⊦ ∃ c. p*(a, c) ∧ p(c, b)

Rule argument

Additional information

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

User applied rule case distinction

And obtained the following new goals

• Proof step 10:

  n0 = 0, p(a, b0), rtc(n0, b0, b) ⊦ ∃ c. p*(a, c) ∧ p(c, b)

• Proof step 12:

  p(a, b0), p(a0, b), p*(b0, a0), rtc(n0, b0, b) ⊦ ∃ c. p*(a, c) ∧ p(c, b)

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  p(a, b) ⊦ ∃ c. p*(a, c) ∧ p(c, b)

Rule argument

Additional information

Used simplifier rules: rtc-base: ⊦ rtc(0, a, b) ↔ a = b;

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

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: rtc-refl: ⊦ p*(a, a); Used terms: a

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  p(a0, b), p(a, b0), p*(b0, a0), rtc(n0, b0, b) ⊦ ∃ c. p*(a, c) ∧ p(c, b)

Rule argument

Additional information

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

User applied rule exists right

And obtained the following new goals

• Proof step 14:

  p(a, b0), p(a0, b), p*(b0, a0), rtc(n0, b0, b) ⊦ ∃ c. p*(a, c) ∧ p(c, b), p*(a, a0) ∧ p(a0, b)

Rule argument

Additional information

Used terms: a0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  p(a0, b), p(a, b0), p*(b0, a0), rtc(n0, b0, b), ¬ p*(a, a0) ⊦ ∃ c. p*(a, c) ∧ p(c, b)

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 16:

  ⊦ p*(a, b) ∧ p*(b, c) → p*(a, c)

Rule argument

Additional information

Used simplifier rules: rtc-one: ⊦ p(a, b) → (p*(a, b) ↔ true); Used terms: b0, a0, a

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

Lemma rtc-trans

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  p(b0, b), p*(a, b0), ¬ p+(a, b) ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 19:

  ⊦ p+(a, b) ↔ (∃ n. n ≠ 0 ∧ rtc(n, a, b))

• Proof step 20:

  p(b0, b), p*(a, b0), ∀ n. ¬(n ≠ 0 ∧ rtc(n, a, b)) ⊦

Rule argument

Additional information

Used terms: b, a

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

Lemma rtc+

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 21:

  ⊦ p*(a, b) ↔ (∃ n. rtc(n, a, b))

• Proof step 22:

  p(b0, b), ∀ n. ¬(n ≠ 0 ∧ rtc(n, a, b)), ∃ n. rtc(n, a, b0) ⊦

Rule argument

Additional information

Used terms: b0, a

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

Lemma rtc

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  p(b0, b), rtc(n, a, b0), ∀ n0. n0 = 0 ∨ ¬ rtc(n0, a, b) ⊦

Rule argument

Additional information

Proof step 23 from proof rtc+-unfold-last (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 24:

  p(b0, b), rtc(n, a, b0), n + 1 = 0 ∨ ¬ rtc(n + 1, a, b) ⊦

Rule argument

Additional information

Used terms: n + 1

Proof step 24 from proof rtc+-unfold-last (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  p(b0, b), rtc(n, a, b0) ⊦ ∃ c. p(a, c) ∧ rtc(n, 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 25 from proof rtc+-unfold-last (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 26:

  p(b0, b), rtc(n0 +1, a, b0), ∀ b0, b, a. p(b0, b) ∧ rtc(n0, a, b0) → (∃ c. p(a, c) ∧ rtc(n0, c, b)) ⊦ ∃ c. p(a, c) ∧ rtc(n0 +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 26 from proof rtc+-unfold-last (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  p(b0, b), p(a, b1), rtc(n0, b1, b0), ∀ b0, b, a. p(b0, b) ∧ rtc(n0, a, b0) → (∃ c. p(a, c) ∧ rtc(n0, c, b)) ⊦ ∃ c. p(a, c) ∧ (∃ c0. p(c, c0) ∧ rtc(n0, 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 27 from proof rtc+-unfold-last (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 28:

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

Rule argument

Additional information

Used terms: b0, b, b1

Proof step 28 from proof rtc+-unfold-last (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 29:

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

Rule argument

Additional information

Proof step 29 from proof rtc+-unfold-last (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 30:

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

Rule argument

Additional information

Used terms: b1

Proof step 30 from proof rtc+-unfold-last (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

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

Rule argument

Additional information

Proof step 31 from proof rtc+-unfold-last (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: a0