Proof step 1 from proof union-sizele (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(#(s ∪ s0) ≤ # s ↔ s0 ⊆ s) ⊦

Rule argument

Additional information

Proof step 2 from proof union-sizele (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ⊦ #(s ∪ s0) ≤ # s ↔ (∀ a. a ∈ s0 → a ∈ s)

Rule argument

Additional information

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

Proof step 3 from proof union-sizele (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 4:

  #(s ∪ s0) ≤ # s ⊦ ∀ a. a ∈ s0 → a ∈ s

• Proof step 10:

  ¬ #(s ∪ s0) ≤ # s, ∀ a. a ∈ s0 → a ∈ s ⊦

Rule argument

Additional information

Proof step 4 from proof union-sizele (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 5:

  #(s ∪ s0) = # s, #(s ∪ s0) ≤ # s ⊦ ∀ a. a ∈ s0 → a ∈ s

• Proof step 7:

  #(s ∪ s0) ≠ # s, #(s ∪ s0) ≤ # s ⊦ ∀ a. a ∈ s0 → a ∈ s

Rule argument

Additional information

Used formulas: #(s ∪ s0) = # s

Proof step 5 from proof union-sizele (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  a ∈ s0, #(s ∪ s0) ≤ # s, ¬ a ∈ s, ∀ a. a ∈ s0 → a ∈ s ⊦

Rule argument

Additional information

Used simplifier rules: union-sizeeq: ⊦ #(s ∪ s0) = # s ↔ s0 ⊆ s; una: ⊦ (s ∪ s0) ∪ s1 = s ∪ s0 ∪ s1; unc: ⊦ s ∪ s0 = s0 ∪ s; ⊦ s1 ⊆ s2 ↔ (∀ a. a ∈ s1 → a ∈ s2); (s)

Proof step 6 from proof union-sizele (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: a

Proof step 7 from proof union-sizele (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 8:

  #(s ∪ s0) ≠ # s, #(s ∪ s0) ≤ # s, ¬ #(s ∪ s0) < # s ⊦ ∀ a. a ∈ s0 → a ∈ s

Rule argument

Additional information

Used simplifier rules: union-sizeeq: ⊦ #(s ∪ s0) = # s ↔ s0 ⊆ s; union-size: ⊦ ¬ #(s ∪ s0) < # s; una: ⊦ (s ∪ s0) ∪ s1 = s ∪ s0 ∪ s1; unc: ⊦ s ∪ s0 = s0 ∪ s; ⊦ s1 ⊆ s2 ↔ (∀ a. a ∈ s1 → a ∈ s2); (s) Used formulas: #(s ∪ s0) < # s

Proof step 8 from proof union-sizele (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

  ⊦ m ≠ n → (m < n ↔ ¬ n < m)

Rule argument

Additional information

Used simplifier rules: union-sizeeq: ⊦ #(s ∪ s0) = # s ↔ s0 ⊆ s; una: ⊦ (s ∪ s0) ∪ s1 = s ∪ s0 ∪ s1; unc: ⊦ s ∪ s0 = s0 ∪ s; ⊦ s1 ⊆ s2 ↔ (∀ a. a ∈ s1 → a ∈ s2); (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat ⊦ m < n → n ≠ 0; (s) ⊦ ¬ n < n; (s) Used terms: # s, #(s ∪ s0)

Proof step 9 from proof union-sizele (previous step) (back to tree)

A spec-lemma

Proof step 10 from proof union-sizele (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 11:

  ⊦ s0 ⊆ s → s ∪ s0 = s

Rule argument

Additional information

Used simplifier rules: ⊦ s1 ⊆ s2 ↔ (∀ a. a ∈ s1 → a ∈ s2); (s) ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ ¬ n < n; (s) Used terms: s0, s

Proof step 11 from proof union-sizele (previous step) (back to tree)

Lemma union-sub