---

Step * of Lemma swap-names_wf

∀[I:Cname List]. ∀[z1,z2:nameset(I)].  (swap-names(z1;z2) ∈ name-morph(I;I))
BY
{ (ProveWfLemma THEN MemTypeCD THEN Reduce 0) }

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

2
1. I : Cname List
2. z1 : nameset(I)
3. z2 : nameset(I)
⊢ ∀i,j:nameset(I).
    ((↑isname(if eq-cname(i;z1) then z2
     if eq-cname(i;z2) then z1
     else i
     fi ))
    ⇒ (↑isname(if eq-cname(j;z1) then z2
       if eq-cname(j;z2) then z1
       else j
       fi ))
    ⇒ (if eq-cname(i;z1) then z2
       if eq-cname(i;z2) then z1
       else i
       fi 
       = if eq-cname(j;z1) then z2
         if eq-cname(j;z2) then z1
         else j
         fi 
       ∈ extd-nameset(I))
    ⇒ (i = j ∈ nameset(I)))

3
.....wf..... 
1. I : Cname List
2. z1 : nameset(I)
3. z2 : nameset(I)
4. f : nameset(I) ⟶ extd-nameset(I)
⊢ ∀i,j:nameset(I).  ((↑isname(f i)) ⇒ (↑isname(f j)) ⇒ ((f i) = (f j) ∈ extd-nameset(I)) ⇒ (i = j ∈ nameset(I)))
  ∈ Type

---

Latex:

---

Latex:
\mforall{}[I:Cname  List].  \mforall{}[z1,z2:nameset(I)].    (swap-names(z1;z2)  \mmember{}  name-morph(I;I))


By

---

Latex:
(ProveWfLemma  THEN  MemTypeCD  THEN  Reduce  0)

---

Home Index