---

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

.....wf..... 
1. L : (Cname × ℕ2) List
⊢ λL.∀[I:Cname List]
       ∀y:nameset(map(λp.(fst(p));L) @ I)
         (((↑isname(face-maps-comp(L) y)) ⇒ ((¬(y ∈ map(λp.(fst(p));L))) ∧ ((face-maps-comp(L) y) = y ∈ nameset(I))))
         ∧ ((¬↑isname(face-maps-comp(L) y))
           ⇒ ((y ∈ map(λp.(fst(p));L)) ∧ ((face-maps-comp(L) y) = outl(apply-alist(CnameDeq;L;y)) ∈ ℕ2)))) ∈ ((Cname
  × ℕ2) List) ⟶ ℙ
BY
{ TACTIC:MemCD }

1
.....subterm..... T:t
1:n
1. L : (Cname × ℕ2) List
2. L1 : (Cname × ℕ2) List
⊢ ∀[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)))) ∈ ℙ

2
.....eq aux..... 
1. L : (Cname × ℕ2) List
⊢ istype((Cname × ℕ2) List)

---

Latex:

---

Latex:
.....wf..... 
1.  L  :  (Cname  \mtimes{}  \mBbbN{}2)  List
\mvdash{}  \mlambda{}L.\mforall{}[I:Cname  List]
              \mforall{}y:nameset(map(\mlambda{}p.(fst(p));L)  @  I)
                  (((\muparrow{}isname(face-maps-comp(L)  y))
                  {}\mRightarrow{}  ((\mneg{}(y  \mmember{}  map(\mlambda{}p.(fst(p));L)))  \mwedge{}  ((face-maps-comp(L)  y)  =  y)))
                  \mwedge{}  ((\mneg{}\muparrow{}isname(face-maps-comp(L)  y))
                      {}\mRightarrow{}  ((y  \mmember{}  map(\mlambda{}p.(fst(p));L))
                            \mwedge{}  ((face-maps-comp(L)  y)  =  outl(apply-alist(CnameDeq;L;y))))))  \mmember{}  ((Cname  \mtimes{}  \mBbbN{}2)  List)
    {}\mrightarrow{}  \mBbbP{}


By

---

Latex:
TACTIC:MemCD

---

Home Index