---

Step * of Lemma iterated-classrel-exists-iff

∀[Info,A,S:Type]. ∀[init:Id ─→ bag(S)].
  ∀f:A ─→ S ─→ S. ∀X:EClass(A). ∀es:EO+(Info). ∀e:E.
    (single-valued-classrel(es;X;A) ⇒ (∃s:S. s ↓∈ init loc(e) ⇐⇒ ∃v:S. iterated-classrel(es;S;A;f;init;X;e;v)))
BY
{ (UnivCD
   THEN Auto
   THEN Try (Complete ((BLemma `iterated-classrel-exists` THEN Auto)))
   THEN MoveToConcl (-3)
   THEN StrongCausalInd
   THEN Auto
   THEN ExRepD
   THEN RecUnfold `iterated-classrel` (-1)
   THEN ExRepD
   THEN (SplitOnHypITE (-2) THENA Auto)
   THEN Try (Complete ((D (-2) THEN Auto)))
   THEN (InstHyp [⌈pred(e)⌉] (-6)⋅ THENA Auto)
   THEN ExRepD
   THEN InstConcl [⌈s⌉]⋅
   THEN Auto) }

---

Latex:


\mforall{}[Info,A,S:Type].  \mforall{}[init:Id  {}\mrightarrow{}  bag(S)].
    \mforall{}f:A  {}\mrightarrow{}  S  {}\mrightarrow{}  S.  \mforall{}X:EClass(A).  \mforall{}es:EO+(Info).  \mforall{}e:E.
        (single-valued-classrel(es;X;A)
        {}\mRightarrow{}  (\mexists{}s:S.  s  \mdownarrow{}\mmember{}  init  loc(e)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}v:S.  iterated-classrel(es;S;A;f;init;X;e;v)))


By

(UnivCD
  THEN  Auto
  THEN  Try  (Complete  ((BLemma  `iterated-classrel-exists`  THEN  Auto)))
  THEN  MoveToConcl  (-3)
  THEN  StrongCausalInd
  THEN  Auto
  THEN  ExRepD
  THEN  RecUnfold  `iterated-classrel`  (-1)
  THEN  ExRepD
  THEN  (SplitOnHypITE  (-2)  THENA  Auto)
  THEN  Try  (Complete  ((D  (-2)  THEN  Auto)))
  THEN  (InstHyp  [\mkleeneopen{}pred(e)\mkleeneclose{}]  (-6)\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  InstConcl  [\mkleeneopen{}s\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index