---

Step * 1 of Lemma rec-bind-class_wf

.....basecase..... 
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 : ℤ
⊢ ∀es:EO+(Info). ∀e:E.  (||≤loc(e)|| < 0 ⇒ (∀a:A. (rec-bind-class(X;Y) a es e ∈ bag(B))))
BY
{ Auto' }

---

Latex:

---

Latex:
.....basecase..... 
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{}
\mvdash{}  \mforall{}es:EO+(Info).  \mforall{}e:E.    (||\mleq{}loc(e)||  <  0  {}\mRightarrow{}  (\mforall{}a:A.  (rec-bind-class(X;Y)  a  es  e  \mmember{}  bag(B))))


By

---

Latex:
Auto'

---

Home Index