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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬ s ⊆ s ++ a ++ a0 ++ a1 ++ b ++ c ⊦

Rule argument

Additional information

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

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 3:

  c ∈ s ++ a ++ a0 ++ a1 ++ b, ¬ s ⊆ s ++ a ++ a0 ++ a1 ++ b ++ c ⊦

Rule argument

Additional information

Used simplifier rules: In-insert: ⊦ a ∈ s ++ b ↔ a = b ∨ a ∈ s; sub-insert: ⊦ ¬ a ∈ s → (s ⊆ s0 ++ a ↔ s ⊆ s0); subset-insert-01: ⊦ s ⊆ s ++ a ++ a0 ++ b ++ c; Used formulas: c ∈ s ++ a ++ a0 ++ a1 ++ b

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  c ≠ a0, c ≠ a1, c ≠ b, c ∈ s, ¬ s ⊆ s ++ a ++ a0 ++ a1 ++ b ++ c ⊦

Rule argument

Additional information

Used simplifier rules: In-insert: ⊦ a ∈ s ++ b ↔ a = b ∨ a ∈ s; add-01: ⊦ s ++ a ++ a = s ++ a; addtwo: ⊦ s ++ a ++ b ++ a = s ++ b ++ a; addthree: ⊦ s ++ a ++ b ++ c ++ a = s ++ a ++ b ++ c; sub-insert: ⊦ ¬ a ∈ s → (s ⊆ s0 ++ a ↔ s ⊆ s0); subset-insert-01: ⊦ s ⊆ s ++ a ++ a0 ++ b ++ c; ne-01: ⊦ a ∈ s → s ≠ ∅; ne-02: ⊦ a ∈ s → (s = ∅ ↔ false);

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

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 5:

  c ≠ a0, c ≠ a1, c ≠ b, c ∈ s, ¬ a ∈ s, ¬ s ⊆ s ++ a ++ a0 ++ a1 ++ b ++ c ⊦

Rule argument

Additional information

Used simplifier rules: eq: ⊦ a ∈ s → s ++ a = s; subset-insert-01: ⊦ s ⊆ s ++ a ++ a0 ++ b ++ c; Used formulas: a ∈ s

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

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 6:

  c ≠ a0, c ≠ a1, c ≠ b, c ∈ s, ¬ a0 ∈ s ++ a, ¬ a ∈ s, ¬ s ⊆ s ++ a ++ a0 ++ a1 ++ b ++ c ⊦

Rule argument

Additional information

Used simplifier rules: In-insert: ⊦ a ∈ s ++ b ↔ a = b ∨ a ∈ s; add-01: ⊦ s ++ a ++ a = s ++ a; ins-two: ⊦ a ∈ s → s ++ b ++ a = s ++ b; subset-insert-01: ⊦ s ⊆ s ++ a ++ a0 ++ b ++ c; Used formulas: a0 ∈ s ++ a

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  a0 ≠ a, c ≠ a0, c ≠ a1, c ≠ b, c ∈ s, ¬ a ∈ s, ¬ a0 ∈ s, ¬ s ⊆ s ++ a ++ a0 ++ a1 ++ b ++ c ⊦

Rule argument

Additional information

Used simplifier rules: In-insert: ⊦ a ∈ s ++ b ↔ a = b ∨ a ∈ s;

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

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 8:

  a0 ≠ a, c ≠ a0, c ≠ a1, c ≠ b, c ∈ s, a1 ∈ s ++ a ++ a0, ¬ a ∈ s, ¬ a0 ∈ s, ¬ s ⊆ s ++ a ++ a0 ++ a1 ++ b ++ c ⊦

• Proof step 16:

  a0 ≠ a, c ≠ a0, c ≠ a1, c ≠ b, c ∈ s, ¬ a1 ∈ s ++ a ++ a0, ¬ a ∈ s, ¬ a0 ∈ s, ¬ s ⊆ s ++ a ++ a0 ++ a1 ++ b ++ c ⊦

