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

s = s0 \ s1, s1 ⊆ s0 ⊦ # s = # s0 - # s1

System applied rule normalize

And obtained the following new goals

Proof step 2:
s = s0 \ s1, # s ≠ # s0 - # s1, s1 ⊆ s0 ⊦

Rule argument

Additional information

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

s = s0 \ s1, # s ≠ # s0 - # s1, s1 ⊆ s0 ⊦

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 3:
#(s0 \ s1) ≠ # s0 - # s1, ∀ a. a ∈ s1 → a ∈ s0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ s1 ⊆ s2 ↔ (∀ a. a ∈ s1 → a ∈ s2); (s)

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

#(s0 \ s1) ≠ # s0 - # s1, ∀ a. a ∈ s1 → a ∈ s0 ⊦

User applied rule structural induction

And obtained the following new goals

Proof step 4:
#(s0 \ ∅) ≠ # s0 - # ∅, ∀ a. a ∈ ∅ → a ∈ s0 ⊦
Proof step 6:
#(s0 \ (s ++ elem)) ≠ # s0 - #(s ++ elem), ∀ a. a ∈ s ++ elem → a ∈ s0, ∀ s0. ¬(#(s0 \ s) ≠ # s0 - # s ∧ (∀ a. a ∈ s → a ∈ s0)) ⊦

Rule argument

indvar: s1

Additional information

Used simplifier rules: set generated by ∅, ++;;

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

#(s0 \ ∅) ≠ # s0 - # ∅, ∀ a. a ∈ ∅ → a ∈ s0 ⊦

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 5:
# s0 ≠ # s0 - 0 ⊦

Rule argument

Additional information

Used simplifier rules: diff-e: ⊦ s \ ∅ = s; ⊦ ¬ a ∈ ∅; (s) ⊦ # ∅ = 0; (s)

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

# s0 ≠ # s0 - 0 ⊦

Heuristic elimination applied rule apply elim lemma

And closed the goal!

Rule argument

