---

Step * 2 of Lemma rec-bind-classrel2


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)
BY
{ (RecUnfold `rec-bind-class` 0
   THEN Reduce 0
   THEN MaUseClassRel 0
   THEN Auto
   THEN (D 0 THEN Auto)
   THEN (OrRight THENA Auto)
   THEN MaUseClassRel 0) }

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. a' : A
13. a' ∈ Y a(e)
14. v ∈ X a'(e)
⊢ ↓∃e':{e':E| e' ≤loc e } . ∃x:A. (x ∈ Y a(e') ∧ v ∈ rec-bind-class(X;Y) x(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. e' : E
13. a' : A
14. (e' <loc e)
15. a' ∈ Y a(e')
16. v ∈ rec-bind-class(X;Y) a'(e)
⊢ ↓∃e':{e':E| e' ≤loc e } . ∃x:A. (x ∈ Y a(e') ∧ v ∈ rec-bind-class(X;Y) x(e))

---

Latex:

---

Latex:

1.  Info  :  Type
2.  A  :  Type
3.  B  :  Type
4.  X  :  A  {}\mrightarrow{}  EClass(B)
5.  Y  :  A  {}\mrightarrow{}  EClass(A)
6.  not-self-starting\{i:l\}(Info;A;Y)
7.  es  :  EO+(Info)
8.  e  :  E@i
9.  \mforall{}e':E
          ((e'  <  e)
          {}\mRightarrow{}  (\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{}e1:E
                                                                                                      \mexists{}a':A
                                                                                                        ((e1  <loc  e')
                                                                                                        \mwedge{}  a'  \mmember{}  Y  a(e1)
                                                                                                        \mwedge{}  v  \mmember{}  rec-bind-class(X;Y)  a'(e'))))))
10.  a  :  A@i
11.  v  :  B@i
12.  \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)))
\mvdash{}  v  \mmember{}  rec-bind-class(X;Y)  a(e)


By

---

Latex:
(RecUnfold  `rec-bind-class`  0
  THEN  Reduce  0
  THEN  MaUseClassRel  0
  THEN  Auto
  THEN  (D  0  THEN  Auto)
  THEN  (OrRight  THENA  Auto)
  THEN  MaUseClassRel  0)

---

Home Index