---

Step * 1 of Lemma name-morph-extend-comp


1. I : Cname List
2. J : Cname List
3. K : Cname List
4. f : name-morph(I;J)
5. g : name-morph(J;K)
⊢ ((f o g))+ = ((f)+ o (g)+) ∈ (nameset(I+) ⟶ extd-nameset(K+))
BY
{ (RepUR ``name-comp name-morph-extend compose`` 0
   THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))
   THEN Fold `eq-cname` 0
   THEN EqCD
   THEN Auto
   THEN RepUR ``uext`` 0
   THEN (SplitOnConclITE THENA Auto)) }

1
.....truecase..... 
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. x : nameset(I+)
7. x = fresh-cname(I) ∈ Cname
⊢ fresh-cname(K)
= if isname(fresh-cname(J))
  then if eq-cname(fresh-cname(J);fresh-cname(J)) then fresh-cname(K) else g fresh-cname(J) fi 
  else fresh-cname(J)
  fi 
∈ extd-nameset(K+)

2
.....falsecase..... 
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. x : nameset(I+)
7. ¬(x = fresh-cname(I) ∈ Cname)
⊢ if isname(f x) then g (f x) else f x fi 
= if isname(f x) then if eq-cname(f x;fresh-cname(J)) then fresh-cname(K) else g (f x) fi  else f x fi 
∈ extd-nameset(K+)

---

Latex:

---

Latex:

1.  I  :  Cname  List
2.  J  :  Cname  List
3.  K  :  Cname  List
4.  f  :  name-morph(I;J)
5.  g  :  name-morph(J;K)
\mvdash{}  ((f  o  g))+  =  ((f)+  o  (g)+)


By

---

Latex:
(RepUR  ``name-comp  name-morph-extend  compose``  0
  THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto))
  THEN  Fold  `eq-cname`  0
  THEN  EqCD
  THEN  Auto
  THEN  RepUR  ``uext``  0
  THEN  (SplitOnConclITE  THENA  Auto))

---

Home Index