---

Step * 2 1 of Lemma face-map-property


1. L : Cname List
2. x : Cname
3. p : ℕ2
4. y : Cname
5. (y ∈ [x / L])
6. ¬(y = x ∈ ℤ)
7. True
8. ¬(y = x ∈ Cname)
⊢ y ∈ nameset(L)
BY
{ (MemTypeCD THEN Auto) }

1
.....set predicate..... 
1. L : Cname List
2. x : Cname
3. p : ℕ2
4. y : Cname
5. (y ∈ [x / L])
6. ¬(y = x ∈ ℤ)
7. True
8. ¬(y = x ∈ Cname)
⊢ (y ∈ L)

---

Latex:

---

Latex:

1.  L  :  Cname  List
2.  x  :  Cname
3.  p  :  \mBbbN{}2
4.  y  :  Cname
5.  (y  \mmember{}  [x  /  L])
6.  \mneg{}(y  =  x)
7.  True
8.  \mneg{}(y  =  x)
\mvdash{}  y  \mmember{}  nameset(L)


By

---

Latex:
(MemTypeCD  THEN  Auto)

---

Home Index