Proof step 1 from proof size-two (conclusion) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 2:

  ⊦ # s = 2 ↔ (∃ a, b. a ≠ b ∧ s = ∅ ++ a ++ b)

Rule argument

Additional information

Proof step 2 from proof size-two (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 3:

  ⊦ # s ≠ 0 → (∃ a. a ∈ s)

• Proof step 4:

  # s ≠ 0 → (∃ a. a ∈ s) ⊦ # s = 2 ↔ (∃ a, b. a ≠ b ∧ s = ∅ ++ a ++ b)

Rule argument

Additional information

Used terms: s

Proof step 3 from proof size-two (previous step) (back to tree)

Lemma selsize

Proof step 4 from proof size-two (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  # s ≠ 0 → a ∈ s ⊦ # s = 2 ↔ (∃ a, b. a ≠ b ∧ s = ∅ ++ a ++ b)

Rule argument

Additional information

Proof step 5 from proof size-two (previous step) (back to tree)

Heuristic cut applied rule cut formula

And obtained the following new goals

• Proof step 6:

  a ∈ s, # s ≠ 0 → a ∈ s ⊦ # s = 2 ↔ (∃ a, b. a ≠ b ∧ s = ∅ ++ a ++ b)

Rule argument

Additional information

Used simplifier rules: size-zero-02: ⊦ # s = 0 → s = ∅; Size-empty: ⊦ # ∅ = 0; ne: ⊦ ∅ ≠ s ++ a; Used formulas: a ∈ s

Proof step 6 from proof size-two (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  a ∈ s ⊦ # s = 2 ↔ (∃ a, b. a ≠ b ∧ s = ∅ ++ a ++ b)

Rule argument

Additional information

Used simplifier rules: ne-01: ⊦ a ∈ s → s ≠ ∅; ne-02: ⊦ a ∈ s → (s = ∅ ↔ false);

Proof step 7 from proof size-two (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 8:

  ⊦ a ∈ s ↔ (∃ s0. s = s0 ++ a ∧ ¬ a ∈ s0)

• Proof step 9:

  ∃ s0. s = s0 ++ a ∧ ¬ a ∈ s0 ⊦ # s = 2 ↔ (∃ a, b. a ≠ b ∧ s = ∅ ++ a ++ b)

Rule argument

Additional information

Used terms: s, a

Proof step 8 from proof size-two (previous step) (back to tree)

Lemma indef

Proof step 9 from proof size-two (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  ¬ a ∈ s0 ⊦ 1 = # s0 ↔ (∃ a0, b. a0 ≠ b ∧ s0 ++ a = ∅ ++ a0 ++ b)

Rule argument

Additional information

Used simplifier rules: Size-insert: ⊦ ¬ a ∈ s → #(s ++ a) = # s + 1; c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic n0 < n ⊦ (* n) = m0 + (* n0) ↔ n - n0 = m0; (s)

Proof step 10 from proof size-two (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 11:

  1 = # s0, ¬ a ∈ s0 ⊦ ∃ a0, b. a0 ≠ b ∧ s0 ++ a = ∅ ++ a0 ++ b

• Proof step 15:

  1 ≠ # s0, ¬ a ∈ s0, ∃ a0, b. a0 ≠ b ∧ s0 ++ a = ∅ ++ a0 ++ b ⊦

Rule argument

Additional information

Proof step 11 from proof size-two (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 12:

  ⊦ # s = 1 → (∃ a. s = ∅ ++ a)

• Proof step 13:

  1 = # s0, ¬ a ∈ s0, # s0 = 1 → (∃ a. s0 = ∅ ++ a) ⊦ ∃ a0, b. a0 ≠ b ∧ s0 ++ a = ∅ ++ a0 ++ b

Rule argument

Additional information

Used terms: s0

Proof step 12 from proof size-two (previous step) (back to tree)

Lemma size-one

Proof step 13 from proof size-two (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  a ≠ a0 ⊦ ∃ a1, b. a1 ≠ b ∧ ∅ ++ a0 ++ a = ∅ ++ a1 ++ b

Rule argument

Additional information

Used simplifier rules: size-one-01: ⊦ #(∅ ++ a) = 1; in-04: ⊦ a ∈ ∅ ++ b ↔ a = b;

Proof step 14 from proof size-two (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: a0, a

Proof step 15 from proof size-two (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  s0 ++ a = ∅ ++ a0 ++ a1, 1 ≠ # s0, a0 ≠ a1, ¬ a ∈ s0 ⊦

Rule argument

Additional information

Proof step 16 from proof size-two (previous step) (back to tree)

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 17:

  s0 ++ a = ∅ ++ a0 ++ a1, 1 ≠ # s0, a0 ≠ a1, ¬ a0 ∈ ∅, ¬ a ∈ s0 ⊦

Rule argument

Additional information

Used simplifier rules: eq: ⊦ a ∈ s → s ++ a = s; eq-02: ⊦ ¬ a ∈ s → (s ++ a = ∅ ++ b ↔ a = b ∧ s = ∅); In-empty: ⊦ ¬ a ∈ ∅; Used formulas: a0 ∈ ∅

Proof step 17 from proof size-two (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  s0 ++ a = ∅ ++ a0 ++ a1, 1 ≠ # s0, a0 ≠ a1, ¬ a ∈ s0 ⊦

Rule argument

Additional information

Used simplifier rules: In-empty: ⊦ ¬ a ∈ ∅;

Proof step 18 from proof size-two (previous step) (back to tree)

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 19:

  s0 ++ a = ∅ ++ a0 ++ a1, 1 ≠ # s0, a0 ≠ a1, ¬ a1 ∈ ∅ ++ a0, ¬ a ∈ s0 ⊦

Rule argument

Additional information

Used simplifier rules: eq: ⊦ a ∈ s → s ++ a = s; eq-02: ⊦ ¬ a ∈ s → (s ++ a = ∅ ++ b ↔ a = b ∧ s = ∅); in-04: ⊦ a ∈ ∅ ++ b ↔ a = b; Used formulas: a1 ∈ ∅ ++ a0

Proof step 19 from proof size-two (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  s0 ++ a = ∅ ++ a0 ++ a1, 1 ≠ # s0, a0 ≠ a1, ¬ a ∈ s0 ⊦

Rule argument

Additional information

Used simplifier rules: in-04: ⊦ a ∈ ∅ ++ b ↔ a = b;

Proof step 20 from proof size-two (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 21:

  ⊦ # s = 1 ↔ (∃ a. s = ∅ ++ a)

• Proof step 22:

  s0 ++ a = ∅ ++ a0 ++ a1, 1 ≠ # s0, a0 ≠ a1, ¬ a ∈ s0, # s0 = 1 ↔ (∃ a. s0 = ∅ ++ a) ⊦

Rule argument

Additional information

Used terms: s0

Proof step 21 from proof size-two (previous step) (back to tree)

Lemma size-one-03

Proof step 22 from proof size-two (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  s0 ++ a = ∅ ++ a0 ++ a1, 1 ≠ # s0, a0 ≠ a1, ¬ a ∈ s0 ⊦ ∃ a. s0 = ∅ ++ a

Rule argument

Additional information

Proof step 23 from proof size-two (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 24:

  s0 ++ a = ∅ ++ a0 ++ a1, 1 ≠ # s0, a0 ≠ a1, s0 ≠ ∅ ++ a1, ¬ a ∈ s0 ⊦ ∃ a. s0 = ∅ ++ a

Rule argument

Additional information

Used terms: a1

Proof step 24 from proof size-two (previous step) (back to tree)

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 25:

  s0 ++ a = ∅ ++ a0 ++ a1, 1 ≠ # s0, a0 ≠ a1, s0 ≠ ∅ ++ a1, ¬ a1 ∈ ∅, ¬ a ∈ s0 ⊦ ∃ a. s0 = ∅ ++ a

Rule argument

Additional information

Used simplifier rules: eq: ⊦ a ∈ s → s ++ a = s; In-empty: ⊦ ¬ a ∈ ∅; Used formulas: a1 ∈ ∅

Proof step 25 from proof size-two (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 26:

  s0 ++ a = ∅ ++ a0 ++ a1, 1 ≠ # s0, a0 ≠ a1, s0 ≠ ∅ ++ a1, ¬ a ∈ s0 ⊦ ∃ a. s0 = ∅ ++ a

Rule argument

Additional information

Used simplifier rules: In-empty: ⊦ ¬ a ∈ ∅;

Proof step 26 from proof size-two (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 27:

  s0 ++ a = ∅ ++ a0 ++ a1, 1 ≠ # s0, a0 ≠ a1, s0 ≠ ∅ ++ a0, s0 ≠ ∅ ++ a1, ¬ a ∈ s0 ⊦ ∃ a. s0 = ∅ ++ a

Rule argument

Additional information

Used terms: a0

Proof step 27 from proof size-two (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 28:

  ⊦ s1 = s2 ↔ (∀ a. a ∈ s1 ↔ a ∈ s2)

• Proof step 29:

  1 ≠ # s0, a0 ≠ a1, s0 ≠ ∅ ++ a0, s0 ≠ ∅ ++ a1, ¬ a ∈ s0, ∀ a2. a2 ∈ s0 ++ a ↔ a2 ∈ ∅ ++ a0 ++ a1 ⊦ ∃ a. s0 = ∅ ++ a

Rule argument

Additional information

Used terms: ∅ ++ a0 ++ a1, s0 ++ a

Proof step 28 from proof size-two (previous step) (back to tree)

Lemma Extension

Proof step 29 from proof size-two (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 30:

  1 ≠ # s0, a0 ≠ a1, s0 ≠ ∅ ++ a0, s0 ≠ ∅ ++ a1, ¬ a ∈ s0, ∀ a2. a2 = a ∨ a2 ∈ s0 ↔ a2 = a1 ∨ a2 = a0 ⊦ ∃ a. s0 = ∅ ++ a

Rule argument

Additional information

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

Proof step 30 from proof size-two (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 31:

  a0 = a ∨ a0 ∈ s0 ↔ a0 = a1 ∨ a0 = a0, 1 ≠ # s0, a0 ≠ a1, s0 ≠ ∅ ++ a0, s0 ≠ ∅ ++ a1, ¬ a ∈ s0, ∀ a2. a2 = a ∨ a2 ∈ s0 ↔ a2 = a1 ∨ a2 = a0 ⊦ ∃ a. s0 = ∅ ++ a

Rule argument

Additional information

Used terms: a0

Proof step 31 from proof size-two (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 32:

  1 ≠ # s0, a0 ≠ a1, s0 ≠ ∅ ++ a0, s0 ≠ ∅ ++ a1, ¬ a ∈ s0, ∀ a2. a2 = a ∨ a2 ∈ s0 ↔ a2 = a1 ∨ a2 = a0, a0 = a ∨ a0 ∈ s0 ⊦ ∃ a. s0 = ∅ ++ a

Rule argument

Additional information

Proof step 32 from proof size-two (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 33:

  a1 = a ∨ a1 ∈ s0 ↔ a1 = a1 ∨ a1 = a0, 1 ≠ # s0, a0 ≠ a1, s0 ≠ ∅ ++ a0, s0 ≠ ∅ ++ a1, ¬ a ∈ s0, ∀ a2. a2 = a ∨ a2 ∈ s0 ↔ a2 = a1 ∨ a2 = a0, a0 = a ∨ a0 ∈ s0 ⊦ ∃ a. s0 = ∅ ++ a

Rule argument

Additional information

Used terms: a1

Proof step 33 from proof size-two (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 34:

  1 ≠ # s0, a0 ≠ a1, s0 ≠ ∅ ++ a0, s0 ≠ ∅ ++ a1, ¬ a ∈ s0, ∀ a2. a2 = a ∨ a2 ∈ s0 ↔ a2 = a1 ∨ a2 = a0, a0 = a ∨ a0 ∈ s0, a1 = a ∨ a1 ∈ s0 ⊦ ∃ a. s0 = ∅ ++ a

Rule argument

Additional information

Proof step 34 from proof size-two (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 35:

  ⊦ s1 = s2 ↔ (∀ a. a ∈ s1 ↔ a ∈ s2)

• Proof step 36:

  1 ≠ # s0, a0 ≠ a1, s0 ≠ ∅ ++ a0, ¬ a ∈ s0, ∀ a2. a2 = a ∨ a2 ∈ s0 ↔ a2 = a1 ∨ a2 = a0, ∃ a. ¬(a ∈ s0 ↔ a ∈ ∅ ++ a1), a1 = a ∨ a1 ∈ s0, a0 = a ∨ a0 ∈ s0 ⊦ ∃ a. s0 = ∅ ++ a

Rule argument

Additional information

Used terms: ∅ ++ a1, s0

Proof step 35 from proof size-two (previous step) (back to tree)

Lemma Extension

Proof step 36 from proof size-two (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 37:

  ¬(a2 ∈ s0 ↔ a2 = a1), 1 ≠ # s0, a0 ≠ a1, s0 ≠ ∅ ++ a0, ¬ a ∈ s0, ∀ a2. a2 = a ∨ a2 ∈ s0 ↔ a2 = a1 ∨ a2 = a0, a0 = a ∨ a0 ∈ s0, a1 = a ∨ a1 ∈ s0 ⊦ ∃ a. s0 = ∅ ++ a

Rule argument

Additional information

Used simplifier rules: in-04: ⊦ a ∈ ∅ ++ b ↔ a = b;

Proof step 37 from proof size-two (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 38:

  ⊦ s1 = s2 ↔ (∀ a. a ∈ s1 ↔ a ∈ s2)

• Proof step 39:

  ¬(a2 ∈ s0 ↔ a2 = a1), 1 ≠ # s0, a0 ≠ a1, ¬ a ∈ s0, ∀ a2. a2 = a ∨ a2 ∈ s0 ↔ a2 = a1 ∨ a2 = a0, ∃ a. ¬(a ∈ s0 ↔ a ∈ ∅ ++ a0), a1 = a ∨ a1 ∈ s0, a0 = a ∨ a0 ∈ s0 ⊦ ∃ a. s0 = ∅ ++ a

Rule argument

Additional information

Used terms: ∅ ++ a0, s0

Proof step 38 from proof size-two (previous step) (back to tree)

Lemma Extension

Proof step 39 from proof size-two (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 40:

  ¬(a2 ∈ s0 ↔ a2 = a1), ¬(a3 ∈ s0 ↔ a3 = a0), 1 ≠ # s0, a0 ≠ a1, ¬ a ∈ s0, ∀ a2. a2 = a ∨ a2 ∈ s0 ↔ a2 = a1 ∨ a2 = a0, a0 = a ∨ a0 ∈ s0, a1 = a ∨ a1 ∈ s0 ⊦ ∃ a. s0 = ∅ ++ a

Rule argument

Additional information

Used simplifier rules: in-04: ⊦ a ∈ ∅ ++ b ↔ a = b;

Proof step 40 from proof size-two (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 41:

  a2 = a ∨ a2 ∈ s0 ↔ a2 = a1 ∨ a2 = a0, ¬(a2 ∈ s0 ↔ a2 = a1), ¬(a3 ∈ s0 ↔ a3 = a0), 1 ≠ # s0, a0 ≠ a1, ¬ a ∈ s0, ∀ a2. a2 = a ∨ a2 ∈ s0 ↔ a2 = a1 ∨ a2 = a0, a1 = a ∨ a1 ∈ s0, a0 = a ∨ a0 ∈ s0 ⊦ ∃ a. s0 = ∅ ++ a

Rule argument

Additional information

Used terms: a2

Proof step 41 from proof size-two (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 42:

  a2 = a ∨ a2 ∈ s0 ↔ a2 = a1 ∨ a2 = a0, a3 = a ∨ a3 ∈ s0 ↔ a3 = a1 ∨ a3 = a0, ¬(a2 ∈ s0 ↔ a2 = a1), ¬(a3 ∈ s0 ↔ a3 = a0), 1 ≠ # s0, a0 ≠ a1, ¬ a ∈ s0, ∀ a2. a2 = a ∨ a2 ∈ s0 ↔ a2 = a1 ∨ a2 = a0, a0 = a ∨ a0 ∈ s0, a1 = a ∨ a1 ∈ s0 ⊦ ∃ a. s0 = ∅ ++ a

Rule argument

Additional information

Used terms: a3

Proof step 42 from proof size-two (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 43:

  a3 = a ∨ a3 ∈ s0 ↔ a3 = a1 ∨ a3 = a0, a2 = a ∨ a2 ∈ s0 ↔ a2 = a1 ∨ a2 = a0, ¬(a3 ∈ s0 ↔ a3 = a0), 1 ≠ # s0, a0 ≠ a1, a2 ≠ a1, a2 ∈ s0, ¬ a ∈ s0, ∀ a2. a2 = a ∨ a2 ∈ s0 ↔ a2 = a1 ∨ a2 = a0, a1 = a ∨ a1 ∈ s0, a0 = a ∨ a0 ∈ s0 ⊦ ∃ a. s0 = ∅ ++ a

Rule argument

Additional information

Proof step 43 from proof size-two (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 44:

  1 ≠ # s0, a0 ≠ a1, a1 ∈ s0, a0 ∈ s0, ¬ a ∈ s0, ∀ a2. a2 = a ∨ a2 ∈ s0 → a2 = a1 ∨ a2 = a0 ⊦ ∃ a. s0 = ∅ ++ a

Rule argument

Additional information

Used simplifier rules: ne-01: ⊦ a ∈ s → s ≠ ∅; ne-02: ⊦ a ∈ s → (s = ∅ ↔ false);

Proof step 44 from proof size-two (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: a