---

Step * of Lemma State-comb-exists-iff

∀[Info,B,A:Type]. ∀[f:A ─→ B ─→ B]. ∀[init:Id ─→ bag(B)].
  ∀X:EClass(A). ∀[es:EO+(Info)]. ∀[e:E].  uiff(#(init loc(e)) > 0;↓∃v:B. v ∈ State-comb(init;f;X)(e))
BY
{ (UnivCD
   THEN Auto
   THEN Try (Complete ((BLemma `State-comb-exists` THEN Auto)))
   THEN RepeatFor 2 (MoveToConcl (-1))
   THEN VrCausalInd'
   THEN Auto
   THEN TrySquashExRepD (-1)
   THEN RepeatFor 2 (MaUseClassRel (-1))
   THEN Try (Fold `State-comb` (-1))
   THEN BagMemberD (-1)) }

1
1. Info : Type
2. B : Type
3. A : Type
4. f : A ─→ B ─→ B
5. init : Id ─→ bag(B)
6. X : EClass(A)@i'
7. es : EO+(Info)
8. e : E@i
9. ∀e':E. ((e' < e) ⇒ (∃v:B. v ∈ State-comb(init;f;X)(e')) ⇒ 0 < #(init loc(e')))
10. v : B@i
11. (X es e) = {} ∈ bag(A)
12. v ↓∈ Prior(State-comb(init;f;X))?init es e@i
⊢ 0 < #(init loc(e))

2
1. Info : Type
2. B : Type
3. A : Type
4. f : A ─→ B ─→ B
5. init : Id ─→ bag(B)
6. X : EClass(A)@i'
7. es : EO+(Info)
8. e : E@i
9. ∀e':E. ((e' < e) ⇒ (∃v:B. v ∈ State-comb(init;f;X)(e')) ⇒ 0 < #(init loc(e')))
10. v : B@i
11. ¬((X es e) = {} ∈ bag(A))
12. v ↓∈ lifting-2(f) (X es e) (Prior(State-comb(init;f;X))?init es e)@i
⊢ 0 < #(init loc(e))

---

Latex:

---

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


By

---

Latex:
(UnivCD
  THEN  Auto
  THEN  Try  (Complete  ((BLemma  `State-comb-exists`  THEN  Auto)))
  THEN  RepeatFor  2  (MoveToConcl  (-1))
  THEN  VrCausalInd'
  THEN  Auto
  THEN  TrySquashExRepD  (-1)
  THEN  RepeatFor  2  (MaUseClassRel  (-1))
  THEN  Try  (Fold  `State-comb`  (-1))
  THEN  BagMemberD  (-1))

---

Home Index