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

User applied rule apply lemma

And obtained the following new goals

• Proof step 2:

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

• Proof step 3:

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

Rule argument

Additional information

Used terms: s

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

Lemma selsize

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

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

Rule argument

Additional information

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

User applied rule case distinction

And obtained the following new goals

• Proof step 5:

  # s = 3, # s ≠ 0 → a ∈ s ⊦ ∃ a, b, c. a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ s = ∅ ++ a ++ b ++ c

• Proof step 21:

  # s ≠ 3, # s ≠ 0 → a ∈ s, ∃ a, b, c. a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ s = ∅ ++ a ++ b ++ c ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  # s = 3, a ∈ s ⊦ ∃ a, b, c. a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ s = ∅ ++ a ++ b ++ c

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

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

• Proof step 8:

  # s = 3, ∃ s0. s = s0 ++ a ∧ ¬ a ∈ s0 ⊦ ∃ a, b, c. a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ s = ∅ ++ a ++ b ++ c

Rule argument

Additional information

Used terms: s, a

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

Lemma indef

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

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

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 9 from proof size-three-02 (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 10:

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

• Proof step 11:

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

Rule argument

Additional information

Used terms: s0

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

Lemma selsize

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

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

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 13:

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

• Proof step 14:

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

Rule argument

Additional information

Used terms: s0, a0

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

Lemma indef

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

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

Rule argument

Additional information

Used simplifier rules: Size-insert: ⊦ ¬ a ∈ s → #(s ++ a) = # s + 1; In-insert: ⊦ a ∈ s ++ b ↔ a = b ∨ a ∈ s; 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 15 from proof size-three-02 (previous step) (back to tree)

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 16:

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

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

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

Rule argument

Additional information

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

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 18:

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

• Proof step 19:

  1 = # s1, a ≠ a0, ¬ a0 ∈ s1, ¬ a ∈ s1, # s1 ≠ 0 → (∃ a. a ∈ s1) ⊦ ∃ a1, b, c. a1 ≠ b ∧ a1 ≠ c ∧ b ≠ c ∧ s1 ++ a0 ++ a = ∅ ++ a1 ++ b ++ c

Rule argument

Additional information

Used terms: s1

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

Lemma selsize

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

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

Rule argument

Additional information

Used simplifier rules: size-one-02: ⊦ # s = 1 ∧ a ∈ s ∧ b ∈ s → a = b; one-in: ⊦ # s = 1 ∧ a ∈ s → s = ∅ ++ a; ne-01: ⊦ a ∈ s → s ≠ ∅; size-one-01: ⊦ #(∅ ++ a) = 1; ne: ⊦ ∅ ≠ s ++ a; in-04: ⊦ a ∈ ∅ ++ b ↔ a = b;

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

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: a1, a0, a

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  #(∅ ++ a0 ++ a1 ++ a2) ≠ 0, #(∅ ++ a0 ++ a1 ++ a2) ≠ 3, a0 ≠ a2, a0 ≠ a1, a1 ≠ a2, a = a2 ∨ a = a1 ∨ a = a0 ⊦

Rule argument

Additional information

Used simplifier rules: In-insert: ⊦ a ∈ s ++ b ↔ a = b ∨ a ∈ s; in-04: ⊦ a ∈ ∅ ++ b ↔ a = b; size-zero-02: ⊦ # s = 0 → s = ∅; size-zero: ⊦ # s ≠ 0 → s ≠ ∅; ne: ⊦ ∅ ≠ s ++ a;

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

Heuristic weak cut applied rule cut formula

And closed the goal!

Rule argument

Additional information

Used simplifier rules: eq: ⊦ a ∈ s → s ++ a = s; In-insert: ⊦ a ∈ s ++ b ↔ a = b ∨ a ∈ s; in-04: ⊦ a ∈ ∅ ++ b ↔ a = b; Size-insert: ⊦ ¬ a ∈ s → #(s ++ a) = # s + 1; size-two-01: ⊦ #(∅ ++ a ++ b) = 2 ↔ a ≠ b; ⊦ m + 1 ≠ 0; (s) n0 < n ⊦ (* n) = m0 + (* n0) ↔ n - n0 = m0; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used formulas: a2 ∈ ∅ ++ a0 ++ a1