---

Step * of Lemma face-map-property

∀[L:Cname List]
  ∀x:Cname. ∀p:ℕ2. ∀y:nameset([x / L]).
    (((↑isname((x:=p) y)) ⇒ ((¬(y = x ∈ Cname)) ∧ (((x:=p) y) = y ∈ nameset(L))))
    ∧ ((¬↑isname((x:=p) y)) ⇒ ((y = x ∈ Cname) ∧ (((x:=p) y) = p ∈ ℕ2))))
BY
{ ((Intros THEN RepUR ``face-map`` 0) THEN (SplitOnConclITE THENA Auto) THEN Try (HypSubst' (-1) 0)) }

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

2
.....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)))

---

Latex:

---

Latex:
\mforall{}[L:Cname  List]
    \mforall{}x:Cname.  \mforall{}p:\mBbbN{}2.  \mforall{}y:nameset([x  /  L]).
        (((\muparrow{}isname((x:=p)  y))  {}\mRightarrow{}  ((\mneg{}(y  =  x))  \mwedge{}  (((x:=p)  y)  =  y)))
        \mwedge{}  ((\mneg{}\muparrow{}isname((x:=p)  y))  {}\mRightarrow{}  ((y  =  x)  \mwedge{}  (((x:=p)  y)  =  p))))


By

---

Latex:
((Intros  THEN  RepUR  ``face-map``  0)  THEN  (SplitOnConclITE  THENA  Auto)  THEN  Try  (HypSubst'  (-1)  0))

---

Home Index