---

Step * 1 1 of Lemma name-comp-assoc


1. I : Cname List
2. J : Cname List
3. K : Cname List
4. H : Cname List
5. f : name-morph(I;J)
6. g : name-morph(J;K)
7. h : name-morph(K;H)
8. ((f o g) o h) = ((f o g) o h) ∈ (nameset(I) ⟶ extd-nameset(H))
⊢ ((f o g) o h) = (f o (g o h)) ∈ (nameset(I) ⟶ extd-nameset(H))
BY
{ (Auto
   THEN All
   (Unfold `name-morph`)⋅
   THEN RepUR ``name-comp id-morph compose uext name-morph`` 0
   THEN (Ext THENA Auto)
   THEN Reduce 0
   THEN (BoolCase ⌜isname(f x)⌝⋅ THENA Auto)) }

1
1. I : Cname List
2. J : Cname List
3. K : Cname List
4. H : Cname List
5. f : {f:nameset(I) ⟶ extd-nameset(J)| 
        ∀i,j:nameset(I).
          ((↑isname(f i)) ⇒ (↑isname(f j)) ⇒ ((f i) = (f j) ∈ extd-nameset(J)) ⇒ (i = j ∈ nameset(I)))} 
6. g : {f:nameset(J) ⟶ extd-nameset(K)| 
        ∀i,j:nameset(J).
          ((↑isname(f i)) ⇒ (↑isname(f j)) ⇒ ((f i) = (f j) ∈ extd-nameset(K)) ⇒ (i = j ∈ nameset(J)))} 
7. h : {f:nameset(K) ⟶ extd-nameset(H)| 
        ∀i,j:nameset(K).
          ((↑isname(f i)) ⇒ (↑isname(f j)) ⇒ ((f i) = (f j) ∈ extd-nameset(H)) ⇒ (i = j ∈ nameset(K)))} 
8. ((f o g) o h) = ((f o g) o h) ∈ (nameset(I) ⟶ extd-nameset(H))
9. x : nameset(I)
10. ↑isname(f x)
⊢ if isname(g (f x)) then h (g (f x)) else g (f x) fi 
= if isname(g (f x)) then h (g (f x)) else g (f x) fi 
∈ extd-nameset(H)

2
1. I : Cname List
2. J : Cname List
3. K : Cname List
4. H : Cname List
5. f : {f:nameset(I) ⟶ extd-nameset(J)| 
        ∀i,j:nameset(I).
          ((↑isname(f i)) ⇒ (↑isname(f j)) ⇒ ((f i) = (f j) ∈ extd-nameset(J)) ⇒ (i = j ∈ nameset(I)))} 
6. g : {f:nameset(J) ⟶ extd-nameset(K)| 
        ∀i,j:nameset(J).
          ((↑isname(f i)) ⇒ (↑isname(f j)) ⇒ ((f i) = (f j) ∈ extd-nameset(K)) ⇒ (i = j ∈ nameset(J)))} 
7. h : {f:nameset(K) ⟶ extd-nameset(H)| 
        ∀i,j:nameset(K).
          ((↑isname(f i)) ⇒ (↑isname(f j)) ⇒ ((f i) = (f j) ∈ extd-nameset(H)) ⇒ (i = j ∈ nameset(K)))} 
8. ((f o g) o h) = ((f o g) o h) ∈ (nameset(I) ⟶ extd-nameset(H))
9. x : nameset(I)
10. ¬↑isname(f x)
⊢ if isname(f x) then h (f x) else f x fi  = (f x) ∈ extd-nameset(H)

---

Latex:

---

Latex:

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


By

---

Latex:
(Auto
  THEN  All
  (Unfold  `name-morph`)\mcdot{}
  THEN  RepUR  ``name-comp  id-morph  compose  uext  name-morph``  0
  THEN  (Ext  THENA  Auto)
  THEN  Reduce  0
  THEN  (BoolCase  \mkleeneopen{}isname(f  x)\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index