Proof step 19 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 20:

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

• Proof step 23:

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

Rule argument

Additional information