---

Step * 1 1 2 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)
⊢ if isname(f x) then h (f x) else f x fi  = (f x) ∈ extd-nameset(H)
BY
{ (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)
11. ↑isname(f x)
⊢ (h (f x)) = (f x) ∈ 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)
11. ¬False
⊢ (f x) = (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  :  \{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.  \mneg{}\muparrow{}isname(f  x)
\mvdash{}  if  isname(f  x)  then  h  (f  x)  else  f  x  fi    =  (f  x)


By

---

Latex:
(BoolCase  \mkleeneopen{}isname(f  x)\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index