---

Step * 1 of Lemma name-morph-inv_wf


1. I : Cname List
2. J : Cname List
3. f : name-morph(I;J)
4. x : Cname
5. i : nameset(I)
6. (↑isname(f i)) ∧ ((f i) = x ∈ Cname)
⊢ hd(filter(λi.(isname(f i) ∧b (f i =z x));I)) ∈ nameset(I)
BY
{ Assert ⌜λi.(isname(f i) ∧b (f i =z x)) ∈ nameset(I) ⟶ 𝔹⌝⋅ }

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

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

---

Latex:

---

Latex:

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


By

---

Latex:
Assert  \mkleeneopen{}\mlambda{}i.(isname(f  i)  \mwedge{}\msubb{}  (f  i  =\msubz{}  x))  \mmember{}  nameset(I)  {}\mrightarrow{}  \mBbbB{}\mkleeneclose{}\mcdot{}

---

Home Index