---

Step * 2 of Lemma assert-bag_all


1. T : Type
2. f : T ⟶ 𝔹
3. b : bag(T)
4. ↑bag_all(b;f)
5. x : T
6. x ↓∈ b
⊢ ↑f[x]
BY
{ (RepeatFor 3 (MoveToConcl (-1))
   THEN (BagToList (-1) THENA Auto)
   THEN ListInd (-1)
   THEN Try ((Fold `empty-bag` 0 THEN (RWO "bag_all-empty" 0 THENA Auto)))
   THEN Try ((Fold `cons-bag` 0 THEN (RWO "bag_all-cons" 0 THENA Auto)))
   THEN All (RepUR ``so_apply``)
   THEN Auto
   THEN Try (Complete (BagMemberD (-1)))
   THEN skip{BagMemberD (-1)}
   THEN skip{((RW assert_pushdownC (-3) THENA Auto)
              THEN D (-1)
              THEN (Unhide THENA Auto)
              THEN DProdsAndUnions
              THEN Auto)}) }

1
1. T : Type
2. f : T ⟶ 𝔹
3. u : T
4. v : T List
5. ↑bag_all(v;f)
6. x : T
7. x ↓∈ u.v
8. ↑(f u)
9. ∀x:T. (x ↓∈ v ⇒ (↑(f x)))
⊢ ↑(f x)

---

Latex:

---

Latex:

1.  T  :  Type
2.  f  :  T  {}\mrightarrow{}  \mBbbB{}
3.  b  :  bag(T)
4.  \muparrow{}bag\_all(b;f)
5.  x  :  T
6.  x  \mdownarrow{}\mmember{}  b
\mvdash{}  \muparrow{}f[x]


By

---

Latex:
(RepeatFor  3  (MoveToConcl  (-1))
  THEN  (BagToList  (-1)  THENA  Auto)
  THEN  ListInd  (-1)
  THEN  Try  ((Fold  `empty-bag`  0  THEN  (RWO  "bag\_all-empty"  0  THENA  Auto)))
  THEN  Try  ((Fold  `cons-bag`  0  THEN  (RWO  "bag\_all-cons"  0  THENA  Auto)))
  THEN  All  (RepUR  ``so\_apply``)
  THEN  Auto
  THEN  Try  (Complete  (BagMemberD  (-1)))
  THEN  skip\{BagMemberD  (-1)\}
  THEN  skip\{((RW  assert\_pushdownC  (-3)  THENA  Auto)
                        THEN  D  (-1)
                        THEN  (Unhide  THENA  Auto)
                        THEN  DProdsAndUnions
                        THEN  Auto)\})

---

Home Index