Proof step 1 from proof difference (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  (bag0 \ bag1).count(a) ≠ (bag1.count(a) ≤ bag0.count(a) ⊃ bag0.count(a) - bag1.count(a);0) ⊦

Rule argument

Additional information

Proof step 2 from proof difference (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 3:

  (bag0 \ (bag ++ a0)).count(a) ≠ ((bag ++ a0).count(a) ≤ bag0.count(a) ⊃ bag0.count(a) - (bag ++ a0).count(a);0), ∀ bag0, a. (bag0 \ bag).count(a) = (bag.count(a) ≤ bag0.count(a) ⊃ bag0.count(a) - bag.count(a);0) ⊦

Rule argument

Additional information

Used simplifier rules: diff-empty: ⊦ bag0 \ ∅ = bag0; Bag[A] generated by ∅, ++; ⊦ 0 ≤ m; (s) ⊦ ∅.count(a) = 0; (s) ⊦ m - 0 = m; (s)

Proof step 3 from proof difference (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  ((bag0 -- a0) \ bag).count(a) ≠ ((bag ++ a0).count(a) ≤ bag0.count(a) ⊃ bag0.count(a) - (bag ++ a0).count(a);0), ∀ bag0, a. (bag0 \ bag).count(a) = (bag.count(a) ≤ bag0.count(a) ⊃ bag0.count(a) - bag.count(a);0) ⊦

Rule argument

Additional information

Used simplifier rules: diff-rec: ⊦ bag0 \ (bag1 ++ a) = (bag0 -- a) \ bag1;

Proof step 4 from proof difference (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 5:

  ⊦ bag.count(a) = 0 → bag -- a = bag

• Proof step 6:

  bag0.count(a0) ≠ 0, ((bag0 -- a0) \ bag).count(a) ≠ ((bag ++ a0).count(a) ≤ bag0.count(a) ⊃ bag0.count(a) - (bag ++ a0).count(a);0), ∀ bag0, a. (bag0 \ bag).count(a) = (bag.count(a) ≤ bag0.count(a) ⊃ bag0.count(a) - bag.count(a);0) ⊦

• Proof step 15:

  bag0.count(a0) = 0, (bag0 \ bag).count(a) ≠ ((bag ++ a0).count(a) ≤ bag0.count(a) ⊃ bag0.count(a) - (bag ++ a0).count(a);0), ∀ bag0, a. (bag0 \ bag).count(a) = (bag.count(a) ≤ bag0.count(a) ⊃ bag0.count(a) - bag.count(a);0) ⊦

Rule argument

Additional information

Used terms: bag0, a0

Proof step 5 from proof difference (previous step) (back to tree)

Lemma del-notin

Proof step 6 from proof difference (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 7:

  ((bag0 -- a0) \ bag).count(a) = (bag.count(a) ≤ (bag0 -- a0).count(a) ⊃ (bag0 -- a0).count(a) - bag.count(a);0), bag0.count(a0) ≠ 0, ((bag0 -- a0) \ bag).count(a) ≠ ((bag ++ a0).count(a) ≤ bag0.count(a) ⊃ bag0.count(a) - (bag ++ a0).count(a);0) ⊦

Rule argument

Additional information

Used terms: bag0 -- a0, a

Proof step 7 from proof difference (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  ((bag0 -- a0) \ bag).count(a) = (bag.count(a) ≤ bag0.count(a) - (a = a0 ⊃ 1;0) ⊃ bag0.count(a) - (a = a0 ⊃ 1;0) - bag.count(a);0), bag0.count(a0) ≠ 0, ((bag0 -- a0) \ bag).count(a) ≠ ((bag ++ a0).count(a) ≤ bag0.count(a) ⊃ bag0.count(a) - (bag ++ a0).count(a);0) ⊦

Rule argument

Additional information

Used simplifier rules: count-del: ⊦ (bag -- b).count(a) = bag.count(a) - (a = b ∧ bag.count(a) ≠ 0 ⊃ 1;0);

Proof step 8 from proof difference (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 9:

  bag0.count(a0) ≠ 0, (bag.count(a) ≤ bag0.count(a) - (a = a0 ⊃ 1;0) ⊃ bag0.count(a) - (a = a0 ⊃ 1;0) - bag.count(a);0) ≠ ((bag ++ a0).count(a) ≤ bag0.count(a) ⊃ bag0.count(a) - (bag ++ a0).count(a);0) ⊦

Rule argument

Additional information

Proof step 9 from proof difference (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

  ⊦ a ≠ b → (bag ++ b).count(a) = bag.count(a)

• Proof step 11:

  a = a0, bag0.count(a0) ≠ 0, (bag.count(a) ≤ bag0.count(a) - (a = a0 ⊃ 1;0) ⊃ bag0.count(a) - (a = a0 ⊃ 1;0) - bag.count(a);0) ≠ ((bag ++ a0).count(a) ≤ bag0.count(a) ⊃ bag0.count(a) - (bag ++ a0).count(a);0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m - 0 = m; (s) Used terms: bag, a0, a

Proof step 10 from proof difference (previous step) (back to tree)

A spec-lemma

Proof step 11 from proof difference (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  bag0.count(a0) ≠ 0, (bag.count(a0) < bag0.count(a0) ⊃ bag0.count(a0) - 1 - bag.count(a0);0) ≠ (bag.count(a0) < bag0.count(a0) ⊃ bag0.count(a0) - bag.count(a0) + 1;0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ (bag ++ a).count(a) = bag.count(a) + 1; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m + 1 ≤ n ↔ m < n; (s) n0 ≤ n ⊦ m ≤ n - n0 ↔ m + n0 ≤ n; (s) ⊦ m < 1 ↔ m = 0; (s) ⊦ m ≤ n ↔ ¬ n < m; (ss)

Proof step 12 from proof difference (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 13:

  bag0.count(a0) - 1 - bag.count(a0) ≠ (bag.count(a0) < bag0.count(a0) ⊃ bag0.count(a0) - bag.count(a0) + 1;0), bag0.count(a0) ≠ 0, bag.count(a0) < bag0.count(a0) ⊦

Rule argument

Additional information

Proof step 13 from proof difference (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  bag0.count(a0) - 1 - bag.count(a0) ≠ bag0.count(a0) - bag.count(a0) + 1, bag.count(a0) < bag0.count(a0) ⊦

Rule argument

Additional information

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

Proof step 14 from proof difference (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic ⊦ m + 1 ≠ 0; (s) ⊦ m + n - n + n1 = m - n1; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic n ≠ 0 ⊦ m = n - 1 ↔ n = m + 1; (elim) Used terms: bag0.count(a0), n0

Proof step 15 from proof difference (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 16:

  bag0.count(a0) = 0, (bag0 \ bag).count(a) = (bag.count(a) ≤ bag0.count(a) ⊃ bag0.count(a) - bag.count(a);0), (bag0 \ bag).count(a) ≠ ((bag ++ a0).count(a) ≤ bag0.count(a) ⊃ bag0.count(a) - (bag ++ a0).count(a);0) ⊦

Rule argument

Additional information

Used terms: bag0, a

Proof step 16 from proof difference (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 17:

  bag0.count(a0) = 0, (bag.count(a) ≤ bag0.count(a) ⊃ bag0.count(a) - bag.count(a);0) ≠ ((bag ++ a0).count(a) ≤ bag0.count(a) ⊃ bag0.count(a) - (bag ++ a0).count(a);0) ⊦

Rule argument

Additional information

Proof step 17 from proof difference (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 18:

  ⊦ a ≠ b → (bag ++ b).count(a) = bag.count(a)

Rule argument

Additional information

Used simplifier rules: ⊦ m + 1 ≤ n ↔ m < n; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ (bag ++ a).count(a) = bag.count(a) + 1; (s) ⊦ m ≤ 0 ↔ m = 0; (s) ⊦ ¬ n < 0; (s) Used terms: bag, a0, a

Proof step 18 from proof difference (previous step) (back to tree)

A spec-lemma