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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(bag ∪ bag1 ⊆ bag ∪ bag2 ↔ bag1 ⊆ bag2) ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 3:

  ⊦ bag0 ⊆ bag1 ↔ (∀ a. count(a, bag0) ≤ count(a, bag1))

• Proof step 4:

  ⊦ (∀ a. count(a, bag ∪ bag1) ≤ count(a, bag ∪ bag2)) ↔ bag1 ⊆ bag2

Rule argument

Additional information

Used terms: bag ∪ bag2, bag ∪ bag1

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

Lemma count-subset

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  ⊦ (∀ a. count(a, bag1) ≤ count(a, bag2)) ↔ bag1 ⊆ bag2

Rule argument

Additional information

Used simplifier rules: union: ⊦ count(a, bag0 ∪ bag1) = count(a, bag0) + count(a, bag1); union-ass: ⊦ bag0 ∪ bag1 ∪ bag2 = (bag0 ∪ bag1) ∪ bag2; union-com: ⊦ bag0 ∪ bag1 = bag1 ∪ bag0; c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m + n ≤ m + n0 ↔ n ≤ n0; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

  ⊦ bag0 ⊆ bag1 ↔ (∀ a. count(a, bag0) ≤ count(a, bag1))

Rule argument

Additional information

Used terms: bag2, bag1

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

Lemma count-subset