---

Step * 1 of Lemma name-morph-inv-eq


1. I : Cname List
2. J : Cname List
3. f : name-morph(I;J)
4. x : nameset(I)
5. ↑isname(f x)
6. f x ∈ nameset(J)
7. λi.(isname(f i) ∧b (f i =z f x)) ∈ nameset(I) ⟶ 𝔹
⊢ hd(filter(λi.(isname(f i) ∧b (f i =z f x));I)) = x ∈ nameset(I)
BY
{ (D -4
   THEN (Assert I ∈ nameset(I) List BY
               (Unfold `nameset` 0 THEN Auto))
   THEN (Assert (x ∈ filter(λi.(isname(f i) ∧b (f i =z f x));I)) BY
               (RW ListC 0 THEN Auto THEN Unfold `nameset` 0 THEN Auto))) }

1
1. I : Cname List
2. J : Cname List
3. f : name-morph(I;J)
4. x : Cname
5. (x ∈ I)
6. ↑isname(f x)
7. f x ∈ nameset(J)
8. λi.(isname(f i) ∧b (f i =z f x)) ∈ nameset(I) ⟶ 𝔹
9. I ∈ nameset(I) List
10. (x ∈ filter(λi.(isname(f i) ∧b (f i =z f x));I))
⊢ hd(filter(λi.(isname(f i) ∧b (f i =z f x));I)) = x ∈ nameset(I)

---

Latex:

---

Latex:

1.  I  :  Cname  List
2.  J  :  Cname  List
3.  f  :  name-morph(I;J)
4.  x  :  nameset(I)
5.  \muparrow{}isname(f  x)
6.  f  x  \mmember{}  nameset(J)
7.  \mlambda{}i.(isname(f  i)  \mwedge{}\msubb{}  (f  i  =\msubz{}  f  x))  \mmember{}  nameset(I)  {}\mrightarrow{}  \mBbbB{}
\mvdash{}  hd(filter(\mlambda{}i.(isname(f  i)  \mwedge{}\msubb{}  (f  i  =\msubz{}  f  x));I))  =  x


By

---

Latex:
(D  -4
  THEN  (Assert  I  \mmember{}  nameset(I)  List  BY
                          (Unfold  `nameset`  0  THEN  Auto))
  THEN  (Assert  (x  \mmember{}  filter(\mlambda{}i.(isname(f  i)  \mwedge{}\msubb{}  (f  i  =\msubz{}  f  x));I))  BY
                          (RW  ListC  0  THEN  Auto  THEN  Unfold  `nameset`  0  THEN  Auto)))

---

Home Index