---

Step * of Lemma assert-bag-deq-member

∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[b:bag(A)]. ∀[x:A].  uiff(↑bag-deq-member(eq;x;b);x ↓∈ b)
BY
{ (Auto
   THEN Try ((Unhide THEN Auto))
   THEN (MoveToConcl (-1)
         THEN UseWitness ⌜λx.Ax⌝⋅
         THEN D -2
         THEN Try (Complete (Auto))
         THEN (MemCD
               THEN Try (Complete (Auto))
               THEN (All
                     (RepUR ``bag-member bag-deq-member squash``)⋅
                     THEN ((MemTypeCD THEN Auto) ORELSE (D -1 THEN ExRepD))⋅
                     )⋅)⋅)⋅) }

1
1. A : Type
2. eq : EqDecider(A)
3. b : Base
4. b1 : Base
5. b = b1 ∈ pertype(λas,bs. ((as ∈ A List) ∧ (bs ∈ A List) ∧ permutation(A;as;bs)))
6. b ∈ A List
7. b1 ∈ A List
8. permutation(A;b;b1)
9. x : A
10. x1 : ↑x ∈b b
⊢ ∃L:A List. ((L = b ∈ bag(A)) ∧ (x ∈ L))

2
1. A : Type
2. eq : EqDecider(A)
3. b : Base
4. b1 : Base
5. b = b1 ∈ pertype(λas,bs. ((as ∈ A List) ∧ (bs ∈ A List) ∧ permutation(A;as;bs)))
6. b ∈ A List
7. b1 ∈ A List
8. permutation(A;b;b1)
9. x : A
10. L : A List
11. L = b ∈ bag(A)
12. (x ∈ L)
⊢ Ax = Ax ∈ (↑x ∈b b)

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[eq:EqDecider(A)].  \mforall{}[b:bag(A)].  \mforall{}[x:A].    uiff(\muparrow{}bag-deq-member(eq;x;b);x  \mdownarrow{}\mmember{}  b)


By

---

Latex:
(Auto
  THEN  Try  ((Unhide  THEN  Auto))
  THEN  (MoveToConcl  (-1)
              THEN  UseWitness  \mkleeneopen{}\mlambda{}x.Ax\mkleeneclose{}\mcdot{}
              THEN  D  -2
              THEN  Try  (Complete  (Auto))
              THEN  (MemCD
                          THEN  Try  (Complete  (Auto))
                          THEN  (All
                                      (RepUR  ``bag-member  bag-deq-member  squash``)\mcdot{}
                                      THEN  ((MemTypeCD  THEN  Auto)  ORELSE  (D  -1  THEN  ExRepD))\mcdot{}
                                      )\mcdot{})\mcdot{})\mcdot{})

---

Home Index