---

Step * 2 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. ∃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)
BY
{ (RecUnfold `iterated-classrel` 0
   THEN ExRepD
   THEN (InstConcl [⌈z⌉]⋅ THENA Auto)
   THEN OldAutoSplit
   THEN UnfoldTopAb (-3)
   THEN SplitOrHyps
   THEN 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.  \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))))@i
\mvdash{}  iterated-classrel(es;S;A;f;init;X;e;v)


By

(RecUnfold  `iterated-classrel`  0
  THEN  ExRepD
  THEN  (InstConcl  [\mkleeneopen{}z\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  OldAutoSplit
  THEN  UnfoldTopAb  (-3)
  THEN  SplitOrHyps
  THEN  Auto
  THEN  Try  (Complete  ((OrLeft  THEN  Auto)))
  THEN  Try  (Complete  ((OrRight  THEN  Auto))))

---

Home Index