Proof step 1 from proof ex-lst-shift (conclusion) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 2:

  (o[_∃ xv] * hR)[rs, cf, af] ⊦ ∃ x. (o[xv(x)] * hR)[rs, cf, af]

• Proof step 23:

  ¬ (o[_∃ xv] * hR)[rs, cf, af], ∃ x. (o[xv(x)] * hR)[rs, cf, af] ⊦

Rule argument

Additional information

Proof step 2 from proof ex-lst-shift (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] ↔ (∃ rs0, rs1. rs0 ∪ rs1 = rs ∧ rs0 ∩ rs1 = ∅ ∧ hR0[rs0, f, g] ∧ hR1[rs1, f, g])

• Proof step 4:

  ∃ rs0, rs1. rs0 ∪ rs1 = rs ∧ rs0 ∩ rs1 = ∅ ∧ o[_∃ xv][rs0, cf, af] ∧ hR[rs1, cf, af] ⊦ ∃ x. (o[xv(x)] * hR)[rs, cf, af]

Rule argument

Additional information

Used terms: cf, rs, hR, af, o[_∃ xv]

Proof step 3 from proof ex-lst-shift (previous step) (back to tree)

A spec-lemma

Proof step 4 from proof ex-lst-shift (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  rs0 ∩ rs1 = ∅, o[_∃ xv][rs0, cf, af], hR[rs1, cf, af] ⊦ ∃ x. (o[xv(x)] * hR)[rs0 ∪ rs1, cf, af]

Rule argument

Additional information

Proof step 5 from proof ex-lst-shift (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:

  rs0 ∩ rs1 = ∅, hR[rs1, cf, af], o[_∃ xv](mk(rs0, cf, af)) ⊦ ∃ x. (o[xv(x)] * hR)[rs0 ∪ rs1, cf, af]

Rule argument

Additional information

Used terms: o[_∃ xv], rs0, cf, af

Proof step 6 from proof ex-lst-shift (previous step) (back to tree)

A spec-lemma

Proof step 7 from proof ex-lst-shift (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 8:

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

• Proof step 9:

  rs0 ∩ rs1 = ∅, hR[rs1, cf, af], (_∃ xv)(mk(rs0, cf)), ∀ r. r ∈ rs0 → af(r) = o ⊦ ∃ x. (o[xv(x)] * hR)[rs0 ∪ rs1, cf, af]

Rule argument

Additional information

Used terms: cf, o, _∃ xv, rs0, af

Proof step 8 from proof ex-lst-shift (previous step) (back to tree)

A spec-lemma

Proof step 9 from proof ex-lst-shift (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  rs0 ∩ rs1 = ∅, hR[rs1, cf, af], (_∃ xv)(mk(rs0, cf)), ∀ r. r ∈ rs0 → af(r) = o ⊦ ∃ x. (o[xv(x)] * hR)[rs0 ∪ rs1, cf, af]

Rule argument

Additional information

Proof step 10 from proof ex-lst-shift (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 11:

  ⊦ (_∃ xv)(mk(rs, cf)) ↔ (∃ x. xv(x)(mk(rs, cf)))

• Proof step 12:

  rs0 ∩ rs1 = ∅, hR[rs1, cf, af], ∀ r. r ∈ rs0 → af(r) = o, ∃ x. xv(x)(mk(rs0, cf)) ⊦ ∃ x. (o[xv(x)] * hR)[rs0 ∪ rs1, cf, af]

Rule argument

Additional information

Used terms: cf, rs0, xv

Proof step 11 from proof ex-lst-shift (previous step) (back to tree)

Lemma ex-lst

Proof step 12 from proof ex-lst-shift (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  rs0 ∩ rs1 = ∅, hR[rs1, cf, af], xv(x)(mk(rs0, cf)), ∀ r. r ∈ rs0 → af(r) = o ⊦ ∃ x. (o[xv(x)] * hR)[rs0 ∪ rs1, cf, af]

Rule argument

Additional information

Proof step 13 from proof ex-lst-shift (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 14:

  rs0 ∩ rs1 = ∅, hR[rs1, cf, af], xv(x)(mk(rs0, cf)), ¬ (o[xv(x)] * hR)[rs0 ∪ rs1, cf, af], ∀ r. r ∈ rs0 → af(r) = o ⊦

Rule argument

Additional information

Used terms: x

Proof step 14 from proof ex-lst-shift (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

  ⊦ hR0[rs0, f, g] ∧ hR1[rs1, f, g] ∧ rs0 ∩ rs1 = ∅ → (hR0 * hR1)[rs0 ∪ rs1, f, g]

• Proof step 16:

  rs0 ∩ rs1 = ∅, hR[rs1, cf, af], xv(x)(mk(rs0, cf)), ¬ (o[xv(x)] * hR)[rs0 ∪ rs1, cf, af], ∀ r. r ∈ rs0 → af(r) = o ⊦ o[xv(x)][rs0, cf, af] ∧ hR[rs1, cf, af] ∧ rs0 ∩ rs1 = ∅

Rule argument

Additional information

Used terms: cf, rs0, hR, af, o[xv(x)], rs1

Proof step 15 from proof ex-lst-shift (previous step) (back to tree)

A spec-lemma

Proof step 16 from proof ex-lst-shift (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  rs0 ∩ rs1 = ∅, hR[rs1, cf, af], xv(x)(mk(rs0, cf)), ¬ (o[xv(x)] * hR)[rs0 ∪ rs1, cf, af], ¬ o[xv(x)][rs0, cf, af], ∀ r. r ∈ rs0 → af(r) = o ⊦

Rule argument

Additional information

Proof step 17 from proof ex-lst-shift (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 18:

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

• Proof step 19:

  rs0 ∩ rs1 = ∅, hR[rs1, cf, af], xv(x)(mk(rs0, cf)), ¬ (o[xv(x)] * hR)[rs0 ∪ rs1, cf, af], ¬ o[xv(x)](mk(rs0, cf, af)), ∀ r. r ∈ rs0 → af(r) = o ⊦

Rule argument

Additional information

Used terms: o[xv(x)], rs0, cf, af

Proof step 18 from proof ex-lst-shift (previous step) (back to tree)

A spec-lemma

Proof step 19 from proof ex-lst-shift (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 20:

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

• Proof step 21:

  rs0 ∩ rs1 = ∅, hR[rs1, cf, af], xv(x)(mk(rs0, cf)), ¬ (o[xv(x)] * hR)[rs0 ∪ rs1, cf, af], ∀ r. r ∈ rs0 → af(r) = o, ¬ xv(x)(mk(rs0, cf)) ∨ (∃ r. ¬(r ∈ rs0 → af(r) = o)) ⊦

Rule argument

Additional information

Used terms: cf, o, xv(x), rs0, af

Proof step 20 from proof ex-lst-shift (previous step) (back to tree)

A spec-lemma

Proof step 21 from proof ex-lst-shift (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  rs0 ∩ rs1 = ∅, af(r) ≠ o, hR[rs1, cf, af], xv(x)(mk(rs0, cf)), r ∈ rs0, ¬ (o[xv(x)] * hR)[rs0 ∪ rs1, cf, af], ∀ r. r ∈ rs0 → af(r) = o ⊦

Rule argument

Additional information

Proof step 22 from proof ex-lst-shift (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 23 from proof ex-lst-shift (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

  (o[xv(x)] * hR)[rs, cf, af], ¬ (o[_∃ xv] * hR)[rs, cf, af] ⊦

Rule argument

Additional information

Proof step 24 from proof ex-lst-shift (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 25:

  ⊦ (hR0 * hR1)[rs, f, g] ↔ (∃ rs0, rs1. rs0 ∪ rs1 = rs ∧ rs0 ∩ rs1 = ∅ ∧ hR0[rs0, f, g] ∧ hR1[rs1, f, g])

• Proof step 26:

  ¬ (o[_∃ xv] * hR)[rs, cf, af], ∃ rs0, rs1. rs0 ∪ rs1 = rs ∧ rs0 ∩ rs1 = ∅ ∧ o[xv(x)][rs0, cf, af] ∧ hR[rs1, cf, af] ⊦

Rule argument

Additional information

Used terms: cf, rs, hR, af, o[xv(x)]

Proof step 25 from proof ex-lst-shift (previous step) (back to tree)

A spec-lemma

Proof step 26 from proof ex-lst-shift (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  rs0 ∩ rs1 = ∅, o[xv(x)][rs0, cf, af], hR[rs1, cf, af], ¬ (o[_∃ xv] * hR)[rs0 ∪ rs1, cf, af] ⊦

Rule argument

Additional information

Proof step 27 from proof ex-lst-shift (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 28:

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

• Proof step 29:

  rs0 ∩ rs1 = ∅, hR[rs1, cf, af], o[xv(x)](mk(rs0, cf, af)), ¬ (o[_∃ xv] * hR)[rs0 ∪ rs1, cf, af] ⊦

Rule argument

Additional information

Used terms: o[xv(x)], rs0, cf, af

Proof step 28 from proof ex-lst-shift (previous step) (back to tree)

A spec-lemma

Proof step 29 from proof ex-lst-shift (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 30:

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

• Proof step 31:

  rs0 ∩ rs1 = ∅, hR[rs1, cf, af], xv(x)(mk(rs0, cf)), ¬ (o[_∃ xv] * hR)[rs0 ∪ rs1, cf, af], ∀ r. r ∈ rs0 → af(r) = o ⊦

Rule argument

Additional information

Used terms: cf, o, xv(x), rs0, af

Proof step 30 from proof ex-lst-shift (previous step) (back to tree)

A spec-lemma

Proof step 31 from proof ex-lst-shift (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 32:

  rs0 ∩ rs1 = ∅, hR[rs1, cf, af], xv(x)(mk(rs0, cf)), ¬ (o[_∃ xv] * hR)[rs0 ∪ rs1, cf, af], ∀ r. r ∈ rs0 → af(r) = o ⊦

Rule argument

Additional information

Proof step 32 from proof ex-lst-shift (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 33:

  ⊦ hR0[rs0, f, g] ∧ hR1[rs1, f, g] ∧ rs0 ∩ rs1 = ∅ → (hR0 * hR1)[rs0 ∪ rs1, f, g]

• Proof step 34:

  rs0 ∩ rs1 = ∅, hR[rs1, cf, af], xv(x)(mk(rs0, cf)), ¬ (o[_∃ xv] * hR)[rs0 ∪ rs1, cf, af], ∀ r. r ∈ rs0 → af(r) = o ⊦ o[_∃ xv][rs0, cf, af] ∧ hR[rs1, cf, af] ∧ rs0 ∩ rs1 = ∅

Rule argument

Additional information

Used terms: cf, rs0, hR, af, o[_∃ xv], rs1

Proof step 33 from proof ex-lst-shift (previous step) (back to tree)

A spec-lemma

Proof step 34 from proof ex-lst-shift (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 35:

  rs0 ∩ rs1 = ∅, hR[rs1, cf, af], xv(x)(mk(rs0, cf)), ¬ (o[_∃ xv] * hR)[rs0 ∪ rs1, cf, af], ¬ o[_∃ xv][rs0, cf, af], ∀ r. r ∈ rs0 → af(r) = o ⊦

Rule argument

Additional information

Proof step 35 from proof ex-lst-shift (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 36:

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

• Proof step 37:

  rs0 ∩ rs1 = ∅, hR[rs1, cf, af], xv(x)(mk(rs0, cf)), ¬ (o[_∃ xv] * hR)[rs0 ∪ rs1, cf, af], ¬ o[_∃ xv](mk(rs0, cf, af)), ∀ r. r ∈ rs0 → af(r) = o ⊦

Rule argument

Additional information

Used terms: o[_∃ xv], rs0, cf, af

Proof step 36 from proof ex-lst-shift (previous step) (back to tree)

A spec-lemma

Proof step 37 from proof ex-lst-shift (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 38:

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

• Proof step 39:

  rs0 ∩ rs1 = ∅, hR[rs1, cf, af], xv(x)(mk(rs0, cf)), ¬ (o[_∃ xv] * hR)[rs0 ∪ rs1, cf, af], ∀ r. r ∈ rs0 → af(r) = o, ¬ (_∃ xv)(mk(rs0, cf)) ∨ (∃ r. ¬(r ∈ rs0 → af(r) = o)) ⊦

Rule argument

Additional information

Used terms: cf, o, _∃ xv, rs0, af

Proof step 38 from proof ex-lst-shift (previous step) (back to tree)

A spec-lemma

Proof step 39 from proof ex-lst-shift (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 40:

  rs0 ∩ rs1 = ∅, hR[rs1, cf, af], xv(x)(mk(rs0, cf)), ¬ (o[_∃ xv] * hR)[rs0 ∪ rs1, cf, af], ∀ r. r ∈ rs0 → af(r) = o, ¬ (_∃ xv)(mk(rs0, cf)) ∨ ¬(r ∈ rs0 → af(r) = o) ⊦

Rule argument

Additional information

Proof step 40 from proof ex-lst-shift (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 41:

  ⊦ (_∃ xv)(mk(rs, cf)) ↔ (∃ x. xv(x)(mk(rs, cf)))

• Proof step 42:

  rs0 ∩ rs1 = ∅, hR[rs1, cf, af], xv(x)(mk(rs0, cf)), ¬ (o[_∃ xv] * hR)[rs0 ∪ rs1, cf, af], ∀ r. r ∈ rs0 → af(r) = o, ¬(∃ x. xv(x)(mk(rs0, cf))) ∨ ¬(r ∈ rs0 → af(r) = o) ⊦

Rule argument

Additional information

Used terms: xv, rs0, cf

Proof step 41 from proof ex-lst-shift (previous step) (back to tree)

Lemma ex-lst

Proof step 42 from proof ex-lst-shift (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 43:

  rs0 ∩ rs1 = ∅, hR[rs1, cf, af], xv(x)(mk(rs0, cf)), ¬ (o[_∃ xv] * hR)[rs0 ∪ rs1, cf, af], ∀ r. r ∈ rs0 → af(r) = o ⊦ ∃ x. xv(x)(mk(rs0, cf))

• Proof step 44:

  rs0 ∩ rs1 = ∅, af(r) ≠ o, hR[rs1, cf, af], xv(x)(mk(rs0, cf)), r ∈ rs0, ¬ (o[_∃ xv] * hR)[rs0 ∪ rs1, cf, af], ∀ r. r ∈ rs0 → af(r) = o ⊦

Rule argument

Additional information

Proof step 43 from proof ex-lst-shift (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: x

Proof step 44 from proof ex-lst-shift (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 45:

  rs0 ∩ rs1 = ∅, # rs0 ≠ 0, af(r) ≠ o, rs0 ≠ ∅, hR[rs1, cf, af], xv(x)(mk(rs0, cf)), r ∈ rs0, ¬ (o[_∃ xv] * hR)[rs0 ∪ rs1, cf, af], ∀ r. r ∈ rs0 → af(r) = o ⊦

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 45 from proof ex-lst-shift (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: r