Proof step 27 from proof bag-add-rem-same (previous step)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 28:

  n0 = n, ∀ n. (∀ n0. count(n0, (bag0 -- n) ++ n) = count(n0, bag0)) ↔ count(n, bag0) ≠ 0 ⊦ 1 + count(n0, bag0 -- n) = count(n0, bag0), count(n, bag0) = 0, n = m, n0 = m

• Proof step 31:

  ∀ n. (∀ n0. count(n0, (bag0 -- n) ++ n) = count(n0, bag0)) ↔ count(n, bag0) ≠ 0 ⊦ 0 + count(n0, bag0 -- n) = count(n0, bag0), count(n, bag0) = 0, n = m, n0 = m, n0 = n

Rule argument

Additional information