---

Step * of Lemma bag_all-cons

∀[T:Type]. ∀[x:T]. ∀[b:bag(T)]. ∀[f:T ⟶ 𝔹].  (bag_all(x.b;f) ~ (f x) ∧b bag_all(b;f))
BY
{ (Auto
   THEN (BagToList (-2) THENA Auto)
   THEN RepUR ``bag_all bag-accum cons-bag`` 0
   THEN GenConclAtAddr [3;2;2]
   THEN (Subst ⌜f[x] ~ f[x] ∧b v⌝ 0⋅ THENA ((Subst ⌜v ~ tt⌝ 0⋅ THENA Auto) THEN RWO "band-btrue" 0 THEN Auto))
   THEN Thin (-1)
   THEN MoveToConcl (-1)
   THEN ListInd (-2)
   THEN Reduce 0
   THEN Auto
   THEN RepUR ``so_apply`` 0
   THEN Try ((RWO "band-btrue" 0 THEN Auto))
   THEN (RWO "band_assoc" 0 THEN Auto)
   THEN BackThruSomeHyp) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[x:T].  \mforall{}[b:bag(T)].  \mforall{}[f:T  {}\mrightarrow{}  \mBbbB{}].    (bag\_all(x.b;f)  \msim{}  (f  x)  \mwedge{}\msubb{}  bag\_all(b;f))


By

---

Latex:
(Auto
  THEN  (BagToList  (-2)  THENA  Auto)
  THEN  RepUR  ``bag\_all  bag-accum  cons-bag``  0
  THEN  GenConclAtAddr  [3;2;2]
  THEN  (Subst  \mkleeneopen{}f[x]  \msim{}  f[x]  \mwedge{}\msubb{}  v\mkleeneclose{}  0\mcdot{}
              THENA  ((Subst  \mkleeneopen{}v  \msim{}  tt\mkleeneclose{}  0\mcdot{}  THENA  Auto)  THEN  RWO  "band-btrue"  0  THEN  Auto)
              )
  THEN  Thin  (-1)
  THEN  MoveToConcl  (-1)
  THEN  ListInd  (-2)
  THEN  Reduce  0
  THEN  Auto
  THEN  RepUR  ``so\_apply``  0
  THEN  Try  ((RWO  "band-btrue"  0  THEN  Auto))
  THEN  (RWO  "band\_assoc"  0  THEN  Auto)
  THEN  BackThruSomeHyp)

---

Home Index