Rule argument

Additional information

Used formulas: a1 ∈ s ++ a ++ a0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  a0 ≠ a, a1 ≠ a0, a1 ≠ a, c ≠ b, c ≠ a1, c ≠ a0, c ∈ s, a1 ∈ s, ¬ a0 ∈ s, ¬ a ∈ s, ¬ s ⊆ s ++ a ++ a0 ++ a1 ++ b ++ c ⊦

Rule argument

Additional information

Used simplifier rules: In-insert: ⊦ a ∈ s ++ b ↔ a = b ∨ a ∈ s; add-01: ⊦ s ++ a ++ a = s ++ a; addtwo: ⊦ s ++ a ++ b ++ a = s ++ b ++ a; subset-insert-01: ⊦ s ⊆ s ++ a ++ a0 ++ b ++ c;

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

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 10:

  a0 ≠ a, a1 ≠ a0, a1 ≠ a, c ≠ b, c ≠ a1, c ≠ a0, a1 ∈ s, c ∈ s, b ∈ s ++ a ++ a0 ++ a1, ¬ a0 ∈ s, ¬ a ∈ s, ¬ s ⊆ s ++ a ++ a0 ++ a1 ++ b ++ c ⊦

• Proof step 13:

  a0 ≠ a, a1 ≠ a0, a1 ≠ a, c ≠ b, c ≠ a1, c ≠ a0, a1 ∈ s, c ∈ s, ¬ b ∈ s ++ a ++ a0 ++ a1, ¬ a0 ∈ s, ¬ a ∈ s, ¬ s ⊆ s ++ a ++ a0 ++ a1 ++ b ++ c ⊦

Rule argument

Additional information

Used formulas: b ∈ s ++ a ++ a0 ++ a1

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  a0 ≠ a, a1 ≠ a, a1 ≠ a0, b ≠ a0, b ≠ a, c ≠ a0, c ≠ a1, c ≠ b, a1 ∈ s, c ∈ s, b ∈ s, ¬ a ∈ s, ¬ a0 ∈ s, ¬ s ⊆ s ++ a ++ a0 ++ a1 ++ b ++ c ⊦

Rule argument

Additional information

Used simplifier rules: In-insert: ⊦ a ∈ s ++ b ↔ a = b ∨ a ∈ s; addtwo: ⊦ s ++ a ++ b ++ a = s ++ b ++ a; ins-two: ⊦ a ∈ s → s ++ b ++ a = s ++ b; subset-insert: ⊦ s ⊆ s ++ a ++ b ++ c; addthree: ⊦ s ++ a ++ b ++ c ++ a = s ++ a ++ b ++ c; subset-insert-01: ⊦ s ⊆ s ++ a ++ a0 ++ b ++ c;

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

  ⊦ s1 ⊆ s2 ↔ (∀ a. a ∈ s1 → a ∈ s2)

Rule argument

Additional information

Used simplifier rules: In-insert: ⊦ a ∈ s ++ b ↔ a = b ∨ a ∈ s; Used terms: s ++ a ++ a0 ++ a1 ++ b ++ c, s

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

Lemma Subset

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  a0 ≠ a, a1 ≠ a0, a1 ≠ a, b ≠ a1, b ≠ a0, b ≠ a, c ≠ b, c ≠ a1, c ≠ a0, c ∈ s, a1 ∈ s, ¬ a0 ∈ s, ¬ a ∈ s, ¬ b ∈ s, ¬ s ⊆ s ++ a ++ a0 ++ a1 ++ b ++ c ⊦

Rule argument

Additional information

Used simplifier rules: In-insert: ⊦ a ∈ s ++ b ↔ a = b ∨ a ∈ s;

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

  ⊦ s1 ⊆ s2 ↔ (∀ a. a ∈ s1 → a ∈ s2)

Rule argument

Additional information

