---

Step * 1 of Lemma iterated-classrel-as-prior


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))))
BY
{ (RecUnfold `iterated-classrel` (-1)
   THEN ParallelLast
   THEN Auto
   THEN Unfold `prior-iterated-classrel` 0
   THEN (SplitOnHypITE (-2) THENA Auto)
   THEN Try (Complete ((OrLeft THEN Auto)))
   THEN Try (Complete ((OrRight THEN Auto)))) }

---

Latex:



1.  [Info]  :  Type
2.  [A]  :  Type
3.  [S]  :  Type
4.  [init]  :  Id  {}\mrightarrow{}  bag(S)
5.  [f]  :  A  {}\mrightarrow{}  S  {}\mrightarrow{}  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
\mvdash{}  \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

(RecUnfold  `iterated-classrel`  (-1)
  THEN  ParallelLast
  THEN  Auto
  THEN  Unfold  `prior-iterated-classrel`  0
  THEN  (SplitOnHypITE  (-2)  THENA  Auto)
  THEN  Try  (Complete  ((OrLeft  THEN  Auto)))
  THEN  Try  (Complete  ((OrRight  THEN  Auto))))

---

Home Index