---

Step * 2 of Lemma face-map-property

.....falsecase..... 
1. [L] : Cname List
2. x : Cname
3. p : ℕ2
4. y : nameset([x / L])
5. ¬(y = x ∈ ℤ)
⊢ ((↑isname(y)) ⇒ ((¬(y = x ∈ Cname)) ∧ (y = y ∈ nameset(L)))) ∧ ((¬↑isname(y)) ⇒ ((y = x ∈ Cname) ∧ (y = p ∈ ℕ2)))
BY
{ (DVar `y' THEN Subst' isname(y) ~ tt 0 THEN Reduce 0 THEN Auto) }

1
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)

---

Latex:

---

Latex:
.....falsecase..... 
1.  [L]  :  Cname  List
2.  x  :  Cname
3.  p  :  \mBbbN{}2
4.  y  :  nameset([x  /  L])
5.  \mneg{}(y  =  x)
\mvdash{}  ((\muparrow{}isname(y))  {}\mRightarrow{}  ((\mneg{}(y  =  x))  \mwedge{}  (y  =  y)))  \mwedge{}  ((\mneg{}\muparrow{}isname(y))  {}\mRightarrow{}  ((y  =  x)  \mwedge{}  (y  =  p)))


By

---

Latex:
(DVar  `y'  THEN  Subst'  isname(y)  \msim{}  tt  0  THEN  Reduce  0  THEN  Auto)

---

Home Index