---

Step * 1 2 1 2 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
⊢ ∀y:nameset(map(λp.(fst(p));L1) @ I)
    (((↑isname(face-maps-comp(L1) y)) ⇒ ((¬(y ∈ map(λp.(fst(p));L1))) ∧ ((face-maps-comp(L1) y) = y ∈ nameset(I))))
    ∧ ((¬↑isname(face-maps-comp(L1) y))
      ⇒ ((y ∈ map(λp.(fst(p));L1)) ∧ ((face-maps-comp(L1) y) = outl(apply-alist(CnameDeq;L1;y)) ∈ ℕ2)))) ∈ ℙ
BY
{ TACTIC:MemCD }

1
.....subterm..... T:t
1:n
1. L : (Cname × ℕ2) List
2. L1 : (Cname × ℕ2) List
3. I : Cname List
⊢ nameset(map(λp.(fst(p));L1) @ I) ∈ Type

2
.....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)
⊢ ((↑isname(face-maps-comp(L1) y)) ⇒ ((¬(y ∈ map(λp.(fst(p));L1))) ∧ ((face-maps-comp(L1) y) = y ∈ nameset(I))))
  ∧ ((¬↑isname(face-maps-comp(L1) y))
    ⇒ ((y ∈ map(λp.(fst(p));L1)) ∧ ((face-maps-comp(L1) y) = outl(apply-alist(CnameDeq;L1;y)) ∈ ℕ2))) ∈ ℙ

---

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
\mvdash{}  \mforall{}y:nameset(map(\mlambda{}p.(fst(p));L1)  @  I)
        (((\muparrow{}isname(face-maps-comp(L1)  y))
        {}\mRightarrow{}  ((\mneg{}(y  \mmember{}  map(\mlambda{}p.(fst(p));L1)))  \mwedge{}  ((face-maps-comp(L1)  y)  =  y)))
        \mwedge{}  ((\mneg{}\muparrow{}isname(face-maps-comp(L1)  y))
            {}\mRightarrow{}  ((y  \mmember{}  map(\mlambda{}p.(fst(p));L1))  \mwedge{}  ((face-maps-comp(L1)  y)  =  outl(apply-alist(CnameDeq;L1;y))))))
    \mmember{}  \mBbbP{}


By

---

Latex:
TACTIC:MemCD

---

Home Index