---

Step * 1 of Lemma swap-names_wf


1. I : Cname List
2. z1 : nameset(I)
3. z2 : nameset(I)
⊢ λx.if eq-cname(x;z1) then z2
     if eq-cname(x;z2) then z1
     else x
     fi  ∈ nameset(I) ⟶ extd-nameset(I)
BY
{ Auto }

---

Latex:

---

Latex:

1.  I  :  Cname  List
2.  z1  :  nameset(I)
3.  z2  :  nameset(I)
\mvdash{}  \mlambda{}x.if  eq-cname(x;z1)  then  z2
          if  eq-cname(x;z2)  then  z1
          else  x
          fi    \mmember{}  nameset(I)  {}\mrightarrow{}  extd-nameset(I)


By

---

Latex:
Auto

---

Home Index