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

User applied rule structural induction

And obtained the following new goals

• Proof step 2:

  # ∅ < # s0 ⊦ ∃ a. a ∈ s0 ∧ ¬ a ∈ ∅

• Proof step 6:

  #(s1 ++ a) < # s0, ∀ s0. # s1 < # s0 → (∃ a. a ∈ s0 ∧ ¬ a ∈ s1) ⊦ ∃ a0. a0 ∈ s0 ∧ ¬ a0 ∈ s1 ++ a

Rule argument

Additional information

Used simplifier rules: gen: ⊦ ;

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  # s0 ≠ 0, s0 ≠ ∅ ⊦ ∃ a. a ∈ s0

Rule argument

Additional information

Used simplifier rules: Size-empty: ⊦ # ∅ = 0; In-empty: ⊦ ¬ a ∈ ∅; size-zero: ⊦ # s ≠ 0 → s ≠ ∅; size-zero-01: ⊦ s ≠ ∅ → # s ≠ 0; ⊦ 0 < m ↔ m ≠ 0; (s)

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

User applied rule constructor cut

And obtained the following new goals

• Proof step 4:

  s0 = s ++ a0, # s0 ≠ 0, s0 ≠ s, s0 ≠ ∅ ⊦ ∃ a. a ∈ s0

Rule argument

Additional information

Used simplifier rules: gen: ⊦ ;

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  ¬ a0 ∈ s ⊦ ∃ a. a = a0 ∨ a ∈ s

Rule argument

Additional information

Used simplifier rules: eq-03: ⊦ s ++ a = s ↔ a ∈ s; ne: ⊦ ∅ ≠ s ++ a; 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 ⊦ m + 1 ≠ 0; (s)

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

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: a0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  #(s1 ++ a) < # s0, ∀ s0. # s1 < # s0 → (∃ a. a ∈ s0 ∧ ¬ a ∈ s1) ⊦ ∃ a0. a0 ∈ s0 ∧ a0 ≠ a ∧ ¬ a0 ∈ s1

Rule argument

Additional information

Used simplifier rules: In-insert: ⊦ a ∈ s ++ b ↔ a = b ∨ a ∈ s; ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic

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

Heuristic cut applied rule cut formula

And obtained the following new goals

• Proof step 8:

  #(s1 ++ a) < # s0, a ∈ s0, ∀ s0. # s1 < # s0 → (∃ a. a ∈ s0 ∧ ¬ a ∈ s1) ⊦ ∃ a0. a0 ∈ s0 ∧ a0 ≠ a ∧ ¬ a0 ∈ s1

• Proof step 26:

  #(s1 ++ a) < # s0, ¬ a ∈ s0, ∀ s0. # s1 < # s0 → (∃ a. a ∈ s0 ∧ ¬ a ∈ s1) ⊦ ∃ a0. a0 ∈ s0 ∧ a0 ≠ a ∧ ¬ a0 ∈ s1

Rule argument

Additional information

Used formulas: a ∈ s0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  #(s1 ++ a) < # s0, a ∈ s0, ∀ s0. # s1 < # s0 → (∃ a. a ∈ s0 ∧ ¬ a ∈ s1) ⊦ ∃ a0. a0 ∈ s0 ∧ a0 ≠ a ∧ ¬ a0 ∈ s1

Rule argument

Additional information

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

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

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 10:

  #(s1 ++ a) < # s0, a ∈ s0, a ∈ s1, ∀ s0. # s1 < # s0 → (∃ a. a ∈ s0 ∧ ¬ a ∈ s1) ⊦ ∃ a0. a0 ∈ s0 ∧ a0 ≠ a ∧ ¬ a0 ∈ s1

• Proof step 14:

  #(s1 ++ a) < # s0, a ∈ s0, ¬ a ∈ s1, ∀ s0. # s1 < # s0 → (∃ a. a ∈ s0 ∧ ¬ a ∈ s1) ⊦ ∃ a0. a0 ∈ s0 ∧ a0 ≠ a ∧ ¬ a0 ∈ s1

Rule argument

Additional information

Used formulas: a ∈ s1

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  # s1 < # s0, a ∈ s0, a ∈ s1, ∀ s0. # s1 < # s0 → (∃ a. a ∈ s0 ∧ ¬ a ∈ s1) ⊦ ∃ a0. a0 ∈ s0 ∧ ¬ a0 ∈ s1

Rule argument

Additional information

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

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

Heuristic quantifier closing applied rule all left

And obtained the following new goals

