---

Step * 2 of Lemma rec-bind-class_wf

.....upcase..... 
1. Info : Type
2. A : Type
3. B : Type
4. X : A ─→ EClass(B)
5. Y : A ─→ EClass(A)
6. ∀x,a:A. ∀es:EO+(Info). ∀e:E.  (a ∈ Y x(e) ⇒ (∀w:A. (¬w ∈ Y a(e))))
7. n : ℤ
8. 0 < n
9. ∀es:EO+(Info). ∀e:E.  (||≤loc(e)|| < n - 1 ⇒ (∀a:A. (rec-bind-class(X;Y) a es e ∈ bag(B))))
⊢ ∀es:EO+(Info). ∀e:E.  (||≤loc(e)|| < n ⇒ (∀a:A. (rec-bind-class(X;Y) a es e ∈ bag(B))))
BY
{ (UnivCD THENA Auto) }

1
1. Info : Type
2. A : Type
3. B : Type
4. X : A ─→ EClass(B)
5. Y : A ─→ EClass(A)
6. ∀x,a:A. ∀es:EO+(Info). ∀e:E.  (a ∈ Y x(e) ⇒ (∀w:A. (¬w ∈ Y a(e))))
7. n : ℤ
8. 0 < n
9. ∀es:EO+(Info). ∀e:E.  (||≤loc(e)|| < n - 1 ⇒ (∀a:A. (rec-bind-class(X;Y) a es e ∈ bag(B))))
10. es : EO+(Info)@i'
11. e : E@i
12. ||≤loc(e)|| < n@i
13. a : A@i
⊢ rec-bind-class(X;Y) a es e ∈ bag(B)

---

Latex:

---

Latex:
.....upcase..... 
1.  Info  :  Type
2.  A  :  Type
3.  B  :  Type
4.  X  :  A  {}\mrightarrow{}  EClass(B)
5.  Y  :  A  {}\mrightarrow{}  EClass(A)
6.  \mforall{}x,a:A.  \mforall{}es:EO+(Info).  \mforall{}e:E.    (a  \mmember{}  Y  x(e)  {}\mRightarrow{}  (\mforall{}w:A.  (\mneg{}w  \mmember{}  Y  a(e))))
7.  n  :  \mBbbZ{}
8.  0  <  n
9.  \mforall{}es:EO+(Info).  \mforall{}e:E.    (||\mleq{}loc(e)||  <  n  -  1  {}\mRightarrow{}  (\mforall{}a:A.  (rec-bind-class(X;Y)  a  es  e  \mmember{}  bag(B))))
\mvdash{}  \mforall{}es:EO+(Info).  \mforall{}e:E.    (||\mleq{}loc(e)||  <  n  {}\mRightarrow{}  (\mforall{}a:A.  (rec-bind-class(X;Y)  a  es  e  \mmember{}  bag(B))))


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index