---

Step * of Lemma rename-one-name_wf

∀[I:Cname List]. ∀[z1,z2:Cname].
  rename-one-name(z1;z2) ∈ name-morph([z1 / I];[z2 / I]) supposing (¬(z1 ∈ I)) ∧ (¬(z2 ∈ I))
BY
{ (ProveWfLemma THEN MemTypeCD THEN Reduce 0) }

1
1. I : Cname List
2. z1 : Cname
3. z2 : Cname
4. ¬(z1 ∈ I)
5. ¬(z2 ∈ I)
⊢ λx.if eq-cname(x;z1) then z2 else x fi  ∈ nameset([z1 / I]) ⟶ extd-nameset([z2 / I])

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

3
.....wf..... 
1. I : Cname List
2. z1 : Cname
3. z2 : Cname
4. ¬(z1 ∈ I)
5. ¬(z2 ∈ I)
6. f : nameset([z1 / I]) ⟶ extd-nameset([z2 / I])
⊢ istype(∀i,j:nameset([z1 / I]).
           ((↑isname(f i))
           ⇒ (↑isname(f j))
           ⇒ ((f i) = (f j) ∈ extd-nameset([z2 / I]))
           ⇒ (i = j ∈ nameset([z1 / I]))))

---

Latex:

---

Latex:
\mforall{}[I:Cname  List].  \mforall{}[z1,z2:Cname].
    rename-one-name(z1;z2)  \mmember{}  name-morph([z1  /  I];[z2  /  I])  supposing  (\mneg{}(z1  \mmember{}  I))  \mwedge{}  (\mneg{}(z2  \mmember{}  I))


By

---

Latex:
(ProveWfLemma  THEN  MemTypeCD  THEN  Reduce  0)

---

Home Index