---

Step * 2 of Lemma nc-se'-p

.....wf..... 
1. J : fset(ℕ)
2. k : ℕ
3. z : ℕ
4. n : {n:ℕ| ¬n ∈ J} 
5. x : names(J+z)
6. x ≠ z
7. x ∈ names(J)
⊢ x ∈ names(J+k+n)
BY
{ (DoSubsume THEN Auto) }

1
1. J : fset(ℕ)
2. k : ℕ
3. z : ℕ
4. n : {n:ℕ| ¬n ∈ J} 
5. x : names(J+z)
6. x ≠ z
7. x ∈ names(J)
8. x = x ∈ names(J)
⊢ names(J) ⊆r names(J+k+n)

---

Latex:

---

Latex:
.....wf..... 
1.  J  :  fset(\mBbbN{})
2.  k  :  \mBbbN{}
3.  z  :  \mBbbN{}
4.  n  :  \{n:\mBbbN{}|  \mneg{}n  \mmember{}  J\} 
5.  x  :  names(J+z)
6.  x  \mneq{}  z
7.  x  \mmember{}  names(J)
\mvdash{}  x  \mmember{}  names(J+k+n)


By

---

Latex:
(DoSubsume  THEN  Auto)

---

Home Index