---

Step * 1 1 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 : {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)
11. f x ∈ nameset(J)
12. v : nameset(J)
13. (f x) = v ∈ nameset(J)
⊢ if isname(g v) then h (g v) else g v fi  = if isname(g v) then h (g v) else g v fi  ∈ extd-nameset(H)
BY
{ Subst' if isname(g v) then h (g v) else g v fi  ~ uext(h) (g v) 0 }

1
.....equality..... 
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)
11. f x ∈ nameset(J)
12. v : nameset(J)
13. (f x) = v ∈ nameset(J)
⊢ if isname(g v) then h (g v) else g v fi  ~ uext(h) (g v)

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)
11. f x ∈ nameset(J)
12. v : nameset(J)
13. (f x) = v ∈ nameset(J)
⊢ (uext(h) (g v)) = (uext(h) (g v)) ∈ extd-nameset(H)

---

Latex:

---

Latex:

1.  I  :  Cname  List
2.  J  :  Cname  List
3.  K  :  Cname  List
4.  H  :  Cname  List
5.  f  :  \{f:nameset(I)  {}\mrightarrow{}  extd-nameset(J)| 
                \mforall{}i,j:nameset(I).    ((\muparrow{}isname(f  i))  {}\mRightarrow{}  (\muparrow{}isname(f  j))  {}\mRightarrow{}  ((f  i)  =  (f  j))  {}\mRightarrow{}  (i  =  j))\} 
6.  g  :  \{f:nameset(J)  {}\mrightarrow{}  extd-nameset(K)| 
                \mforall{}i,j:nameset(J).    ((\muparrow{}isname(f  i))  {}\mRightarrow{}  (\muparrow{}isname(f  j))  {}\mRightarrow{}  ((f  i)  =  (f  j))  {}\mRightarrow{}  (i  =  j))\} 
7.  h  :  \{f:nameset(K)  {}\mrightarrow{}  extd-nameset(H)| 
                \mforall{}i,j:nameset(K).    ((\muparrow{}isname(f  i))  {}\mRightarrow{}  (\muparrow{}isname(f  j))  {}\mRightarrow{}  ((f  i)  =  (f  j))  {}\mRightarrow{}  (i  =  j))\} 
8.  ((f  o  g)  o  h)  =  ((f  o  g)  o  h)
9.  x  :  nameset(I)
10.  \muparrow{}isname(f  x)
11.  f  x  \mmember{}  nameset(J)
12.  v  :  nameset(J)
13.  (f  x)  =  v
\mvdash{}  if  isname(g  v)  then  h  (g  v)  else  g  v  fi    =  if  isname(g  v)  then  h  (g  v)  else  g  v  fi 


By

---

Latex:
Subst'  if  isname(g  v)  then  h  (g  v)  else  g  v  fi    \msim{}  uext(h)  (g  v)  0

---

Home Index