Proof step 1 from proof union-subset (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(spmx1 ∪ spmx2 ⊆ spmx ↔ spmx1 ⊆ spmx ∧ spmx2 ⊆ spmx), disjointp(spmx1, spmx2) ⊦

Rule argument

Additional information

Proof step 2 from proof union-subset (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ¬(spmx1 ⊕ spmx2 ⊆ spmx ↔ spmx1 ⊆ spmx ∧ spmx2 ⊆ spmx), ∀ np. np ∈ spmx1 → ¬ np ∈ spmx2 ⊦

Rule argument

Additional information

Used simplifier rules: union-def: ⊦ sa1 ∪ sa2 = sa1 ⊕ sa2; disjointp-def: ⊦ disjointp(sa1, sa2) ↔ (∀ np. np ∈ sa1 → ¬ np ∈ sa2);

Proof step 3 from proof union-subset (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

  ⊦ st1 ⊆ st2 ↔ (∀ a. a ∈ st1 → a ∈ st2 ∧ st1[a] = st2[a])

• Proof step 5:

  ∀ np. np ∈ spmx1 → ¬ np ∈ spmx2 ⊦ (∀ a. a ∈ spmx1 ⊕ spmx2 → a ∈ spmx ∧ (spmx1 ⊕ spmx2)[a] = spmx[a]) ↔ spmx1 ⊆ spmx ∧ spmx2 ⊆ spmx

Rule argument

Additional information

Used terms: spmx1 ⊕ spmx2, spmx

Proof step 4 from proof union-subset (previous step) (back to tree)

A spec-lemma

Proof step 5 from proof union-subset (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

  ⊦ st1 ⊆ st2 ↔ (∀ a. a ∈ st1 → a ∈ st2 ∧ st1[a] = st2[a])

• Proof step 7:

  ∀ np. np ∈ spmx1 → ¬ np ∈ spmx2 ⊦ (∀ a. a ∈ spmx1 ⊕ spmx2 → a ∈ spmx ∧ (spmx1 ⊕ spmx2)[a] = spmx[a]) ↔ (∀ a. a ∈ spmx1 → a ∈ spmx ∧ spmx1[a] = spmx[a]) ∧ spmx2 ⊆ spmx

Rule argument

Additional information

Used terms: spmx1, spmx

Proof step 6 from proof union-subset (previous step) (back to tree)

A spec-lemma

Proof step 7 from proof union-subset (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 8:

  ⊦ st1 ⊆ st2 ↔ (∀ a. a ∈ st1 → a ∈ st2 ∧ st1[a] = st2[a])

• Proof step 9:

  ∀ np. np ∈ spmx1 → ¬ np ∈ spmx2 ⊦ (∀ a. a ∈ spmx1 ⊕ spmx2 → a ∈ spmx ∧ (spmx1 ⊕ spmx2)[a] = spmx[a]) ↔ (∀ a. a ∈ spmx1 → a ∈ spmx ∧ spmx1[a] = spmx[a]) ∧ (∀ a. a ∈ spmx2 → a ∈ spmx ∧ spmx2[a] = spmx[a])

Rule argument

Additional information

Used terms: spmx2, spmx

Proof step 8 from proof union-subset (previous step) (back to tree)

A spec-lemma

Proof step 9 from proof union-subset (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 10:

  ∀ np. np ∈ spmx1 → ¬ np ∈ spmx2, ∀ a. a ∈ spmx1 ⊕ spmx2 → a ∈ spmx ∧ (spmx1 ⊕ spmx2)[a] = spmx[a] ⊦ (∀ a. a ∈ spmx1 → a ∈ spmx ∧ spmx1[a] = spmx[a]) ∧ (∀ a. a ∈ spmx2 → a ∈ spmx ∧ spmx2[a] = spmx[a])

• Proof step 21:

  ∀ np. np ∈ spmx1 → ¬ np ∈ spmx2, ∀ a. a ∈ spmx1 → a ∈ spmx ∧ spmx1[a] = spmx[a], ∀ a. a ∈ spmx2 → a ∈ spmx ∧ spmx2[a] = spmx[a] ⊦ ∀ a. a ∈ spmx1 ⊕ spmx2 → a ∈ spmx ∧ (spmx1 ⊕ spmx2)[a] = spmx[a]

Rule argument

Additional information

Proof step 10 from proof union-subset (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  ∀ a. a ∈ spmx1 ⊕ spmx2 → a ∈ spmx ∧ (spmx1 ⊕ spmx2)[a] = spmx[a], ∀ np. np ∈ spmx1 → ¬ np ∈ spmx2 ⊦ (np ∈ spmx1 → np ∈ spmx ∧ spmx1[np] = spmx[np]) ∧ (np0 ∈ spmx2 → np0 ∈ spmx ∧ spmx2[np0] = spmx[np0])

Rule argument

Additional information

Proof step 11 from proof union-subset (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 12:

  np ∈ spmx1, ∀ np. np ∈ spmx1 → ¬ np ∈ spmx2, ∀ a. a ∈ spmx1 ⊕ spmx2 → a ∈ spmx ∧ (spmx1 ⊕ spmx2)[a] = spmx[a] ⊦ np ∈ spmx ∧ spmx1[np] = spmx[np]

• Proof step 13:

  np0 ∈ spmx2, ∀ np. np ∈ spmx1 → ¬ np ∈ spmx2, ∀ a. a ∈ spmx1 ⊕ spmx2 → a ∈ spmx ∧ (spmx1 ⊕ spmx2)[a] = spmx[a] ⊦ np0 ∈ spmx ∧ spmx2[np0] = spmx[np0]

Rule argument

Additional information

Proof step 12 from proof union-subset (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ a ∈ st0 → (st0 ⊕ st1)[a] = st0[a]; (s) ⊦ a ∈ st0 ⊕ st1 ↔ a ∈ st0 ∨ a ∈ st1; (ws) Used terms: np

Proof step 13 from proof union-subset (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 14:

  np0 ∈ spmx2, np0 ∈ spmx1 ⊕ spmx2 → np0 ∈ spmx ∧ (spmx1 ⊕ spmx2)[np0] = spmx[np0], ∀ np. np ∈ spmx1 → ¬ np ∈ spmx2 ⊦ np0 ∈ spmx ∧ spmx2[np0] = spmx[np0]

Rule argument

Additional information

Used terms: np0

Proof step 14 from proof union-subset (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  (spmx1 ⊕ spmx2)[np0] = spmx[np0], spmx2[np0] ≠ spmx[np0], np0 ∈ spmx2, np0 ∈ spmx1 ⊕ spmx2, np0 ∈ spmx, ∀ np. np ∈ spmx1 → ¬ np ∈ spmx2 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a ∈ st0 ⊕ st1 ↔ a ∈ st0 ∨ a ∈ st1; (ws)

Proof step 15 from proof union-subset (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 16:

  ⊦ a ∈ st0 → (st0 ⊕ st1)[a] = st0[a]

• Proof step 17:

  spmx1[np0] = spmx[np0], spmx2[np0] ≠ spmx[np0], np0 ∈ spmx, np0 ∈ spmx1 ⊕ spmx2, np0 ∈ spmx2, np0 ∈ spmx1, ∀ np. np ∈ spmx1 → ¬ np ∈ spmx2 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ a ∈ st0 ∧ a ∈ st1 → (st0 ⊕ st1)[a] = st1[a]; (s) Used terms: spmx1, spmx2, np0

Proof step 16 from proof union-subset (previous step) (back to tree)

A spec-lemma

Proof step 17 from proof union-subset (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 18:

  ⊦ a ∈ st0 ⊕ st1 ↔ a ∈ st0 ∨ a ∈ st1

• Proof step 19:

  spmx1[np0] = spmx[np0], spmx2[np0] ≠ spmx[np0], np0 ∈ spmx1, np0 ∈ spmx2, np0 ∈ spmx, ∀ np. np ∈ spmx1 → ¬ np ∈ spmx2, np0 ∈ spmx1 ∨ np0 ∈ spmx2 ⊦

Rule argument

Additional information

Used terms: np0, spmx1, spmx2

Proof step 18 from proof union-subset (previous step) (back to tree)

A spec-lemma

Proof step 19 from proof union-subset (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  spmx1[np0] = spmx[np0], spmx2[np0] ≠ spmx[np0], np0 ∈ spmx, np0 ∈ spmx2, np0 ∈ spmx1, ∀ np. np ∈ spmx1 → ¬ np ∈ spmx2 ⊦

Rule argument

Additional information

Proof step 20 from proof union-subset (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: np0

Proof step 21 from proof union-subset (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  np ∈ spmx1 ⊕ spmx2, ∀ a. a ∈ spmx2 → a ∈ spmx ∧ spmx2[a] = spmx[a], ∀ a. a ∈ spmx1 → a ∈ spmx ∧ spmx1[a] = spmx[a], ∀ np. np ∈ spmx1 → ¬ np ∈ spmx2 ⊦ np ∈ spmx ∧ (spmx1 ⊕ spmx2)[np] = spmx[np]

Rule argument

Additional information

Proof step 22 from proof union-subset (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 23:

  np ∈ spmx1 ⊕ spmx2, np ∈ spmx2 → np ∈ spmx ∧ spmx2[np] = spmx[np], ∀ np. np ∈ spmx1 → ¬ np ∈ spmx2, ∀ a. a ∈ spmx1 → a ∈ spmx ∧ spmx1[a] = spmx[a] ⊦ np ∈ spmx ∧ (spmx1 ⊕ spmx2)[np] = spmx[np]

Rule argument

Additional information

Used terms: np

Proof step 23 from proof union-subset (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 24:

  np ∈ spmx1 ⊕ spmx2, np ∈ spmx2 → np ∈ spmx ∧ spmx2[np] = spmx[np], np ∈ spmx1 → np ∈ spmx ∧ spmx1[np] = spmx[np], ∀ np. np ∈ spmx1 → ¬ np ∈ spmx2 ⊦ np ∈ spmx ∧ (spmx1 ⊕ spmx2)[np] = spmx[np]

Rule argument

Additional information

Used terms: np

Proof step 24 from proof union-subset (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 25:

  ⊦ a ∈ st0 ⊕ st1 ↔ a ∈ st0 ∨ a ∈ st1

• Proof step 26:

  np ∈ spmx1 → np ∈ spmx ∧ spmx1[np] = spmx[np], np ∈ spmx2 → np ∈ spmx ∧ spmx2[np] = spmx[np], ∀ np. np ∈ spmx1 → ¬ np ∈ spmx2, np ∈ spmx1 ∨ np ∈ spmx2 ⊦ np ∈ spmx ∧ (spmx1 ⊕ spmx2)[np] = spmx[np]

Rule argument

Additional information

Used terms: np, spmx1, spmx2

Proof step 25 from proof union-subset (previous step) (back to tree)

A spec-lemma

Proof step 26 from proof union-subset (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 27:

  ⊦ a ∈ st0 → (st0 ⊕ st1)[a] = st0[a]

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ a ∈ st0 ∧ a ∈ st1 → (st0 ⊕ st1)[a] = st1[a]; (s) Used terms: spmx1, spmx2, np

Proof step 27 from proof union-subset (previous step) (back to tree)

A spec-lemma