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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(x \ y ⊆ z ↔ x ⊆ z ∪ y) ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ¬(x \ y ⊆ z ↔ x ⊆ z + y) ⊦

Rule argument

Additional information

Used simplifier rules: union: ⊦ x ∪ y = rmdup(x + y); assoc: ⊦ (x ∪ y) ∪ z = x ∪ y ∪ z; rmdup-01: ⊦ x ⊆ rmdup(y) ↔ x ⊆ y;

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

User applied rule case distinction

And obtained the following new goals

• Proof step 4:

  x \ y ⊆ z, ¬ x ⊆ z + y ⊦

• Proof step 6:

  x ⊆ z + y, ¬ x \ y ⊆ z ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 5:

  ⊦ x ⊆ y ↔ (∀ a. a ∈ x → a ∈ y)

Rule argument

Additional information

Used simplifier rules: sub-notin: ⊦ x ⊆ y ∧ ¬ a ∈ y → ¬ a ∈ x; diff-in: ⊦ a ∈ x \ y ↔ a ∈ x ∧ ¬ a ∈ y; ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) a: ⊦ (x + y) + z = x + y + z; from specification polylist Used terms: z + y, x

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

Lemma subset

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

  ⊦ x ⊆ y ↔ (∀ a. a ∈ x → a ∈ y)

Rule argument

Additional information

Used simplifier rules: diff-in: ⊦ a ∈ x \ y ↔ a ∈ x ∧ ¬ a ∈ y; sub-in: ⊦ x ⊆ y ∧ a ∈ x → a ∈ y; ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) a: ⊦ (x + y) + z = x + y + z; from specification polylist Used terms: z, x \ y

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

Lemma subset