• Proof step 12:

  # s1 < # s0, a ∈ s1, a ∈ s0, # s1 < # s0 → (∃ a. a ∈ s0 ∧ ¬ a ∈ s1), ∀ s0. # s1 < # s0 → (∃ a. a ∈ s0 ∧ ¬ a ∈ s1) ⊦ ∃ a0. a0 ∈ s0 ∧ ¬ a0 ∈ s1

Rule argument

Additional information

Used terms: s0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  # s1 < # s0, a ∈ s0, a ∈ s1, a0 ∈ s0, ¬ a0 ∈ s1, ∀ s0. # s1 < # s0 → (∃ a. a ∈ s0 ∧ ¬ a ∈ s1) ⊦ ∃ a0. a0 ∈ s0 ∧ ¬ a0 ∈ s1

Rule argument

Additional information

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

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: a0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  # s1 + 1 < # s0, a ∈ s0, ¬ a ∈ s1, ∀ s0. # s1 < # s0 → (∃ a. a ∈ s0 ∧ ¬ a ∈ s1) ⊦ ∃ a0. a0 ∈ s0 ∧ a0 ≠ a ∧ ¬ a0 ∈ s1

Rule argument

Additional information

Used simplifier rules: Size-insert: ⊦ ¬ a ∈ s → #(s ++ a) = # s + 1;

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

User applied rule constructor cut

And obtained the following new goals

• Proof step 16:

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

• Proof step 21:

  s1 = s ++ a1, s1 ≠ s, # s1 + 1 < # s0, a ∈ s0, ¬ a ∈ s1, ∀ s0. # s1 < # s0 → (∃ a. a ∈ s0 ∧ ¬ a ∈ s1) ⊦ ∃ a0. a0 ∈ s0 ∧ a0 ≠ a ∧ ¬ a0 ∈ s1

Rule argument

Additional information

Used simplifier rules: gen: ⊦ ;

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  # s0 ≠ 1, # s0 ≠ 0, a ∈ s0, ∀ s. # s ≠ 0 → (∃ a0. a0 ∈ s) ⊦ ∃ a0. a0 ∈ s0 ∧ a0 ≠ a

Rule argument

Additional information

Used simplifier rules: Size-empty: ⊦ # ∅ = 0; In-empty: ⊦ ¬ a ∈ ∅; ⊦ 0 < m ↔ m ≠ 0; (s) ⊦ 1 < m ↔ ¬(m = 0 ∨ m = 1); (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 18:

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

• Proof step 19:

  # s0 ≠ 1, # s0 ≠ 0, ∀ s. # s ≠ 0 → (∃ a0. a0 ∈ s), ∃ s1. s0 = s1 ++ a ∧ ¬ a ∈ s1 ⊦ ∃ a0. a0 ∈ s0 ∧ a0 ≠ a

Rule argument

Additional information

Used terms: s0, a

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

Lemma indef

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  # s1 ≠ 0, s1 ≠ ∅, ¬ a ∈ s1, ∀ s. # s ≠ 0 → (∃ a0. a0 ∈ s) ⊦ ∃ a0. a0 ∈ s1

Rule argument

Additional information

