---

Step * of Lemma iterated_classrel-exists

∀[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) supposing ↓∃s:S. s ↓∈ init loc(e)
BY
{ ((UnivCD THENA Auto)
   THEN RepeatFor 2 (MoveToConcl (-1))
   THEN VrCausalInd'
   THEN (D 0 THENA Auto)
   THEN SquashExRepD
   THEN (Assert ⌈Dec(↑first(e))⌉⋅ THENA Auto)
   THEN D (-1)) }

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)
8. e : E@i
9. ∀e':E. ((e' < e) ⇒ (↓∃s:S. s ↓∈ init loc(e')) ⇒ (↓∃v:S. iterated_classrel(es;S;A;f;init;X;e';v)))
10. s : S@i
11. s ↓∈ init loc(e)@i
12. ↑first(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)
5. f : A ─→ S ─→ S
6. X : EClass(A)
7. es : EO+(Info)
8. e : E@i
9. ∀e':E. ((e' < e) ⇒ (↓∃s:S. s ↓∈ init loc(e')) ⇒ (↓∃v:S. iterated_classrel(es;S;A;f;init;X;e';v)))
10. s : S@i
11. s ↓∈ init loc(e)@i
12. ¬↑first(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].
    \mdownarrow{}\mexists{}v:S.  iterated\_classrel(es;S;A;f;init;X;e;v)  supposing  \mdownarrow{}\mexists{}s:S.  s  \mdownarrow{}\mmember{}  init  loc(e)


By

((UnivCD  THENA  Auto)
  THEN  RepeatFor  2  (MoveToConcl  (-1))
  THEN  VrCausalInd'
  THEN  (D  0  THENA  Auto)
  THEN  SquashExRepD
  THEN  (Assert  \mkleeneopen{}Dec(\muparrow{}first(e))\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  D  (-1))

---

Home Index