---

Step * of Lemma decidable__exists-iterated-classrel

∀[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)
    ⇒ single-valued-bag(init loc(e);S)
    ⇒ Dec(∃v:S. iterated-classrel(es;S;A;f;init;X;e;v)))
BY
{ ((UnivCD THENA Auto)
   THEN (InstLemma `decidable__exists-single-valued-bag` [⌈S⌉;⌈init loc(e)⌉]⋅ THENA Auto)
   THEN RepeatFor 2 (ParallelLast)
   THEN Try (Complete ((BLemma `iterated-classrel-exists` THEN Auto)))
   THEN (D 0 THENA Auto)
   THEN (RWO "iterated-classrel-exists-iff<" (-1) THENA Auto)
   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{}  single-valued-bag(init  loc(e);S)
        {}\mRightarrow{}  Dec(\mexists{}v:S.  iterated-classrel(es;S;A;f;init;X;e;v)))


By

((UnivCD  THENA  Auto)
  THEN  (InstLemma  `decidable\_\_exists-single-valued-bag`  [\mkleeneopen{}S\mkleeneclose{};\mkleeneopen{}init  loc(e)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  (ParallelLast)
  THEN  Try  (Complete  ((BLemma  `iterated-classrel-exists`  THEN  Auto)))
  THEN  (D  0  THENA  Auto)
  THEN  (RWO  "iterated-classrel-exists-iff<"  (-1)  THENA  Auto)
  THEN  Auto)

---

Home Index