---

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


1. L : (Cname × ℕ2) List
2. aaaa : Cname × ℕ2
3. LLLL : (Cname × ℕ2) List
4. ∀[I:Cname List]
     ∀y:nameset(map(λp.(fst(p));LLLL) @ I)
       (((↑isname(face-maps-comp(LLLL) y))
       ⇒ ((¬(y ∈ map(λp.(fst(p));LLLL))) ∧ ((face-maps-comp(LLLL) y) = y ∈ nameset(I))))
       ∧ ((¬↑isname(face-maps-comp(LLLL) y))
         ⇒ ((y ∈ map(λp.(fst(p));LLLL)) ∧ ((face-maps-comp(LLLL) y) = outl(apply-alist(CnameDeq;LLLL;y)) ∈ ℕ2))))
⊢ ∀[I:Cname List]
    ∀y:nameset(map(λp.(fst(p));[aaaa / LLLL]) @ I)
      (((↑isname(face-maps-comp([aaaa / LLLL]) y))
      ⇒ ((¬(y ∈ map(λp.(fst(p));[aaaa / LLLL]))) ∧ ((face-maps-comp([aaaa / LLLL]) y) = y ∈ nameset(I))))
      ∧ ((¬↑isname(face-maps-comp([aaaa / LLLL]) y))
        ⇒ ((y ∈ map(λp.(fst(p));[aaaa / LLLL]))
           ∧ ((face-maps-comp([aaaa / LLLL]) y) = outl(apply-alist(CnameDeq;[aaaa / LLLL];y)) ∈ ℕ2))))
BY
{ (Thin 1 THEN RenameVar `L' (-2) THEN D 1) }

1
1. a1 : Cname
2. a2 : ℕ2
3. L : (Cname × ℕ2) List
4. ∀[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))))
⊢ ∀[I:Cname List]
    ∀y:nameset(map(λp.(fst(p));[<a1, a2> / L]) @ I)
      (((↑isname(face-maps-comp([<a1, a2> / L]) y))
      ⇒ ((¬(y ∈ map(λp.(fst(p));[<a1, a2> / L]))) ∧ ((face-maps-comp([<a1, a2> / L]) y) = y ∈ nameset(I))))
      ∧ ((¬↑isname(face-maps-comp([<a1, a2> / L]) y))
        ⇒ ((y ∈ map(λp.(fst(p));[<a1, a2> / L]))
           ∧ ((face-maps-comp([<a1, a2> / L]) y) = outl(apply-alist(CnameDeq;[<a1, a2> / L];y)) ∈ ℕ2))))

---

Latex:

---

Latex:

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


By

---

Latex:
(Thin  1  THEN  RenameVar  `L'  (-2)  THEN  D  1)

---

Home Index