Used simplifier rules: Size-insert: ⊦ ¬ a ∈ s → #(s ++ a) = # s + 1; in-02: ⊦ a ≠ b → (a ∈ s ++ b ↔ a ∈ s); size-zero: ⊦ # s ≠ 0 → s ≠ ∅; size-zero-01: ⊦ s ≠ ∅ → # s ≠ 0; c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m + 1 ≠ 0; (s) ⊦ m + n = 1 ↔ m = 0 ∧ n = 1 ∨ n = 0 ∧ m = 1; (ws)

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: s1

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  a ≠ a1, (# s + 1) + 1 < # s0, a ∈ s0, ¬ a1 ∈ s, ¬ a ∈ s, ∀ s1. # s + 1 < # s1 → (∃ a0. a0 ∈ s1 ∧ a0 ≠ a1 ∧ ¬ a0 ∈ s) ⊦ ∃ a0. a0 ∈ s0 ∧ a0 ≠ a ∧ a0 ≠ a1 ∧ ¬ a0 ∈ s

Rule argument

Additional information

Used simplifier rules: eq-03: ⊦ s ++ a = s ↔ a ∈ s; Size-insert: ⊦ ¬ a ∈ s → #(s ++ a) = # s + 1; In-insert: ⊦ a ∈ s ++ b ↔ a = b ∨ a ∈ s;

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 23:

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

• Proof step 24:

  a ≠ a1, (# s + 1) + 1 < # s0, ¬ a1 ∈ s, ¬ a ∈ s, ∀ s1. # s + 1 < # s1 → (∃ a0. a0 ∈ s1 ∧ a0 ≠ a1 ∧ ¬ a0 ∈ s), ∃ s1. s0 = s1 ++ a ∧ ¬ a ∈ s1 ⊦ ∃ a0. a0 ∈ s0 ∧ a0 ≠ a ∧ a0 ≠ a1 ∧ ¬ a0 ∈ s

Rule argument

Additional information

Used terms: s0, a

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

Lemma indef

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  a ≠ a1, # s + 1 < # s1, ¬ a ∈ s1, ¬ a ∈ s, ¬ a1 ∈ s, ∀ s1. # s + 1 < # s1 → (∃ a0. a0 ∈ s1 ∧ a0 ≠ a1 ∧ ¬ a0 ∈ s) ⊦ ∃ a0. a0 ∈ s1 ∧ a0 ≠ a1 ∧ ¬ a0 ∈ s

Rule argument

Additional information

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

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

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: s1

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  #(s1 ++ a) < # s0, ¬ a ∈ s0, ∀ s0. # s1 < # s0 → (∃ a. a ∈ s0 ∧ ¬ a ∈ s1) ⊦ ∃ a0. a0 ∈ s0 ∧ ¬ a0 ∈ s1

Rule argument

Additional information

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

User applied rule cut formula

And obtained the following new goals

• Proof step 28:

  #(s1 ++ a) < # s0, a ∈ s1, ¬ a ∈ s0, ∀ s0. # s1 < # s0 → (∃ a. a ∈ s0 ∧ ¬ a ∈ s1) ⊦ ∃ a0. a0 ∈ s0 ∧ ¬ a0 ∈ s1

• Proof step 32:

  #(s1 ++ a) < # s0, ¬ a ∈ s1, ¬ a ∈ s0, ∀ s0. # s1 < # s0 → (∃ a. a ∈ s0 ∧ ¬ a ∈ s1) ⊦ ∃ a0. a0 ∈ s0 ∧ ¬ a0 ∈ s1

Rule argument

Additional information

Used formulas: a ∈ s1

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 29:

  # s1 < # s0, a ∈ s1, ¬ a ∈ s0, ∀ s0. # s1 < # s0 → (∃ a. a ∈ s0 ∧ ¬ a ∈ s1) ⊦ ∃ a0. a0 ∈ s0 ∧ ¬ a0 ∈ s1

Rule argument

Additional information

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

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

Heuristic quantifier closing applied rule all left

And obtained the following new goals

• Proof step 30:

  # s1 < # s0, a ∈ s1, ¬ a ∈ s0, # s1 < # s0 → (∃ a. a ∈ s0 ∧ ¬ a ∈ s1), ∀ s0. # s1 < # s0 → (∃ a. a ∈ s0 ∧ ¬ a ∈ s1) ⊦ ∃ a0. a0 ∈ s0 ∧ ¬ a0 ∈ s1

Rule argument

Additional information

Used terms: s0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

  # s1 < # s0, a0 ∈ s0, a ∈ s1, ¬ a0 ∈ s1, ¬ a ∈ s0, ∀ s0. # s1 < # s0 → (∃ a. a ∈ s0 ∧ ¬ a ∈ s1) ⊦ ∃ a0. a0 ∈ s0 ∧ ¬ a0 ∈ s1

Rule argument

Additional information

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

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

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: a0

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

Heuristic quantifier closing applied rule all left

And obtained the following new goals

• Proof step 33:

  #(s1 ++ a) < # s0, ¬ a ∈ s1, ¬ a ∈ s0, # s1 < # s0 → (∃ a. a ∈ s0 ∧ ¬ a ∈ s1), ∀ s0. # s1 < # s0 → (∃ a. a ∈ s0 ∧ ¬ a ∈ s1) ⊦ ∃ a0. a0 ∈ s0 ∧ ¬ a0 ∈ s1

Rule argument

Additional information

Used terms: s0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 34:

  # s1 < # s0, # s1 + 1 < # s0, a0 ∈ s0, ¬ a0 ∈ s1, ¬ a ∈ s1, ¬ a ∈ s0, ∀ s0. # s1 < # s0 → (∃ a. a ∈ s0 ∧ ¬ a ∈ s1) ⊦ ∃ a0. a0 ∈ s0 ∧ ¬ a0 ∈ s1

Rule argument

Additional information

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

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

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: a0