---

Step * of Lemma iterated-classrel-as-prior

∀[Info,A,S:Type]. ∀[init:Id ─→ bag(S)]. ∀[f:A ─→ S ─→ S]. ∀[X:EClass(A)].
  ∀es:EO+(Info). ∀e:E.
    ∀[v:S]
      (iterated-classrel(es;S;A;f;init;X;e;v)
      ⇐⇒ ∃z:S
           (prior-iterated-classrel(es;A;S;z;X;f;init;e)
           ∧ ((∃a:A. (a ∈ X(e) ∧ (v = (f a z) ∈ S))) ∨ ((∀a:A. (¬a ∈ X(e))) ∧ (v = z ∈ S)))))
BY
{ Auto }

1
1. [Info] : Type
2. [A] : Type
3. [S] : Type
4. [init] : Id ─→ bag(S)
5. [f] : A ─→ S ─→ S
6. [X] : EClass(A)
7. es : EO+(Info)@i'
8. e : E@i
9. [v] : S
10. iterated-classrel(es;S;A;f;init;X;e;v)@i
⊢ ∃z:S
   (prior-iterated-classrel(es;A;S;z;X;f;init;e)
   ∧ ((∃a:A. (a ∈ X(e) ∧ (v = (f a z) ∈ S))) ∨ ((∀a:A. (¬a ∈ X(e))) ∧ (v = z ∈ S))))

2
1. [Info] : Type
2. [A] : Type
3. [S] : Type
4. [init] : Id ─→ bag(S)
5. [f] : A ─→ S ─→ S
6. [X] : EClass(A)
7. es : EO+(Info)@i'
8. e : E@i
9. [v] : S
10. ∃z:S
     (prior-iterated-classrel(es;A;S;z;X;f;init;e)
     ∧ ((∃a:A. (a ∈ X(e) ∧ (v = (f a z) ∈ S))) ∨ ((∀a:A. (¬a ∈ X(e))) ∧ (v = z ∈ S))))@i
⊢ 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.
        \mforall{}[v:S]
            (iterated-classrel(es;S;A;f;init;X;e;v)
            \mLeftarrow{}{}\mRightarrow{}  \mexists{}z:S
                      (prior-iterated-classrel(es;A;S;z;X;f;init;e)
                      \mwedge{}  ((\mexists{}a:A.  (a  \mmember{}  X(e)  \mwedge{}  (v  =  (f  a  z))))  \mvee{}  ((\mforall{}a:A.  (\mneg{}a  \mmember{}  X(e)))  \mwedge{}  (v  =  z)))))


By

Auto

---

Home Index