---

Step * of Lemma assert-bag-eq

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[as,bs:bag(T)].  uiff(↑bag-eq(eq;as;bs);as = bs ∈ bag(T))
BY
{ xxx(xxx(UnivCD THENA Auto)xxx
      THEN Unfold `bag-eq` 0
      THEN (RW assert_pushdownC 0 THENA Auto)
      THEN (InstLemma `bag-extensionality2` [⌜T⌝;⌜eq⌝;⌜as⌝;⌜bs⌝]⋅ THENA Auto)
      THEN (InstLemma `assert-bag-all` [⌜T⌝;⌜eq⌝]⋅ THENA Auto)
      THEN (RWO "-1<" 0 THENA Auto)
      THEN (RW assert_pushdownC 0 THENA Auto)
      THEN Thin (-1)
      THEN Auto
      THEN ThinTrivial
      THEN Auto
      THEN Try ((BackThruSomeHyp THEN Auto)))xxx }

1
1. T : Type
2. eq : EqDecider(T)
3. as : bag(T)
4. bs : bag(T)
5. (∀x:T. (x ↓∈ as ⇒ ((#x in as) = (#x in bs) ∈ ℤ))) ∧ (∀x:T. (x ↓∈ bs ⇒ x ↓∈ as)) supposing as = bs ∈ bag(T)
6. as = bs ∈ bag(T) supposing (∀x:T. (x ↓∈ as ⇒ ((#x in as) = (#x in bs) ∈ ℤ))) ∧ (∀x:T. (x ↓∈ bs ⇒ x ↓∈ as))
7. ∀x:T. (x ↓∈ as ⇒ ((#x in as) = (#x in bs) ∈ ℤ))
8. ∀x:T. (x ↓∈ bs ⇒ 0 < (#x in as))
9. ∀x:T. (x ↓∈ as ⇒ ((#x in as) = (#x in bs) ∈ ℤ))
10. x : T
11. x ↓∈ bs
⊢ x ↓∈ as

2
1. T : Type
2. eq : EqDecider(T)
3. as : bag(T)
4. bs : bag(T)
5. as = bs ∈ bag(T)
6. x : T
7. x ↓∈ bs
8. ∀x:T. (x ↓∈ as ⇒ ((#x in as) = (#x in bs) ∈ ℤ))
9. ∀x:T. (x ↓∈ bs ⇒ x ↓∈ as)
10. as = bs ∈ bag(T)
⊢ 0 < (#x in as)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[as,bs:bag(T)].    uiff(\muparrow{}bag-eq(eq;as;bs);as  =  bs)


By

---

Latex:
xxx(xxx(UnivCD  THENA  Auto)xxx
        THEN  Unfold  `bag-eq`  0
        THEN  (RW  assert\_pushdownC  0  THENA  Auto)
        THEN  (InstLemma  `bag-extensionality2`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}as\mkleeneclose{};\mkleeneopen{}bs\mkleeneclose{}]\mcdot{}  THENA  Auto)
        THEN  (InstLemma  `assert-bag-all`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{}]\mcdot{}  THENA  Auto)
        THEN  (RWO  "-1<"  0  THENA  Auto)
        THEN  (RW  assert\_pushdownC  0  THENA  Auto)
        THEN  Thin  (-1)
        THEN  Auto
        THEN  ThinTrivial
        THEN  Auto
        THEN  Try  ((BackThruSomeHyp  THEN  Auto)))xxx

---

Home Index