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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  a[_∃ rhP] ≠ _∃(λ r. a[rhP(r)]) ⊦

Rule argument

Additional information

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

User applied rule expand left

And obtained the following new goals

• Proof step 3:

  ¬(a[_∃ rhP](heap-aux) ↔ (_∃(λ r. a[rhP(r)]))(heap-aux)) ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  ⊦ a[_∃ rhP](heap-aux) ↔ (∃ r. a[rhP(r)](heap-aux))

Rule argument

Additional information

Used simplifier rules: ⊦ (_∃ rR)(ha) ↔ (∃ r. rR(r)(ha)); (s)

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

User applied rule case distinction

And obtained the following new goals

• Proof step 5:

  a[_∃ rhP](heap-aux) ⊦ ∃ r. a[rhP(r)](heap-aux)

• Proof step 16:

  ¬ a[_∃ rhP](heap-aux), ∃ r. a[rhP(r)](heap-aux) ⊦

Rule argument

Additional information

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 6:

  ⊦ ∃ rs, f, g. ha = mk(rs, f, g)

• Proof step 7:

  a[_∃ rhP](heap-aux), ∃ rs, f, g. heap-aux = mk(rs, f, g) ⊦ ∃ r. a[rhP(r)](heap-aux)

Rule argument

Additional information

Used terms: heap-aux

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  a[_∃ rhP](mk(rs, f, g)) ⊦ ∃ r. a[rhP(r)](mk(rs, f, g))

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

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

• Proof step 10:

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

Rule argument

Additional information

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

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

Lemma lift-aux

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

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

Rule argument

Additional information

Used simplifier rules: ⊦ (_∃ rP)(h) ↔ (∃ r. rP(r)(h)); (s)

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

User applied rule exists right

And obtained the following new goals

• Proof step 12:

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

Rule argument

Additional information

Used terms: r

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 13:

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

• Proof step 14:

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

Rule argument

Additional information

Used terms: a, rhP(r), rs, g, f

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

Lemma lift-aux

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  # rs ≠ 0, g(r0) ≠ a, rs ≠ ∅, rhP(r)(mk(rs, f)), r0 ∈ 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 15 from proof lift-ex-r (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: r0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  a[rhP(r)](heap-aux), ¬ a[_∃ rhP](heap-aux) ⊦

Rule argument

Additional information

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 18:

  ⊦ ∃ rs, f, g. ha = mk(rs, f, g)

• Proof step 19:

  a[rhP(r)](heap-aux), ¬ a[_∃ rhP](heap-aux), ∃ rs, f, g. heap-aux = mk(rs, f, g) ⊦

Rule argument

Additional information

Used terms: heap-aux

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  a[rhP(r)](mk(rs, f, g)), ¬ a[_∃ rhP](mk(rs, f, g)) ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 21:

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

• Proof step 22:

  a[rhP(r)](mk(rs, f, g)), ¬ (_∃ rhP)(mk(rs, f)) ∨ (∃ r. ¬(r ∈ rs → g(r) = a)) ⊦

Rule argument

Additional information

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

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

Lemma lift-aux

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  a[rhP(r)](mk(rs, f, g)), ¬(∃ r. rhP(r)(mk(rs, f))) ∨ ¬(r0 ∈ rs → g(r0) = a) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ (_∃ rP)(h) ↔ (∃ r. rP(r)(h)); (s)

Proof step 23 from proof lift-ex-r (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:

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

Rule argument

Additional information

Used terms: a, rhP(r), rs, g, f

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

Lemma lift-aux

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 26:

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

Rule argument

Additional information

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

User applied rule case distinction

And obtained the following new goals

• Proof step 27:

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

• Proof step 28:

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

Rule argument

Additional information

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

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: r

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 29:

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

Rule argument

Additional information

Proof step 29 from proof lift-ex-r (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: r0