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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(p*(a, b) ↔ a = b ∨ p+(a, b)) ⊦

Rule argument

Additional information

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

User applied rule case distinction

And obtained the following new goals

• Proof step 3:

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

• Proof step 10:

  ¬ p*(a, b), a = b ∨ p+(a, b) ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

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

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 5:

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

• Proof step 6:

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

Rule argument

Additional information

Used terms: b, a

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

Lemma rtc+

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

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

• Proof step 8:

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

Rule argument

Additional information

Used terms: b, a

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

Lemma rtc

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

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

Rule argument

Additional information

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

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

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

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

• Proof step 13:

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

Rule argument

Additional information

Used terms: b, a

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

Lemma rtc+

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  a ≠ b, n ≠ 0, rtc(n, a, b), ¬ p*(a, b) ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

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

• Proof step 16:

  a ≠ b, n ≠ 0, rtc(n, a, b), ∀ n. ¬ rtc(n, a, b) ⊦

Rule argument

Additional information

Used terms: b, a

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

Lemma rtc

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: n