---

Step * of Lemma extend-name-morph-comp

No Annotations
∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K). ∀z,v,v1:Cname.
  ((¬(z ∈ I)) ⇒ (¬(v ∈ K)) ⇒ (¬(v1 ∈ J)) ⇒ ((f o g)[z:=v] = (f[z:=v1] o g[v1:=v]) ∈ name-morph([z / I];[v / K])))
BY
{ (Auto
   THEN BLemma `name-morphs-equal`
   THEN Auto
   THEN (FunExt THENA Auto)
   THEN RepUR ``name-comp extend-name-morph uext`` 0
   THEN (BoolCase ⌜eq-cname(x;z)⌝⋅ THENA Auto)) }

1
1. I : Cname List
2. J : Cname List
3. K : Cname List
4. f : name-morph(I;J)
5. g : name-morph(J;K)
6. z : Cname
7. v : Cname
8. v1 : Cname
9. ¬(z ∈ I)
10. ¬(v ∈ K)
11. ¬(v1 ∈ J)
12. x : nameset([z / I])
13. x = z ∈ Cname
⊢ v = if isname(v1) then if eq-cname(v1;v1) then v else g v1 fi  else v1 fi  ∈ extd-nameset([v / K])

2
1. I : Cname List
2. J : Cname List
3. K : Cname List
4. f : name-morph(I;J)
5. g : name-morph(J;K)
6. z : Cname
7. v : Cname
8. v1 : Cname
9. ¬(z ∈ I)
10. ¬(v ∈ K)
11. ¬(v1 ∈ J)
12. x : nameset([z / I])
13. ¬(x = z ∈ Cname)
⊢ if isname(f x) then g (f x) else f x fi 
= if isname(f x) then if eq-cname(f x;v1) then v else g (f x) fi  else f x fi 
∈ extd-nameset([v / K])

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  BLemma  `name-morphs-equal`
  THEN  Auto
  THEN  (FunExt  THENA  Auto)
  THEN  RepUR  ``name-comp  extend-name-morph  uext``  0
  THEN  (BoolCase  \mkleeneopen{}eq-cname(x;z)\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index