---

Step * 3 of Lemma name-comp_wf

.....wf..... 
1. I : Cname List
2. J : Cname List
3. K : Cname List
4. f : nameset(I) ⟶ extd-nameset(J)
5. ∀i,j:nameset(I).  ((↑isname(f i)) ⇒ (↑isname(f j)) ⇒ ((f i) = (f j) ∈ extd-nameset(J)) ⇒ (i = j ∈ nameset(I)))
6. g : nameset(J) ⟶ extd-nameset(K)
7. ∀i,j:nameset(J).  ((↑isname(g i)) ⇒ (↑isname(g j)) ⇒ ((g i) = (g j) ∈ extd-nameset(K)) ⇒ (i = j ∈ nameset(J)))
8. f1 : nameset(I) ⟶ extd-nameset(K)
⊢ ∀i,j:nameset(I).  ((↑isname(f1 i)) ⇒ (↑isname(f1 j)) ⇒ ((f1 i) = (f1 j) ∈ extd-nameset(K)) ⇒ (i = j ∈ nameset(I)))
  ∈ Type
BY
{ Auto }

---

Latex:

---

Latex:
.....wf..... 
1.  I  :  Cname  List
2.  J  :  Cname  List
3.  K  :  Cname  List
4.  f  :  nameset(I)  {}\mrightarrow{}  extd-nameset(J)
5.  \mforall{}i,j:nameset(I).    ((\muparrow{}isname(f  i))  {}\mRightarrow{}  (\muparrow{}isname(f  j))  {}\mRightarrow{}  ((f  i)  =  (f  j))  {}\mRightarrow{}  (i  =  j))
6.  g  :  nameset(J)  {}\mrightarrow{}  extd-nameset(K)
7.  \mforall{}i,j:nameset(J).    ((\muparrow{}isname(g  i))  {}\mRightarrow{}  (\muparrow{}isname(g  j))  {}\mRightarrow{}  ((g  i)  =  (g  j))  {}\mRightarrow{}  (i  =  j))
8.  f1  :  nameset(I)  {}\mrightarrow{}  extd-nameset(K)
\mvdash{}  \mforall{}i,j:nameset(I).    ((\muparrow{}isname(f1  i))  {}\mRightarrow{}  (\muparrow{}isname(f1  j))  {}\mRightarrow{}  ((f1  i)  =  (f1  j))  {}\mRightarrow{}  (i  =  j))  \mmember{}  Type


By

---

Latex:
Auto

---

Home Index