---

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

.....antecedent..... 
1. L : (Cname × ℕ2) List
⊢ ∀[I:Cname List]
    ∀y:nameset(map(λp.(fst(p));[]) @ I)
      (((↑isname(face-maps-comp([]) y)) ⇒ ((¬(y ∈ map(λp.(fst(p));[]))) ∧ ((face-maps-comp([]) y) = y ∈ nameset(I))))
      ∧ ((¬↑isname(face-maps-comp([]) y))
        ⇒ ((y ∈ map(λp.(fst(p));[])) ∧ ((face-maps-comp([]) y) = outl(apply-alist(CnameDeq;[];y)) ∈ ℕ2))))
BY
{ TACTIC:(RepUR ``face-maps-comp`` 0 THEN Auto THEN (Assert y ∈ extd-nameset(I) BY Auto) THEN Auto) }

1
1. L : (Cname × ℕ2) List
2. [I] : Cname List
3. y : nameset(I)
4. (↑isname(y)) ⇒ ((¬(y ∈ [])) ∧ (y = y ∈ nameset(I)))
5. ¬↑isname(y)
6. y ∈ extd-nameset(I)
⊢ (y ∈ [])

---

Latex:

---

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


By

---

Latex:
TACTIC:(RepUR  ``face-maps-comp``  0  THEN  Auto  THEN  (Assert  y  \mmember{}  extd-nameset(I)  BY  Auto)  THEN  Auto)

---

Home Index