---

Step * 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)
⊢ 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)
BY
{ ((FLemma `assert-isname` [-1] THENA Auto) THEN (GenConclTerm ⌜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. 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)

---

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)
\mvdash{}  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 


By

---

Latex:
((FLemma  `assert-isname`  [-1]  THENA  Auto)  THEN  (GenConclTerm  \mkleeneopen{}f  x\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index