---

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)) }

1
1. [Info] : Type
2. [A] : Type
3. [S] : Type
4. init : Id ─→ bag(S)@i
5. f : A ─→ S ─→ S@i
6. X : EClass(A)@i'
7. es : EO+(Info)@i'
8. e : E@i
9. single-valued-classrel(es;X;A)@i
10. single-valued-bag(init loc(e);S)@i
11. ∃v:S. v ↓∈ init loc(e)
⊢ ∃v:S. iterated_classrel(es;S;A;f;init;X;e;v)

2
1. [Info] : Type
2. [A] : Type
3. [S] : Type
4. init : Id ─→ bag(S)@i
5. f : A ─→ S ─→ S@i
6. X : EClass(A)@i'
7. es : EO+(Info)@i'
8. e : E@i
9. single-valued-classrel(es;X;A)@i
10. single-valued-bag(init loc(e);S)@i
11. ¬(∃v:S. v ↓∈ init loc(e))
⊢ ¬(∃v:S. iterated_classrel(es;S;A;f;init;X;e;v))

---

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))

---

Home Index