---

Step * of Lemma State-loc-comb-non-empty-iff

∀[Info,B,A:Type]. ∀[f:Id ─→ A ─→ B ─→ B]. ∀[init:Id ─→ bag(B)].
  ∀X:EClass(A). ∀es:EO+(Info). ∀e:E.  (¬↑bag-null(init loc(e)) ⇐⇒ ↓∃v:B. v ∈ State-loc-comb(init;f;X)(e))
BY
{ ((UnivCD THENA Auto)
   THEN D 0
   THEN (D 0 THENA Auto)
   THEN Try ((BLemma `State-loc-comb-non-empty` THEN Auto))
   THEN (RWO "State-loc-comb-classrel-non-loc" (-1) THENA Auto)
   THEN RWO "State-comb-exists-iff<" (-1)
   THEN Auto
   THEN RWO "null-bag-size" 0
   THEN Auto
   THEN RW assert_pushdownC 0
   THEN Auto') }

---

Latex:

---

Latex:
\mforall{}[Info,B,A:Type].  \mforall{}[f:Id  {}\mrightarrow{}  A  {}\mrightarrow{}  B  {}\mrightarrow{}  B].  \mforall{}[init:Id  {}\mrightarrow{}  bag(B)].
    \mforall{}X:EClass(A).  \mforall{}es:EO+(Info).  \mforall{}e:E.
        (\mneg{}\muparrow{}bag-null(init  loc(e))  \mLeftarrow{}{}\mRightarrow{}  \mdownarrow{}\mexists{}v:B.  v  \mmember{}  State-loc-comb(init;f;X)(e))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  D  0
  THEN  (D  0  THENA  Auto)
  THEN  Try  ((BLemma  `State-loc-comb-non-empty`  THEN  Auto))
  THEN  (RWO  "State-loc-comb-classrel-non-loc"  (-1)  THENA  Auto)
  THEN  RWO  "State-comb-exists-iff<"  (-1)
  THEN  Auto
  THEN  RWO  "null-bag-size"  0
  THEN  Auto
  THEN  RW  assert\_pushdownC  0
  THEN  Auto')

---

Home Index