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

User applied rule case distinction

And obtained the following new goals

• Proof step 2:

  (_∃ bcdP -* hP)(h) ⊦ ∀ b, c, d. (bcdP(b, c, d) -* hP)(h)

• Proof step 12:

  ¬ (_∃ bcdP -* hP)(h), ∀ b, c, d. (bcdP(b, c, d) -* hP)(h) ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  (_∃ bcdP -* hP)(h), ¬ (bcdP(b, c, d) -* hP)(h) ⊦

Rule argument

Additional information

Proof step 3 from proof ex3-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:

  ¬ (bcdP(b, c, d) -* hP)(h), ∀ h1. h1 ⊥ h ∧ (_∃ bcdP)(h1) → hP(h1 ∪ h) ⊦

Rule argument

Additional information

Used terms: _∃ bcdP, hP, h

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  ¬ (bcdP(b, c, d) -* hP)(h), ∀ h1. h1 ⊥ h ∧ (∃ b, c, d. bcdP(b, c, d)(h1)) → hP(h1 ∪ h) ⊦

Rule argument

Additional information

Used simplifier rules: ex3: ⊦ (_∃ bcdP)(h) ↔ (∃ b, c, d. bcdP(b, c, d)(h));

Proof step 6 from proof ex3-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 ∧ (∃ b, c, d. bcdP(b, c, d)(h1)) → hP(h1 ∪ h), ∃ h1. ¬(h1 ⊥ h ∧ bcdP(b, c, d)(h1) → hP(h1 ∪ h)) ⊦

Rule argument

Additional information

Used terms: bcdP(b, c, d), hP, h

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  bcdP(b, c, d)(h1), h1 ⊥ h, ¬ hP(h1 ∪ h), ∀ h1. h1 ⊥ h ∧ (∃ b, c, d. bcdP(b, c, d)(h1)) → hP(h1 ∪ h) ⊦

Rule argument

Additional information

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

User applied rule all left

And obtained the following new goals

• Proof step 10:

  bcdP(b, c, d)(h1), h1 ⊥ h, ¬ hP(h1 ∪ h), ∀ h1. h1 ⊥ h ∧ (∃ b, c, d. bcdP(b, c, d)(h1)) → hP(h1 ∪ h), h1 ⊥ h ∧ (∃ b, c, d. bcdP(b, c, d)(h1)) → hP(h1 ∪ h) ⊦

Rule argument

Additional information

Used terms: h1

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  bcdP(b, c, d)(h1), h1 ⊥ h, ¬ hP(h1 ∪ h), ∀ h1. h1 ⊥ h ∧ (∃ b, c, d. bcdP(b, c, d)(h1)) → hP(h1 ∪ h) ⊦ ∃ b, c, d. bcdP(b, c, d)(h1)

Rule argument

Additional information

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

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: b, c, d

Proof step 12 from proof ex3-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:

  ∀ b, c, d. (bcdP(b, c, d) -* hP)(h), ∃ h1. ¬(h1 ⊥ h ∧ (_∃ bcdP)(h1) → hP(h1 ∪ h)) ⊦

Rule argument

Additional information

Used terms: _∃ bcdP, hP, h

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  bcdP(b, c, d)(h1), h1 ⊥ h, ¬ hP(h1 ∪ h), ∀ b, c, d. (bcdP(b, c, d) -* hP)(h) ⊦

Rule argument

Additional information

Used simplifier rules: ex3: ⊦ (_∃ bcdP)(h) ↔ (∃ b, c, d. bcdP(b, c, d)(h));

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

User applied rule all left

And obtained the following new goals

• Proof step 16:

  bcdP(b, c, d)(h1), (bcdP(b, c, d) -* hP)(h), h1 ⊥ h, ¬ hP(h1 ∪ h), ∀ b, c, d. (bcdP(b, c, d) -* hP)(h) ⊦

Rule argument

Additional information

Used terms: b, c, d

Proof step 16 from proof ex3-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:

  bcdP(b, c, d)(h1), h1 ⊥ h, ¬ hP(h1 ∪ h), ∀ b, c, d. (bcdP(b, c, d) -* hP)(h), ∀ h1. h1 ⊥ h ∧ bcdP(b, c, d)(h1) → hP(h1 ∪ h) ⊦

Rule argument

Additional information

Used terms: bcdP(b, c, d), hP, h

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

A spec-lemma

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: h1