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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  a[emp] ≠ emp ⊦

Rule argument

Additional information

Proof step 2 from proof lift-emp (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[emp][rs, f, g] ↔ emp[rs, f, g]) ⊦

Rule argument

Additional information

Used terms: emp, a[emp]

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  ¬(a[emp][rs, f, g] ↔ emp[rs, f, g]) ⊦

Rule argument

Additional information

Proof step 5 from proof lift-emp (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[emp](mk(rs, f, g)) ↔ emp[rs, f, g]) ⊦

Rule argument

Additional information

Used terms: g, f, rs, a[emp]

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

A spec-lemma

Proof step 7 from proof lift-emp (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[emp](mk(rs, f, g)) ↔ emp(mk(rs, f, g))) ⊦

Rule argument

Additional information

Used terms: g, f, rs, emp

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  ¬(a[emp](mk(rs, f, g)) ↔ mk(rs, f, g) = ∅) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ emp(h) ↔ h = ∅; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 11:

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

• Proof step 12:

  ⊦ emp(mk(rs, f)) ∧ (∀ r. r ∈ rs → g(r) = a) ↔ mk(rs, f, g) = ∅

Rule argument

Additional information

Used terms: a, emp, rs, g, f

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

Lemma lift-aux

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

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

Rule argument

Additional information

Used simplifier rules: ⊦ emp(h) ↔ h = ∅; (s)

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

User applied rule case distinction

And obtained the following new goals

• Proof step 14:

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

• Proof step 22:

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

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

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

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 16:

  ⊦ h0 = h1 ↔ (∀ r. (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r]))

• Proof step 17:

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

Rule argument

Additional information

Used terms: ∅, mk(rs, f)

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

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

Rule argument

Additional information

Used simplifier rules: ⊦ r ∈ mk(rs, f) ↔ r ∈ rs; (s) ⊦ ¬ r ∈ ∅; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 19:

  ⊦ h0 = h1 ↔ (∀ r. (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r]__ = h1[r]__))

• Proof step 20:

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

Rule argument

Additional information

Used terms: mk(rs, f, g), ∅

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  # rs ≠ 0, rs ≠ ∅, r ∈ rs, ∀ r. ¬ 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] ⊦ r ∈ mk(rs, f, g) ↔ r ∈ rs; (s) ⊦ ¬ r ∈ ∅; (s)

Proof step 21 from proof lift-emp (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-emp (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  mk(rs, f, g) = ∅ ⊦ mk(rs, f) = ∅ ∧ (r ∈ rs → g(r) = a)

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 24:

  ⊦ h0 = h1 ↔ (∀ r. (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r]__ = h1[r]__))

• Proof step 25:

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

Rule argument

Additional information

Used terms: mk(rs, f, g), ∅

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 26:

  ∀ r0. ¬ r0 ∈ rs ⊦ mk(rs, f) = ∅ ∧ (r ∈ rs → g(r) = a)

Rule argument

Additional information

Used simplifier rules: ⊦ r ∈ mk(rs, f, g) ↔ r ∈ rs; (s) ⊦ ¬ r ∈ ∅; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 27:

  ⊦ h0 = h1 ↔ (∀ r. (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r]))

• Proof step 28:

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

Rule argument

Additional information

Used terms: mk(rs, f), ∅

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 29:

  ∀ r0. ¬ r0 ∈ rs ⊦ ¬ r0 ∈ rs ∧ (r ∈ rs → g(r) = a)

Rule argument

Additional information

Used simplifier rules: ⊦ r ∈ mk(rs, f) ↔ r ∈ rs; (s) ⊦ ¬ r ∈ ∅; (s)

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

User applied rule case distinction

And obtained the following new goals

• Proof step 30:

  r0 ∈ rs, ∀ r0. ¬ r0 ∈ rs ⊦

• Proof step 32:

  g(r) ≠ a, r ∈ rs, ∀ r0. ¬ r0 ∈ rs ⊦

Rule argument

Additional information

Proof step 30 from proof lift-emp (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

  # rs ≠ 0, rs ≠ ∅, r0 ∈ rs, ∀ r0. ¬ r0 ∈ rs ⊦

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 31 from proof lift-emp (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 32 from proof lift-emp (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 33:

  # rs ≠ 0, g(r) ≠ a, rs ≠ ∅, r ∈ rs, ∀ r0. ¬ r0 ∈ rs ⊦

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 33 from proof lift-emp (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: r