Proof step 1 from proof ex2-shiftw (conclusion) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 2:

  ((_∃ rrP -* hP))(h) ⊦ ∀ r0, r1. ((rrP(r0, r1) -* hP))(h)

• Proof step 12:

  ¬ ((_∃ rrP -* hP))(h), ∀ r0, r1. ((rrP(r0, r1) -* hP))(h) ⊦

Rule argument

Additional information

Proof step 2 from proof ex2-shiftw (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ((_∃ rrP -* hP))(h), ¬ ((rrP(r0, r1) -* hP))(h) ⊦

Rule argument

Additional information

Proof step 3 from proof ex2-shiftw (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

  ⊦ ((hP0 -* hP1))(h) ↔ (∀ h1. h1 ⊥ h ∧ hP0(h1) → hP1(h1 ∪ h))

• Proof step 5:

  ¬ ((rrP(r0, r1) -* hP))(h), ∀ h1. h1 ⊥ h ∧ (_∃ rrP)(h1) → hP(h1 ∪ h) ⊦

Rule argument

Additional information

Used terms: h, hP, _∃ rrP

Proof step 4 from proof ex2-shiftw (previous step) (back to tree)

A spec-lemma

Proof step 5 from proof ex2-shiftw (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  ¬ ((rrP(r0, r1) -* hP))(h), ∀ h1. h1 ⊥ h ∧ (∃ r0, r1. rrP(r0, r1)(h1)) → hP(h1 ∪ h) ⊦

Rule argument

Additional information

Used simplifier rules: ex2: ⊦ (_∃ rrP)(h) ↔ (∃ r0, r1. rrP(r0, r1)(h));

Proof step 6 from proof ex2-shiftw (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

  ⊦ ((hP0 -* hP1))(h) ↔ (∀ h1. h1 ⊥ h ∧ hP0(h1) → hP1(h1 ∪ h))

• Proof step 8:

  ∀ h1. h1 ⊥ h ∧ (∃ r0, r1. rrP(r0, r1)(h1)) → hP(h1 ∪ h), ∃ h1. ¬(h1 ⊥ h ∧ rrP(r0, r1)(h1) → hP(h1 ∪ h)) ⊦

Rule argument

Additional information

Used terms: h, hP, rrP(r0, r1)

Proof step 7 from proof ex2-shiftw (previous step) (back to tree)

A spec-lemma

Proof step 8 from proof ex2-shiftw (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  rrP(r0, r1)(h1), h1 ⊥ h, ¬ hP(h1 ∪ h), ∀ h1. h1 ⊥ h ∧ (∃ r0, r1. rrP(r0, r1)(h1)) → hP(h1 ∪ h) ⊦

Rule argument

Additional information

Proof step 9 from proof ex2-shiftw (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 10:

  rrP(r0, r1)(h1), h1 ⊥ h, ¬ hP(h1 ∪ h), h1 ⊥ h ∧ (∃ r0, r1. rrP(r0, r1)(h1)) → hP(h1 ∪ h), ∀ h1. h1 ⊥ h ∧ (∃ r0, r1. rrP(r0, r1)(h1)) → hP(h1 ∪ h) ⊦

Rule argument

Additional information

Used terms: h1

Proof step 10 from proof ex2-shiftw (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  rrP(r0, r1)(h1), h1 ⊥ h, ¬ hP(h1 ∪ h), ∀ h1. h1 ⊥ h ∧ (∃ r0, r1. rrP(r0, r1)(h1)) → hP(h1 ∪ h) ⊦ ∃ r0, r1. rrP(r0, r1)(h1)

Rule argument

Additional information

Proof step 11 from proof ex2-shiftw (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: r0, r1

Proof step 12 from proof ex2-shiftw (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 13:

  ⊦ ((hP0 -* hP1))(h) ↔ (∀ h1. h1 ⊥ h ∧ hP0(h1) → hP1(h1 ∪ h))

• Proof step 14:

  ∀ r0, r1. ((rrP(r0, r1) -* hP))(h), ∃ h1. ¬(h1 ⊥ h ∧ (_∃ rrP)(h1) → hP(h1 ∪ h)) ⊦

Rule argument

Additional information

Used terms: h, hP, _∃ rrP

Proof step 13 from proof ex2-shiftw (previous step) (back to tree)

A spec-lemma

Proof step 14 from proof ex2-shiftw (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  rrP(r0, r1)(h1), h1 ⊥ h, ¬ hP(h1 ∪ h), ∀ r0, r1. ((rrP(r0, r1) -* hP))(h) ⊦

Rule argument

Additional information

Used simplifier rules: ex2: ⊦ (_∃ rrP)(h) ↔ (∃ r0, r1. rrP(r0, r1)(h));

Proof step 15 from proof ex2-shiftw (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 16:

  ((rrP(r0, r1) -* hP))(h), rrP(r0, r1)(h1), h1 ⊥ h, ¬ hP(h1 ∪ h), ∀ r0, r1. ((rrP(r0, r1) -* hP))(h) ⊦

Rule argument

Additional information

Used terms: r0, r1

Proof step 16 from proof ex2-shiftw (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 17:

  ⊦ ((hP0 -* hP1))(h) ↔ (∀ h1. h1 ⊥ h ∧ hP0(h1) → hP1(h1 ∪ h))

• Proof step 18:

  rrP(r0, r1)(h1), h1 ⊥ h, ¬ hP(h1 ∪ h), ∀ r0, r1. ((rrP(r0, r1) -* hP))(h), ∀ h1. h1 ⊥ h ∧ rrP(r0, r1)(h1) → hP(h1 ∪ h) ⊦

Rule argument

Additional information

Used terms: h, hP, rrP(r0, r1)

Proof step 17 from proof ex2-shiftw (previous step) (back to tree)

A spec-lemma

Proof step 18 from proof ex2-shiftw (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: h1