---

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


1. L : (Cname × ℕ2) List
2. aaaa : Cname × ℕ2
3. L1 : (Cname × ℕ2) List
4. I : Cname List
5. face-maps-comp(L1) ∈ name-morph(map(λp.(fst(p));L1) @ I;I)
6. y : nameset(map(λp.(fst(p));L1) @ I)
7. v : extd-nameset(I)
8. (face-maps-comp(L1) y) = v ∈ extd-nameset(I)
⊢ istype(((↑isname(v)) ⇒ ((¬(y ∈ map(λp.(fst(p));L1))) ∧ (v = y ∈ nameset(I))))
∧ ((¬↑isname(v)) ⇒ ((y ∈ map(λp.(fst(p));L1)) ∧ (v = outl(apply-alist(CnameDeq;L1;y)) ∈ ℕ2))))
BY
{ (RepeatFor 2 (D 0) THEN Try ((FLemma `assert-isname` [-1] THEN Auto))) }

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

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

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

---

Latex:

---

Latex:

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


By

---

Latex:
(RepeatFor  2  (D  0)  THEN  Try  ((FLemma  `assert-isname`  [-1]  THEN  Auto)))

---

Home Index