---

Step * 2 1 of Lemma name-comp_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. i : nameset(I)
9. j : nameset(I)
⊢ (↑isname(if isname(f i) then g (f i) else f i fi ))
⇒ (↑isname(if isname(f j) then g (f j) else f j fi ))
⇒ (if isname(f i) then g (f i) else f i fi  = if isname(f j) then g (f j) else f j fi  ∈ extd-nameset(K))
⇒ (i = j ∈ nameset(I))
BY
{ (((BoolCase ⌜isname(f i)⌝⋅ THENA Auto) THEN Try ((FLemma `assert-isname`[-1] THENA Auto)))
   THEN (BoolCase ⌜isname(f j)⌝⋅ THENA Auto)
   THEN Try ((FLemma `assert-isname`[-1] THENA Auto))
   THEN Auto) }

1
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. i : nameset(I)
9. j : nameset(I)
10. ↑isname(f i)
11. f i ∈ nameset(J)
12. ↑isname(f j)
13. f j ∈ nameset(J)
14. ↑isname(g (f i))
15. ↑isname(g (f j))
16. (g (f i)) = (g (f j)) ∈ extd-nameset(K)
⊢ i = j ∈ nameset(I)

---

Latex:

---

Latex:

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.  i  :  nameset(I)
9.  j  :  nameset(I)
\mvdash{}  (\muparrow{}isname(if  isname(f  i)  then  g  (f  i)  else  f  i  fi  ))
{}\mRightarrow{}  (\muparrow{}isname(if  isname(f  j)  then  g  (f  j)  else  f  j  fi  ))
{}\mRightarrow{}  (if  isname(f  i)  then  g  (f  i)  else  f  i  fi    =  if  isname(f  j)  then  g  (f  j)  else  f  j  fi  )
{}\mRightarrow{}  (i  =  j)


By

---

Latex:
(((BoolCase  \mkleeneopen{}isname(f  i)\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  Try  ((FLemma  `assert-isname`[-1]  THENA  Auto)))
  THEN  (BoolCase  \mkleeneopen{}isname(f  j)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Try  ((FLemma  `assert-isname`[-1]  THENA  Auto))
  THEN  Auto)

---

Home Index