---

Step * of Lemma extend-name-morph-rename-one

No Annotations
∀I,K:Cname List. ∀f:name-morph(I;K). ∀z,z1,v:Cname.
  ((¬(z1 ∈ I))
  ⇒ (¬(z ∈ I))
  ⇒ (¬(v ∈ K))
  ⇒ (f[z:=v] = (rename-one-name(z;z1) o f[z1:=v]) ∈ name-morph([z / I];[v / K])))
BY
{ (Auto THEN BLemma `name-morphs-equal` THEN Auto) }

1
.....wf..... 
1. I : Cname List
2. K : Cname List
3. f : name-morph(I;K)
4. z : Cname
5. z1 : Cname
6. v : Cname
7. ¬(z1 ∈ I)
8. ¬(z ∈ I)
9. ¬(v ∈ K)
⊢ (rename-one-name(z;z1) o f[z1:=v]) ∈ nameset([z / I]) ⟶ extd-nameset([v / K])

2
1. I : Cname List
2. K : Cname List
3. f : name-morph(I;K)
4. z : Cname
5. z1 : Cname
6. v : Cname
7. ¬(z1 ∈ I)
8. ¬(z ∈ I)
9. ¬(v ∈ K)
⊢ f[z:=v] = (rename-one-name(z;z1) o f[z1:=v]) ∈ (nameset([z / I]) ⟶ extd-nameset([v / K]))

---

Latex:

---

Latex:
No  Annotations
\mforall{}I,K:Cname  List.  \mforall{}f:name-morph(I;K).  \mforall{}z,z1,v:Cname.
    ((\mneg{}(z1  \mmember{}  I))  {}\mRightarrow{}  (\mneg{}(z  \mmember{}  I))  {}\mRightarrow{}  (\mneg{}(v  \mmember{}  K))  {}\mRightarrow{}  (f[z:=v]  =  (rename-one-name(z;z1)  o  f[z1:=v])))


By

---

Latex:
(Auto  THEN  BLemma  `name-morphs-equal`  THEN  Auto)

---

Home Index