---

Step * 1 of Lemma face-map-property


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

1
1. L : Cname List
2. x : Cname
3. p : ℕ2
4. y : nameset([x / L])
5. y = x ∈ ℤ
⊢ isname(p) = ff

---

Latex:

---

Latex:

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


By

---

Latex:
(Subst'  isname(p)  \msim{}  ff  0  THEN  Reduce  0  THEN  Auto)

---

Home Index