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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 2:

  bag0 ++ a ⊆ bag1 ⊦ ∃ bag2. bag1 = bag2 ++ a ∧ bag0 ⊆ bag2

Rule argument

Additional information

Used simplifier rules: subset-plusplus: ⊦ bag0 ++ a ⊆ bag1 ++ a ↔ bag0 ⊆ bag1;

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 3:

  ⊦ a ∈ bag → (∃ bag0. bag = bag0 ++ a)

• Proof step 4:

  bag0 ++ a ⊆ bag1, a ∈ bag1 → (∃ bag0. bag1 = bag0 ++ a) ⊦ ∃ bag2. bag1 = bag2 ++ a ∧ bag0 ⊆ bag2

Rule argument

Additional information

Used terms: a, bag1

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

Lemma exin

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  bag0 ⊆ bag ⊦ ∃ bag2. bag ++ a = bag2 ++ a ∧ bag0 ⊆ bag2

Rule argument

Additional information

Used simplifier rules: in: ⊦ a ∈ bag ↔ count(a, bag) ≠ 0; subset-in: ⊦ bag0 ++ a ⊆ bag1 → (count(a, bag1) = 0 ↔ false); subset-plusplus: ⊦ bag0 ++ a ⊆ bag1 ++ a ↔ bag0 ⊆ bag1;

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

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: bag