---

Step * 1 1 of Lemma name-comp-id-right


1. I : Cname List
2. J : Cname List
3. f : nameset(I) ⟶ extd-nameset(J)
4. ∀i,j:nameset(I).  ((↑isname(f i)) ⇒ (↑isname(f j)) ⇒ ((f i) = (f j) ∈ extd-nameset(J)) ⇒ (i = j ∈ nameset(I)))
⊢ f = (λx.if isname(f x) then f x else f x fi ) ∈ (nameset(I) ⟶ extd-nameset(J))
BY
{ ((Ext THENA Auto) THEN Reduce 0) }

1
1. I : Cname List
2. J : Cname List
3. f : nameset(I) ⟶ extd-nameset(J)
4. ∀i,j:nameset(I).  ((↑isname(f i)) ⇒ (↑isname(f j)) ⇒ ((f i) = (f j) ∈ extd-nameset(J)) ⇒ (i = j ∈ nameset(I)))
5. x : nameset(I)
⊢ (f x) = if isname(f x) then f x else f x fi  ∈ extd-nameset(J)

---

Latex:

---

Latex:

1.  I  :  Cname  List
2.  J  :  Cname  List
3.  f  :  nameset(I)  {}\mrightarrow{}  extd-nameset(J)
4.  \mforall{}i,j:nameset(I).    ((\muparrow{}isname(f  i))  {}\mRightarrow{}  (\muparrow{}isname(f  j))  {}\mRightarrow{}  ((f  i)  =  (f  j))  {}\mRightarrow{}  (i  =  j))
\mvdash{}  f  =  (\mlambda{}x.if  isname(f  x)  then  f  x  else  f  x  fi  )


By

---

Latex:
((Ext  THENA  Auto)  THEN  Reduce  0)

---

Home Index