---

Step * 1 2 1 2 2 1 2 1 1 of Lemma face-maps-comp-property


1. L : (Cname × ℕ2) List
2. L1 : (Cname × ℕ2) List
3. I : Cname List
4. y : Cname
5. (y ∈ map(λp.(fst(p));L1) @ I)
6. face-maps-comp(L1) ∈ name-morph(map(λp.(fst(p));L1) @ I;I)
7. v : extd-nameset(I)
8. (face-maps-comp(L1) y) = v ∈ extd-nameset(I)
9. ↑isname(v)
10. v ∈ nameset(I)
11. ¬(y ∈ map(λp.(fst(p));L1))
⊢ y ∈ nameset(I)
BY
{ TACTIC:((RW  ListC 5 THENA Auto) THEN D 5) }

1
1. L : (Cname × ℕ2) List
2. L1 : (Cname × ℕ2) List
3. I : Cname List
4. y : Cname
5. (y ∈ map(λp.(fst(p));L1))
6. face-maps-comp(L1) ∈ name-morph(map(λp.(fst(p));L1) @ I;I)
7. v : extd-nameset(I)
8. (face-maps-comp(L1) y) = v ∈ extd-nameset(I)
9. ↑isname(v)
10. v ∈ nameset(I)
11. ¬(y ∈ map(λp.(fst(p));L1))
⊢ y ∈ nameset(I)

2
1. L : (Cname × ℕ2) List
2. L1 : (Cname × ℕ2) List
3. I : Cname List
4. y : Cname
5. (y ∈ I)
6. face-maps-comp(L1) ∈ name-morph(map(λp.(fst(p));L1) @ I;I)
7. v : extd-nameset(I)
8. (face-maps-comp(L1) y) = v ∈ extd-nameset(I)
9. ↑isname(v)
10. v ∈ nameset(I)
11. ¬(y ∈ map(λp.(fst(p));L1))
⊢ y ∈ nameset(I)

---

Latex:

---

Latex:

1.  L  :  (Cname  \mtimes{}  \mBbbN{}2)  List
2.  L1  :  (Cname  \mtimes{}  \mBbbN{}2)  List
3.  I  :  Cname  List
4.  y  :  Cname
5.  (y  \mmember{}  map(\mlambda{}p.(fst(p));L1)  @  I)
6.  face-maps-comp(L1)  \mmember{}  name-morph(map(\mlambda{}p.(fst(p));L1)  @  I;I)
7.  v  :  extd-nameset(I)
8.  (face-maps-comp(L1)  y)  =  v
9.  \muparrow{}isname(v)
10.  v  \mmember{}  nameset(I)
11.  \mneg{}(y  \mmember{}  map(\mlambda{}p.(fst(p));L1))
\mvdash{}  y  \mmember{}  nameset(I)


By

---

Latex:
TACTIC:((RW    ListC  5  THENA  Auto)  THEN  D  5)

---

Home Index