spec: nat, name:elim-sub, seq:n ≤ m ⊦ n0 = m - n ↔ m = n0 + n, subst:[m, n, n0] → [# s0, 0, n0]

Additional information

Used simplifier rules: ⊦ 0 + m = m; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ 0 ≤ m; (s) n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: # s0, 0, n0

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

#(s0 \ (s ++ elem)) ≠ # s0 - #(s ++ elem), ∀ a. a ∈ s ++ elem → a ∈ s0, ∀ s0. ¬(#(s0 \ s) ≠ # s0 - # s ∧ (∀ a. a ∈ s → a ∈ s0)) ⊦

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 7:
#((s0 \ s) -- elem) ≠ # s0 - #(s ++ elem), ∀ a. a ∈ s ++ elem → a ∈ s0, ∀ s1. #(s1 \ s) = # s1 - # s ∨ ¬(∀ a. a ∈ s → a ∈ s1) ⊦

Rule argument

Additional information

Used simplifier rules: diff-add-del: ⊦ s1 \ (s2 ++ a) = (s1 \ s2) -- a;

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

#((s0 \ s) -- elem) ≠ # s0 - #(s ++ elem), ∀ a. a ∈ s ++ elem → a ∈ s0, ∀ s1. #(s1 \ s) = # s1 - # s ∨ ¬(∀ a. a ∈ s → a ∈ s1) ⊦

Heuristic weak cut applied rule cut formula

And obtained the following new goals

Proof step 8:
#((s0 \ s) -- elem) ≠ # s0 - #(s ++ elem), elem ∈ s0 \ s, ∀ s1. #(s1 \ s) = # s1 - # s ∨ ¬(∀ a. a ∈ s → a ∈ s1), ∀ a. a ∈ s ++ elem → a ∈ s0 ⊦
Proof step 28:
#((s0 \ s) -- elem) ≠ # s0 - #(s ++ elem), ¬ elem ∈ s0 \ s, ∀ s1. #(s1 \ s) = # s1 - # s ∨ ¬(∀ a. a ∈ s → a ∈ s1), ∀ a. a ∈ s ++ elem → a ∈ s0 ⊦

Rule argument

fma: elem ∈ s0 \ s

Additional information

Used formulas: elem ∈ s0 \ s

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

#((s0 \ s) -- elem) ≠ # s0 - #(s ++ elem), elem ∈ s0 \ s, ∀ s1. #(s1 \ s) = # s1 - # s ∨ ¬(∀ a. a ∈ s → a ∈ s1), ∀ a. a ∈ s ++ elem → a ∈ s0 ⊦

User applied rule apply rewrite lemma

And obtained the following new goals

Proof step 9:
⊦ a ∈ s → #(s -- a) = # s - 1
Proof step 10:
#(s0 \ s) - 1 ≠ # s0 - #(s ++ elem), elem ∈ s0 \ s, ∀ a. a ∈ s ++ elem → a ∈ s0, ∀ s1. #(s1 \ s) = # s1 - # s ∨ ¬(∀ a. a ∈ s → a ∈ s1) ⊦

Rule argument

spec: <toplevel>, name:del-size, seq: ⊦ a ∈ s → #(s -- a) = # s - 1, subst:[a, s] → [elem, s0 \ s], <all paths>

Additional information

Used terms: elem, s0 \ s

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

⊦ a ∈ s → #(s -- a) = # s - 1

Lemma del-size

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

#(s0 \ s) - 1 ≠ # s0 - #(s ++ elem), elem ∈ s0 \ s, ∀ a. a ∈ s ++ elem → a ∈ s0, ∀ s1. #(s1 \ s) = # s1 - # s ∨ ¬(∀ a. a ∈ s → a ∈ s1) ⊦

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 11:
#(s0 \ s) - 1 ≠ # s0 - # s + 1, elem ∈ s0, elem0 ∈ s0, ¬ elem ∈ s, ∀ a. a ∈ s ++ elem → a ∈ s0, ∀ s1. #(s1 \ s) = # s1 - # s ∨ ¬(∀ a. a ∈ s → a ∈ s1) ⊦

Rule argument

Additional information

Used simplifier rules: Difference: ⊦ a ∈ s1 \ s2 ↔ a ∈ s1 ∧ ¬ a ∈ s2; ⊦ ¬ a ∈ ∅; (s) ⊦ s1 = s2 ↔ (∀ a. a ∈ s1 ↔ a ∈ s2); (s) ne-01: ⊦ a ∈ s → s ≠ ∅; (forward) from specification set-basic ⊦ ¬ a ∈ s → #(s ++ a) = # s + 1; (s)

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

#(s0 \ s) - 1 ≠ # s0 - # s + 1, elem ∈ s0, elem0 ∈ s0, ¬ elem ∈ s, ∀ a. a ∈ s ++ elem → a ∈ s0, ∀ s1. #(s1 \ s) = # s1 - # s ∨ ¬(∀ a. a ∈ s → a ∈ s1) ⊦

User applied rule all left

And obtained the following new goals

Proof step 12:
#(s0 \ s) - 1 ≠ # s0 - # s + 1, elem0 ∈ s0, elem ∈ s0, ¬ elem ∈ s, ∀ a. a ∈ s ++ elem → a ∈ s0, #(s0 \ s) = # s0 - # s ∨ ¬(∀ a. a ∈ s → a ∈ s0) ⊦

Rule argument

pos: left 6 terms: s0 abort: F discard: T computed: T

Additional information

Used terms: s0

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

#(s0 \ s) - 1 ≠ # s0 - # s + 1, elem0 ∈ s0, elem ∈ s0, ¬ elem ∈ s, ∀ a. a ∈ s ++ elem → a ∈ s0, #(s0 \ s) = # s0 - # s ∨ ¬(∀ a. a ∈ s → a ∈ s0) ⊦

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 13:
#(s0 \ s) - 1 ≠ # s0 - # s + 1, elem ∈ s0, elem0 ∈ s0, ¬ elem ∈ s, ∀ a. a ∈ s ++ elem → a ∈ s0, #(s0 \ s) = # s0 - # s ∨ ¬(elem1 ∈ s → elem1 ∈ s0) ⊦

Rule argument

Additional information

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

#(s0 \ s) - 1 ≠ # s0 - # s + 1, elem ∈ s0, elem0 ∈ s0, ¬ elem ∈ s, ∀ a. a ∈ s ++ elem → a ∈ s0, #(s0 \ s) = # s0 - # s ∨ ¬(elem1 ∈ s → elem1 ∈ s0) ⊦

User applied rule case distinction

And obtained the following new goals

Proof step 14:
#(s0 \ s) = # s0 - # s, #(s0 \ s) - 1 ≠ # s0 - # s + 1, elem0 ∈ s0, elem ∈ s0, ¬ elem ∈ s, ∀ a. a ∈ s ++ elem → a ∈ s0 ⊦
Proof step 26:
#(s0 \ s) - 1 ≠ # s0 - # s + 1, elem1 ∈ s, elem0 ∈ s0, elem ∈ s0, ¬ elem1 ∈ s0, ¬ elem ∈ s, ∀ a. a ∈ s ++ elem → a ∈ s0 ⊦

Rule argument

pos: left 6

Additional information

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

#(s0 \ s) = # s0 - # s, #(s0 \ s) - 1 ≠ # s0 - # s + 1, elem0 ∈ s0, elem ∈ s0, ¬ elem ∈ s, ∀ a. a ∈ s ++ elem → a ∈ s0 ⊦

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 15:
#(s0 \ s) = # s0 - # s, # s0 - # s - 1 ≠ # s0 - # s + 1, elem ∈ s0, elem0 ∈ s0, ¬ elem ∈ s, ∀ a. a ∈ s → a ∈ s0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a ∈ s ++ b ↔ a = b ∨ a ∈ s; (s)

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

#(s0 \ s) = # s0 - # s, # s0 - # s - 1 ≠ # s0 - # s + 1, elem ∈ s0, elem0 ∈ s0, ¬ elem ∈ s, ∀ a. a ∈ s → a ∈ s0 ⊦

User applied rule apply elim lemma

And obtained the following new goals

Proof step 16:
#(s0 \ s) = # s0 - # s, # s0 - # s - 1 ≠ # s0 - # s + 1, elem0 ∈ s0, elem ∈ s0, ¬ elem ∈ s, ¬ # s ≤ # s0, ∀ a. a ∈ s → a ∈ s0 ⊦
Proof step 21:
#(s0 \ s) = n0, # s0 = n0 + # s, n0 - 1 ≠ # s0 - # s + 1, elem0 ∈ s0, elem ∈ s0, # s ≤ # s0, ¬ elem ∈ s, ∀ a. a ∈ s → a ∈ s0 ⊦

Rule argument

spec: nat, name:elim-sub, seq:n ≤ m ⊦ n0 = m - n ↔ m = n0 + n, subst:[m, n, n0] → [# s0, # s, n0]

Additional information

Used simplifier rules: n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: # s0, # s, n0

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

#(s0 \ s) = # s0 - # s, # s0 - # s - 1 ≠ # s0 - # s + 1, elem0 ∈ s0, elem ∈ s0, ¬ elem ∈ s, ¬ # s ≤ # s0, ∀ a. a ∈ s → a ∈ s0 ⊦

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 17:
#(s0 \ s) = # s0 - # s, # s0 - # s - 1 ≠ # s0 - # s + 1, # s0 < # s, elem0 ∈ s0, elem ∈ s0, ¬ elem ∈ s, ∀ a. a ∈ s → a ∈ s0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ m ≤ n ↔ ¬ n < m; (ss)

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

#(s0 \ s) = # s0 - # s, # s0 - # s - 1 ≠ # s0 - # s + 1, # s0 < # s, elem0 ∈ s0, elem ∈ s0, ¬ elem ∈ s, ∀ a. a ∈ s → a ∈ s0 ⊦

User applied rule apply lemma

And obtained the following new goals

Proof step 18:
# s < # s0 ⊦ ∃ a. a ∈ s0 ∧ ¬ a ∈ s
Proof step 19:
#(s0 \ s) = # s0 - # s, # s0 - # s - 1 ≠ # s0 - # s + 1, # s0 < # s, elem ∈ s0, elem0 ∈ s0, ¬ elem ∈ s, ∀ a. a ∈ s → a ∈ s0, ∃ a. a ∈ s ∧ ¬ a ∈ s0 ⊦

Rule argument

spec: set-basic, name:size-exgr, seq:# s < # s0 ⊦ ∃ a. a ∈ s0 ∧ ¬ a ∈ s, subst:[s, s0] → [s0, s]

Additional information

Used terms: s0, s

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

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

A spec-lemma

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

#(s0 \ s) = # s0 - # s, # s0 - # s - 1 ≠ # s0 - # s + 1, # s0 < # s, elem ∈ s0, elem0 ∈ s0, ¬ elem ∈ s, ∀ a. a ∈ s → a ∈ s0, ∃ a. a ∈ s ∧ ¬ a ∈ s0 ⊦

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 20:
#(s0 \ s) = # s0 - # s, # s0 - # s - 1 ≠ # s0 - # s + 1, # s0 < # s, elem ∈ s0, elem0 ∈ s0, elem1 ∈ s, elem2 ∈ s, ¬ elem1 ∈ s0, ¬ elem ∈ s, ∀ a. a ∈ s → a ∈ s0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ a ∈ ∅; (s) ⊦ s1 = s2 ↔ (∀ a. a ∈ s1 ↔ a ∈ s2); (s) ne-01: ⊦ a ∈ s → s ≠ ∅; (forward) from specification set-basic

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

#(s0 \ s) = # s0 - # s, # s0 - # s - 1 ≠ # s0 - # s + 1, # s0 < # s, elem ∈ s0, elem0 ∈ s0, elem1 ∈ s, elem2 ∈ s, ¬ elem1 ∈ s0, ¬ elem ∈ s, ∀ a. a ∈ s → a ∈ s0 ⊦

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

pos: left 10 terms: elem1

Additional information

Used terms: elem1

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

#(s0 \ s) = n0, # s0 = n0 + # s, n0 - 1 ≠ # s0 - # s + 1, elem0 ∈ s0, elem ∈ s0, # s ≤ # s0, ¬ elem ∈ s, ∀ a. a ∈ s → a ∈ s0 ⊦

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 22:
# s0 = #(s0 \ s) + # s, #(s0 \ s) - 1 ≠ # s0 - # s + 1, elem ∈ s0, elem0 ∈ s0, # s ≤ # s0, ¬ elem ∈ s, ∀ a. a ∈ s → a ∈ s0 ⊦

Rule argument

Additional information

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

# s0 = #(s0 \ s) + # s, #(s0 \ s) - 1 ≠ # s0 - # s + 1, elem ∈ s0, elem0 ∈ s0, # s ≤ # s0, ¬ elem ∈ s, ∀ a. a ∈ s → a ∈ s0 ⊦

User applied rule apply rewrite lemma

And obtained the following new goals

Proof step 23:
n ≤ m ⊦ n0 = m - n ↔ m = n0 + n
Proof step 24:
# s0 = #(s0 \ s) + # s, #(s0 \ s) - 1 ≠ # s0 - # s + 1, elem0 ∈ s0, elem ∈ s0, # s ≤ # s0, ¬ elem ∈ s, ¬ # s + 1 ≤ # s0, ∀ a. a ∈ s → a ∈ s0 ⊦

Rule argument

spec: nat, name:elim-sub, seq:n ≤ m ⊦ n0 = m - n ↔ m = n0 + n, subst:[n, m, n0] → [# s + 1, # s0, #(s0 \ s) - 1], <all paths>

Additional information

Used simplifier rules: ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ m < 1 ↔ m = 0; (s) ⊦ m + 1 ≤ n ↔ m < n; (s) size-zero-02: ⊦ # s = 0 → s = ∅; (forward) from specification set-basic f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic ⊦ s1 = s2 ↔ (∀ a. a ∈ s1 ↔ a ∈ s2); (s) ⊦ ¬ a ∈ ∅; (s) ⊦ m < n → n ≠ 0; (s) ⊦ m < m + n ↔ n ≠ 0; (s) n ≤ m ⊦ (m - n) + n0 = n1 ↔ m + n0 = n + n1; (s) ⊦ m + n = m + n0 ↔ n = n0; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: # s + 1, # s0, #(s0 \ s) - 1

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

n ≤ m ⊦ n0 = m - n ↔ m = n0 + n

A spec-lemma

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

# s0 = #(s0 \ s) + # s, #(s0 \ s) - 1 ≠ # s0 - # s + 1, elem0 ∈ s0, elem ∈ s0, # s ≤ # s0, ¬ elem ∈ s, ¬ # s + 1 ≤ # s0, ∀ a. a ∈ s → a ∈ s0 ⊦

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 25:
#(s0 \ s) = 0, # s = # s0, 0 - 1 ≠ # s0 - # s0 + 1, elem ∈ s0, elem0 ∈ s0, ¬ elem ∈ s, ∀ a. a ∈ s → a ∈ s0, ∀ a. ¬ a ∈ s0 \ s ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ a ∈ ∅; (s) ⊦ s1 = s2 ↔ (∀ a. a ∈ s1 ↔ a ∈ s2); (s) size-zero-02: ⊦ # s = 0 → s = ∅; (forward) from specification set-basic ⊦ m ≤ m; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m = m + n ↔ n = 0; (s) ⊦ m ≤ n → (n ≤ m ↔ m = n); (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m + 1 ≤ n ↔ m < n; (s)

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

#(s0 \ s) = 0, # s = # s0, 0 - 1 ≠ # s0 - # s0 + 1, elem ∈ s0, elem0 ∈ s0, ¬ elem ∈ s, ∀ a. a ∈ s → a ∈ s0, ∀ a. ¬ a ∈ s0 \ s ⊦

User applied rule all left

And closed the goal!

Rule argument

pos: left 8 terms: elem abort: F discard: F computed: F

Additional information

Used simplifier rules: Difference: ⊦ a ∈ s1 \ s2 ↔ a ∈ s1 ∧ ¬ a ∈ s2; Used terms: elem

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

#(s0 \ s) - 1 ≠ # s0 - # s + 1, elem1 ∈ s, elem0 ∈ s0, elem ∈ s0, ¬ elem1 ∈ s0, ¬ elem ∈ s, ∀ a. a ∈ s ++ elem → a ∈ s0 ⊦

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 27:
# s ≠ 0, #(s0 \ s) - 1 ≠ # s0 - # s + 1, s ≠ ∅, elem1 ∈ s, elem0 ∈ s0, elem ∈ s0, ¬ elem ∈ s, ¬ elem1 ∈ s0, ∀ a. a ∈ s → a ∈ s0 ⊦

Rule argument

Additional information

Used simplifier rules: size-zero-01: ⊦ s ≠ ∅ → # s ≠ 0; (forward) from specification set-basic ne-01: ⊦ a ∈ s → s ≠ ∅; (forward) from specification set-basic ⊦ a ∈ s ++ b ↔ a = b ∨ a ∈ s; (s)

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

# s ≠ 0, #(s0 \ s) - 1 ≠ # s0 - # s + 1, s ≠ ∅, elem1 ∈ s, elem0 ∈ s0, elem ∈ s0, ¬ elem ∈ s, ¬ elem1 ∈ s0, ∀ a. a ∈ s → a ∈ s0 ⊦

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

pos: left 9 terms: elem1

Additional information

Used terms: elem1

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

#((s0 \ s) -- elem) ≠ # s0 - #(s ++ elem), ¬ elem ∈ s0 \ s, ∀ s1. #(s1 \ s) = # s1 - # s ∨ ¬(∀ a. a ∈ s → a ∈ s1), ∀ a. a ∈ s ++ elem → a ∈ s0 ⊦

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 29:
#(s0 \ s) ≠ # s0 - #(s ++ elem), ¬ elem ∈ s0 \ s, ∀ a. a ∈ s ++ elem → a ∈ s0, ∀ s1. #(s1 \ s) = # s1 - # s ∨ ¬(∀ a. a ∈ s → a ∈ s1) ⊦

Rule argument

Additional information

Used simplifier rules: del-in: ⊦ ¬ a ∈ s → s -- a = s;

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

#(s0 \ s) ≠ # s0 - #(s ++ elem), ¬ elem ∈ s0 \ s, ∀ a. a ∈ s ++ elem → a ∈ s0, ∀ s1. #(s1 \ s) = # s1 - # s ∨ ¬(∀ a. a ∈ s → a ∈ s1) ⊦

User applied rule all left

And obtained the following new goals

Proof step 30:
#(s0 \ s) ≠ # s0 - #(s ++ elem), ¬ elem ∈ s0 \ s, ∀ a. a ∈ s ++ elem → a ∈ s0, #(s0 \ s) = # s0 - # s ∨ ¬(∀ a. a ∈ s → a ∈ s0) ⊦

Rule argument

pos: left 4 terms: s0 abort: F discard: T computed: T

Additional information

Used terms: s0

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

#(s0 \ s) ≠ # s0 - #(s ++ elem), ¬ elem ∈ s0 \ s, ∀ a. a ∈ s ++ elem → a ∈ s0, #(s0 \ s) = # s0 - # s ∨ ¬(∀ a. a ∈ s → a ∈ s0) ⊦

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 31:
#(s0 \ s) ≠ # s0 - #(s ++ elem), ¬ elem ∈ s0 \ s, ∀ a. a ∈ s ++ elem → a ∈ s0, #(s0 \ s) = # s0 - # s ∨ ¬(elem0 ∈ s → elem0 ∈ s0) ⊦

Rule argument

Additional information

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

#(s0 \ s) ≠ # s0 - #(s ++ elem), ¬ elem ∈ s0 \ s, ∀ a. a ∈ s ++ elem → a ∈ s0, #(s0 \ s) = # s0 - # s ∨ ¬(elem0 ∈ s → elem0 ∈ s0) ⊦

User applied rule case distinction

And obtained the following new goals

Proof step 32:
#(s0 \ s) = # s0 - # s, #(s0 \ s) ≠ # s0 - #(s ++ elem), ¬ elem ∈ s0 \ s, ∀ a. a ∈ s ++ elem → a ∈ s0 ⊦
Proof step 34:
#(s0 \ s) ≠ # s0 - #(s ++ elem), elem0 ∈ s, ¬ elem0 ∈ s0, ¬ elem ∈ s0 \ s, ∀ a. a ∈ s ++ elem → a ∈ s0 ⊦

Rule argument

pos: left 4

Additional information

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

#(s0 \ s) = # s0 - # s, #(s0 \ s) ≠ # s0 - #(s ++ elem), ¬ elem ∈ s0 \ s, ∀ a. a ∈ s ++ elem → a ∈ s0 ⊦

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 33:
#(s0 \ s) = # s0 - # s, # s0 - # s ≠ # s0 - #(s ++ elem), ¬ elem ∈ s0 \ s, ∀ a. a = elem ∨ a ∈ s → a ∈ s0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a ∈ s ++ b ↔ a = b ∨ a ∈ s; (s)

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

#(s0 \ s) = # s0 - # s, # s0 - # s ≠ # s0 - #(s ++ elem), ¬ elem ∈ s0 \ s, ∀ a. a = elem ∨ a ∈ s → a ∈ s0 ⊦

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

pos: left 4 terms: elem

Additional information

Used simplifier rules: Difference: ⊦ a ∈ s1 \ s2 ↔ a ∈ s1 ∧ ¬ a ∈ s2; ⊦ a ∈ s → s ++ a = s; (s) Used terms: elem

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

#(s0 \ s) ≠ # s0 - #(s ++ elem), elem0 ∈ s, ¬ elem0 ∈ s0, ¬ elem ∈ s0 \ s, ∀ a. a ∈ s ++ elem → a ∈ s0 ⊦

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 35:
#(s0 \ s) ≠ # s0 - #(s ++ elem), # s ≠ 0, s ≠ ∅, elem0 ∈ s, ¬ elem ∈ s0 \ s, ¬ elem0 ∈ s0, ∀ a. a = elem ∨ a ∈ s → a ∈ s0 ⊦

Rule argument

Additional information

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

#(s0 \ s) ≠ # s0 - #(s ++ elem), # s ≠ 0, s ≠ ∅, elem0 ∈ s, ¬ elem ∈ s0 \ s, ¬ elem0 ∈ s0, ∀ a. a = elem ∨ a ∈ s → a ∈ s0 ⊦