---

Step * 1 of Lemma assert-bag_all


1. T : Type
2. f : T ⟶ 𝔹
3. b : bag(T)
4. ∀x:T. (x ↓∈ b ⇒ (↑f[x]))
⊢ ↑bag_all(b;f)
BY
{ (MoveToConcl (-1)
   THEN (BagToList (-1) THENA Try (Complete (Auto)))
   THEN ListInd (-1)
   THEN Auto
   THEN Try ((Fold `empty-bag` 0 THEN RWO "bag_all-empty" 0))
   THEN Try (Complete (Auto))
   THEN Fold `cons-bag` 0
   THEN (RWO "bag_all-cons" 0 THENA Auto)
   THEN RW assert_pushdownC 0
   THEN Auto
   THEN Try (Complete ((Unfold `so_apply` (-1)
                        THEN BackThruSomeHyp
                        THEN BagMemberD 0
                        THEN (D 0 THEN Auto)
                        THEN OrLeft
                        THEN Auto)))
   THEN RepeatFor 2 ((BackThruSomeHyp THEN Auto))
   THEN BagMemberD 0
   THEN (D 0 THEN Auto)
   THEN OrRight
   THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
(MoveToConcl  (-1)
  THEN  (BagToList  (-1)  THENA  Try  (Complete  (Auto)))
  THEN  ListInd  (-1)
  THEN  Auto
  THEN  Try  ((Fold  `empty-bag`  0  THEN  RWO  "bag\_all-empty"  0))
  THEN  Try  (Complete  (Auto))
  THEN  Fold  `cons-bag`  0
  THEN  (RWO  "bag\_all-cons"  0  THENA  Auto)
  THEN  RW  assert\_pushdownC  0
  THEN  Auto
  THEN  Try  (Complete  ((Unfold  `so\_apply`  (-1)
                                            THEN  BackThruSomeHyp
                                            THEN  BagMemberD  0
                                            THEN  (D  0  THEN  Auto)
                                            THEN  OrLeft
                                            THEN  Auto)))
  THEN  RepeatFor  2  ((BackThruSomeHyp  THEN  Auto))
  THEN  BagMemberD  0
  THEN  (D  0  THEN  Auto)
  THEN  OrRight
  THEN  Auto)

---

Home Index