---

Step * of Lemma bag-member-filter

∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[x:T]. ∀[bs:bag(T)].  uiff(x ↓∈ [x∈bs|P[x]];x ↓∈ bs ∧ (↑P[x]))
BY
{ (Auto
   THEN Try ((DoSubsume THEN Auto THEN Auto))
   THEN ((BagToList 4 THENA (Auto THEN Try ((DoSubsume THEN Auto THEN Auto))))
         THEN All (RepUR ``bag-filter bag-member``)
         THEN Try ((RWO "eqtt_to_assert<" 0 THENA Auto))
         THEN SquashExRepD)⋅) }

1
1. T : Type
2. P : T ⟶ 𝔹
3. x : T
4. bs : T List
5. L : T List
6. L = filter(λx.P[x];bs) ∈ bag(T)
7. (x ∈ L)
⊢ ↓∃L:T List. ((L = bs ∈ bag(T)) ∧ (x ∈ L))

2
1. T : Type
2. P : T ⟶ 𝔹
3. x : T
4. bs : T List
5. L : T List
6. L = filter(λx.P[x];bs) ∈ bag(T)
7. (x ∈ L)
⊢ ↑P[x] ∈ ℙ

3
1. T : Type
2. P : T ⟶ 𝔹
3. x : T
4. bs : T List
5. L : T List
6. L = filter(λx.P[x];bs) ∈ bag(T)
7. (x ∈ L)
⊢ P[x] ∈ 𝔹

4
1. T : Type
2. P : T ⟶ 𝔹
3. x : T
4. bs : T List
5. L : T List
6. L = filter(λx.P[x];bs) ∈ bag(T)
7. (x ∈ L)
⊢ P[x] = tt

5
1. T : Type
2. P : T ⟶ 𝔹
3. x : T
4. bs : T List
5. L : T List
6. L = bs ∈ bag(T)
7. (x ∈ L)
8. ↑P[x]
⊢ ↓∃L:T List. ((L = filter(λx.P[x];bs) ∈ bag(T)) ∧ (x ∈ L))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[x:T].  \mforall{}[bs:bag(T)].    uiff(x  \mdownarrow{}\mmember{}  [x\mmember{}bs|P[x]];x  \mdownarrow{}\mmember{}  bs  \mwedge{}  (\muparrow{}P[x]))


By

---

Latex:
(Auto
  THEN  Try  ((DoSubsume  THEN  Auto  THEN  Auto))
  THEN  ((BagToList  4  THENA  (Auto  THEN  Try  ((DoSubsume  THEN  Auto  THEN  Auto))))
              THEN  All  (RepUR  ``bag-filter  bag-member``)
              THEN  Try  ((RWO  "eqtt\_to\_assert<"  0  THENA  Auto))
              THEN  SquashExRepD)\mcdot{})

---

Home Index