---

Step * of Lemma face-maps-comp-property

∀L:(Cname × ℕ2) List
  ∀[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))))
BY
{ (D 0 THENA Auto) }

1
1. L : (Cname × ℕ2) List
⊢ ∀[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))))

---

Latex:

---

Latex:
\mforall{}L:(Cname  \mtimes{}  \mBbbN{}2)  List
    \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))))))


By

---

Latex:
(D  0  THENA  Auto)

---

Home Index