Used simplifier rules: In-insert: ⊦ a ∈ s ++ b ↔ a = b ∨ a ∈ s; Used terms: s ++ a ++ a0 ++ a1 ++ b ++ c, s

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

Lemma Subset

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  a0 ≠ a, a1 ≠ a0, a1 ≠ a, c ≠ a0, c ≠ a1, c ≠ b, c ∈ s, ¬ a ∈ s, ¬ a0 ∈ s, ¬ a1 ∈ s, ¬ s ⊆ s ++ a ++ a0 ++ a1 ++ b ++ c ⊦

Rule argument

Additional information

Used simplifier rules: In-insert: ⊦ a ∈ s ++ b ↔ a = b ∨ a ∈ s;

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

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 18:

  a0 ≠ a, a1 ≠ a0, a1 ≠ a, c ≠ a0, c ≠ a1, c ≠ b, c ∈ s, b ∈ s ++ a ++ a0 ++ a1, ¬ a ∈ s, ¬ a0 ∈ s, ¬ a1 ∈ s, ¬ s ⊆ s ++ a ++ a0 ++ a1 ++ b ++ c ⊦

• Proof step 21:

  a0 ≠ a, a1 ≠ a0, a1 ≠ a, c ≠ a0, c ≠ a1, c ≠ b, c ∈ s, ¬ b ∈ s ++ a ++ a0 ++ a1, ¬ a ∈ s, ¬ a0 ∈ s, ¬ a1 ∈ s, ¬ s ⊆ s ++ a ++ a0 ++ a1 ++ b ++ c ⊦

Rule argument

Additional information

Used formulas: b ∈ s ++ a ++ a0 ++ a1

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  a0 ≠ a, a1 ≠ a, a1 ≠ a0, b ≠ a1, b ≠ a0, b ≠ a, c ≠ b, c ≠ a1, c ≠ a0, c ∈ s, b ∈ s, ¬ a1 ∈ s, ¬ a0 ∈ s, ¬ a ∈ s, ¬ s ⊆ s ++ a ++ a0 ++ a1 ++ b ++ c ⊦

Rule argument

Additional information

Used simplifier rules: In-insert: ⊦ a ∈ s ++ b ↔ a = b ∨ a ∈ s; add-01: ⊦ s ++ a ++ a = s ++ a; addtwo: ⊦ s ++ a ++ b ++ a = s ++ b ++ a; addthree: ⊦ s ++ a ++ b ++ c ++ a = s ++ a ++ b ++ c; subset-insert-01: ⊦ s ⊆ s ++ a ++ a0 ++ b ++ c;

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 20:

  ⊦ s1 ⊆ s2 ↔ (∀ a. a ∈ s1 → a ∈ s2)

Rule argument

Additional information

Used simplifier rules: In-insert: ⊦ a ∈ s ++ b ↔ a = b ∨ a ∈ s; Used terms: s ++ a ++ a0 ++ a1 ++ b ++ c, s

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

Lemma Subset

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  a0 ≠ a, a1 ≠ a0, a1 ≠ a, b ≠ a1, b ≠ a0, b ≠ a, c ≠ a0, c ≠ a1, c ≠ b, c ∈ s, ¬ a ∈ s, ¬ a0 ∈ s, ¬ a1 ∈ s, ¬ b ∈ s, ¬ s ⊆ s ++ a ++ a0 ++ a1 ++ b ++ c ⊦

Rule argument

Additional information

Used simplifier rules: In-insert: ⊦ a ∈ s ++ b ↔ a = b ∨ a ∈ s;

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 23:

  ⊦ s1 ⊆ s2 ↔ (∀ a. a ∈ s1 → a ∈ s2)

Rule argument

Additional information

Used simplifier rules: In-insert: ⊦ a ∈ s ++ b ↔ a = b ∨ a ∈ s; Used terms: s ++ a ++ a0 ++ a1 ++ b ++ c, s

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

Lemma Subset