Proof step 1 from proof lift-ex-o (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  a[_∃ ohP] ≠ _∃(λ o, a0. a[ohP(o)]) ⊦

Rule argument

Additional information

Proof step 2 from proof lift-ex-o (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 3:

  ⊦ hR0 = hR1 ↔ (∀ rs, f, g. hR0[rs, f, g] ↔ hR1[rs, f, g])

• Proof step 4:

  ∃ rs, f, g. ¬(a[_∃ ohP][rs, f, g] ↔ (_∃(λ o, a0. a[ohP(o)]))[rs, f, g]) ⊦

Rule argument

Additional information

Used terms: a[_∃ ohP], _∃(λ o, a0. a[ohP(o)])

Proof step 3 from proof lift-ex-o (previous step) (back to tree)

A spec-lemma

Proof step 4 from proof lift-ex-o (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  ¬(a[_∃ ohP][rs, f, g] ↔ (_∃(λ o, a0. a[ohP(o)]))[rs, f, g]) ⊦

Rule argument

Additional information

Proof step 5 from proof lift-ex-o (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

  ⊦ hR[rs, f, g] ↔ hR(mk(rs, f, g))

• Proof step 7:

  ¬(a[_∃ ohP](mk(rs, f, g)) ↔ (_∃(λ o, a0. a[ohP(o)]))[rs, f, g]) ⊦

Rule argument

Additional information

Used terms: a[_∃ ohP], rs, f, g

Proof step 6 from proof lift-ex-o (previous step) (back to tree)

A spec-lemma

Proof step 7 from proof lift-ex-o (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 8:

  ⊦ hR[rs, f, g] ↔ hR(mk(rs, f, g))

• Proof step 9:

  ¬(a[_∃ ohP](mk(rs, f, g)) ↔ (_∃(λ o, a0. a[ohP(o)]))(mk(rs, f, g))) ⊦

Rule argument

Additional information

Used terms: _∃(λ o, a0. a[ohP(o)]), rs, f, g

Proof step 8 from proof lift-ex-o (previous step) (back to tree)

A spec-lemma

Proof step 9 from proof lift-ex-o (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

  ⊦ a[hP](mk(rs, f, g)) ↔ hP(mk(rs, f)) ∧ (∀ r. r ∈ rs → g(r) = a)

• Proof step 11:

  ⊦ (_∃ ohP)(mk(rs, f)) ∧ (∀ r. r ∈ rs → g(r) = a) ↔ (_∃(λ o, a0. a[ohP(o)]))(mk(rs, f, g))

Rule argument

Additional information

Used terms: a, _∃ ohP, rs, g, f

Proof step 10 from proof lift-ex-o (previous step) (back to tree)

Lemma lift-aux

Proof step 11 from proof lift-ex-o (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  ⊦ (∃ o. ohP(o)(mk(rs, f))) ∧ (∀ r. r ∈ rs → g(r) = a) ↔ (_∃(λ o, a0. a[ohP(o)]))(mk(rs, f, g))

Rule argument

Additional information

Used simplifier rules: ⊦ (_∃ oP)(h) ↔ (∃ o. oP(o)(h)); (s)

Proof step 12 from proof lift-ex-o (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 13:

  ⊦ (_∃ oaR)(ha) ↔ (∃ o, a. oaR(o, a)(ha))

• Proof step 14:

  ⊦ (∃ o. ohP(o)(mk(rs, f))) ∧ (∀ r. r ∈ rs → g(r) = a) ↔ (∃ o, a0. a[ohP(o)](mk(rs, f, g)))

Rule argument

Additional information

Used terms: λ o, a0. a[ohP(o)], mk(rs, f, g)

Proof step 13 from proof lift-ex-o (previous step) (back to tree)

A spec-lemma

Proof step 14 from proof lift-ex-o (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  ⊦ (∃ o. ohP(o)(mk(rs, f))) ∧ (∀ r. r ∈ rs → g(r) = a) ↔ (∃ o. a[ohP(o)](mk(rs, f, g)))

Rule argument

Additional information

Proof step 15 from proof lift-ex-o (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 16:

  ∀ r. r ∈ rs → g(r) = a, ∃ o. ohP(o)(mk(rs, f)) ⊦ ∃ o. a[ohP(o)](mk(rs, f, g))

• Proof step 22:

  ∃ o. a[ohP(o)](mk(rs, f, g)) ⊦ (∃ o. ohP(o)(mk(rs, f))) ∧ (∀ r. r ∈ rs → g(r) = a)

Rule argument

Additional information

Proof step 16 from proof lift-ex-o (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  ohP(o)(mk(rs, f)), ∀ r. r ∈ rs → g(r) = a ⊦ ∃ o. a[ohP(o)](mk(rs, f, g))

Rule argument

Additional information

Proof step 17 from proof lift-ex-o (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 18:

  ohP(o)(mk(rs, f)), ¬ a[ohP(o)](mk(rs, f, g)), ∀ r. r ∈ rs → g(r) = a ⊦

Rule argument

Additional information

Used terms: o

Proof step 18 from proof lift-ex-o (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 19:

  ⊦ a[hP](mk(rs, f, g)) ↔ hP(mk(rs, f)) ∧ (∀ r. r ∈ rs → g(r) = a)

• Proof step 20:

  ohP(o)(mk(rs, f)), ∀ r. r ∈ rs → g(r) = a, ¬ ohP(o)(mk(rs, f)) ∨ (∃ r. ¬(r ∈ rs → g(r) = a)) ⊦

Rule argument

Additional information

Used terms: a, ohP(o), rs, g, f

Proof step 19 from proof lift-ex-o (previous step) (back to tree)

Lemma lift-aux

Proof step 20 from proof lift-ex-o (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  g(r) ≠ a, ohP(o)(mk(rs, f)), r ∈ rs, ∀ r. r ∈ rs → g(r) = a ⊦

Rule argument

Additional information

Proof step 21 from proof lift-ex-o (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: r

Proof step 22 from proof lift-ex-o (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  a[ohP(o)](mk(rs, f, g)) ⊦ (∃ o. ohP(o)(mk(rs, f))) ∧ (r ∈ rs → g(r) = a)

Rule argument

Additional information

Proof step 23 from proof lift-ex-o (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 24:

  ⊦ a[hP](mk(rs, f, g)) ↔ hP(mk(rs, f)) ∧ (∀ r. r ∈ rs → g(r) = a)

• Proof step 25:

  ohP(o)(mk(rs, f)), ∀ r. r ∈ rs → g(r) = a ⊦ (∃ o. ohP(o)(mk(rs, f))) ∧ (r ∈ rs → g(r) = a)

Rule argument

Additional information

Used terms: a, ohP(o), rs, g, f

Proof step 24 from proof lift-ex-o (previous step) (back to tree)

Lemma lift-aux

Proof step 25 from proof lift-ex-o (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 26:

  ohP(o)(mk(rs, f)), ∀ r. r ∈ rs → g(r) = a ⊦ ∃ o. ohP(o)(mk(rs, f))

• Proof step 27:

  g(r) ≠ a, ohP(o)(mk(rs, f)), r ∈ rs, ∀ r. r ∈ rs → g(r) = a ⊦

Rule argument

Additional information

Proof step 26 from proof lift-ex-o (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: o

Proof step 27 from proof lift-ex-o (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

  # rs ≠ 0, g(r) ≠ a, rs ≠ ∅, ohP(o)(mk(rs, f)), r ∈ rs, ∀ r. r ∈ rs → g(r) = a ⊦

Rule argument

Additional information

Used simplifier rules: size-zero-01: ⊦ s ≠ ∅ → # s ≠ 0; (forward) from specification set-basic[refset] ne-01: ⊦ a ∈ s → s ≠ ∅; (forward) from specification set-basic[refset]

Proof step 28 from proof lift-ex-o (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: r