---

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

.....subterm..... T:t
2:n
1. L : (Cname × ℕ2) List
2. L1 : (Cname × ℕ2) List
3. I : Cname List
4. y : nameset(map(λp.(fst(p));L1) @ I)
5. face-maps-comp(L1) ∈ name-morph(map(λp.(fst(p));L1) @ I;I)
6. v : extd-nameset(I)
7. (face-maps-comp(L1) y) = v ∈ extd-nameset(I)
8. ¬↑isname(v)
⊢ (y ∈ map(λp.(fst(p));L1)) ∧ (v = outl(apply-alist(CnameDeq;L1;y)) ∈ ℕ2) ∈ ℙ
BY
{ TACTIC:AndMemCD }

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

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

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
1.  L  :  (Cname  \mtimes{}  \mBbbN{}2)  List
2.  L1  :  (Cname  \mtimes{}  \mBbbN{}2)  List
3.  I  :  Cname  List
4.  y  :  nameset(map(\mlambda{}p.(fst(p));L1)  @  I)
5.  face-maps-comp(L1)  \mmember{}  name-morph(map(\mlambda{}p.(fst(p));L1)  @  I;I)
6.  v  :  extd-nameset(I)
7.  (face-maps-comp(L1)  y)  =  v
8.  \mneg{}\muparrow{}isname(v)
\mvdash{}  (y  \mmember{}  map(\mlambda{}p.(fst(p));L1))  \mwedge{}  (v  =  outl(apply-alist(CnameDeq;L1;y)))  \mmember{}  \mBbbP{}


By

---

Latex:
TACTIC:AndMemCD

---

Home Index