---

Step * of Lemma rename-one-comp

No Annotations
∀I:Cname List. ∀z,z1,z2:Cname.
  (rename-one-name(z;z1) o rename-one-name(z1;z2)) = rename-one-name(z;z2) ∈ name-morph([z / I];[z2 / I]) 
  supposing (¬(z2 ∈ I)) ∧ (¬(z1 ∈ I)) ∧ (¬(z ∈ I))
BY
{ (Auto THEN TACTIC:(Symmetry THEN BLemma `name-morphs-equal` THEN Auto)) }

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

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

---

Latex:

---

Latex:
No  Annotations
\mforall{}I:Cname  List.  \mforall{}z,z1,z2:Cname.
    (rename-one-name(z;z1)  o  rename-one-name(z1;z2))  =  rename-one-name(z;z2) 
    supposing  (\mneg{}(z2  \mmember{}  I))  \mwedge{}  (\mneg{}(z1  \mmember{}  I))  \mwedge{}  (\mneg{}(z  \mmember{}  I))


By

---

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

---

Home Index