---

Step * of Lemma rec-bind-classrel2

∀[Info,A,B:Type]. ∀[X:A ─→ EClass(B)]. ∀[Y:A ─→ EClass(A)].
  ∀[es:EO+(Info)]. ∀[e:E]. ∀[a:A]. ∀[v:B].
    uiff(v ∈ rec-bind-class(X;Y) a(e);↓v ∈ X a(e)
                                       ∨ (∃a':A. (a' ∈ Y a(e) ∧ v ∈ X a'(e)))
                                       ∨ (∃e':E. ∃a':A. ((e' <loc e) ∧ a' ∈ Y a(e') ∧ v ∈ rec-bind-class(X;Y) a'(e)))) 
  supposing not-self-starting{i:l}(Info;A;Y)
BY
{ (BasicUniformUnivCD Auto
   THEN (Unhide THENA (Auto THEN Try ((RelRST THEN Auto))))
   THEN RepeatFor 3 (MoveToConcl (-1))
   THEN VrCausalInd'
   THEN (UnivCD THENA Auto)
   THEN D 0
   THEN (UnivCD THENA Auto)) }

1
1. Info : Type
2. A : Type
3. B : Type
4. X : A ─→ EClass(B)
5. Y : A ─→ EClass(A)
6. not-self-starting{i:l}(Info;A;Y)
7. es : EO+(Info)
8. e : E@i
9. ∀e':E
     ((e' < e)
     ⇒ (∀a:A. ∀v:B.
           uiff(v ∈ rec-bind-class(X;Y) a(e');↓v ∈ X a(e')
                                               ∨ (∃a':A. (a' ∈ Y a(e') ∧ v ∈ X a'(e')))
                                               ∨ (∃e1:E
                                                   ∃a':A
                                                    ((e1 <loc e') ∧ a' ∈ Y a(e1) ∧ v ∈ rec-bind-class(X;Y) a'(e'))))))
10. a : A@i
11. v : B@i
12. v ∈ rec-bind-class(X;Y) a(e)
⊢ ↓v ∈ X a(e)
   ∨ (∃a':A. (a' ∈ Y a(e) ∧ v ∈ X a'(e)))
   ∨ (∃e':E. ∃a':A. ((e' <loc e) ∧ a' ∈ Y a(e') ∧ v ∈ rec-bind-class(X;Y) a'(e)))

2
1. Info : Type
2. A : Type
3. B : Type
4. X : A ─→ EClass(B)
5. Y : A ─→ EClass(A)
6. not-self-starting{i:l}(Info;A;Y)
7. es : EO+(Info)
8. e : E@i
9. ∀e':E
     ((e' < e)
     ⇒ (∀a:A. ∀v:B.
           uiff(v ∈ rec-bind-class(X;Y) a(e');↓v ∈ X a(e')
                                               ∨ (∃a':A. (a' ∈ Y a(e') ∧ v ∈ X a'(e')))
                                               ∨ (∃e1:E
                                                   ∃a':A
                                                    ((e1 <loc e') ∧ a' ∈ Y a(e1) ∧ v ∈ rec-bind-class(X;Y) a'(e'))))))
10. a : A@i
11. v : B@i
12. ↓v ∈ X a(e)
     ∨ (∃a':A. (a' ∈ Y a(e) ∧ v ∈ X a'(e)))
     ∨ (∃e':E. ∃a':A. ((e' <loc e) ∧ a' ∈ Y a(e') ∧ v ∈ rec-bind-class(X;Y) a'(e)))
⊢ v ∈ rec-bind-class(X;Y) a(e)

---

Latex:

---

Latex:
\mforall{}[Info,A,B:Type].  \mforall{}[X:A  {}\mrightarrow{}  EClass(B)].  \mforall{}[Y:A  {}\mrightarrow{}  EClass(A)].
    \mforall{}[es:EO+(Info)].  \mforall{}[e:E].  \mforall{}[a:A].  \mforall{}[v:B].
        uiff(v  \mmember{}  rec-bind-class(X;Y)  a(e);\mdownarrow{}v  \mmember{}  X  a(e)
                                                                              \mvee{}  (\mexists{}a':A.  (a'  \mmember{}  Y  a(e)  \mwedge{}  v  \mmember{}  X  a'(e)))
                                                                              \mvee{}  (\mexists{}e':E
                                                                                      \mexists{}a':A
                                                                                        ((e'  <loc  e)
                                                                                        \mwedge{}  a'  \mmember{}  Y  a(e')
                                                                                        \mwedge{}  v  \mmember{}  rec-bind-class(X;Y)  a'(e)))) 
    supposing  not-self-starting\{i:l\}(Info;A;Y)


By

---

Latex:
(BasicUniformUnivCD  Auto
  THEN  (Unhide  THENA  (Auto  THEN  Try  ((RelRST  THEN  Auto))))
  THEN  RepeatFor  3  (MoveToConcl  (-1))
  THEN  VrCausalInd'
  THEN  (UnivCD  THENA  Auto)
  THEN  D  0
  THEN  (UnivCD  THENA  Auto))

---

Home Index