---

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

.....wf..... 
1. L : (Cname × ℕ2) List
2. aaaa : Cname × ℕ2
3. LLLL : (Cname × ℕ2) List
⊢ istype(∀[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)))))
BY
{ (RenameVar `L1' (-1)
   THEN D 0
   THEN ((InstLemma `face-maps-comp_wf` [⌜L1⌝;⌜I⌝]⋅ THENA Auto) ORELSE Auto)
   THEN D 0
   THEN ((GenConclTerm ⌜face-maps-comp(L1) y⌝⋅ THENA Auto) ORELSE Auto)) }

1
1. L : (Cname × ℕ2) List
2. aaaa : Cname × ℕ2
3. L1 : (Cname × ℕ2) List
4. I : Cname List
5. face-maps-comp(L1) ∈ name-morph(map(λp.(fst(p));L1) @ I;I)
6. y : nameset(map(λp.(fst(p));L1) @ I)
7. v : extd-nameset(I)
8. (face-maps-comp(L1) y) = v ∈ extd-nameset(I)
⊢ istype(((↑isname(v)) ⇒ ((¬(y ∈ map(λp.(fst(p));L1))) ∧ (v = y ∈ nameset(I))))
∧ ((¬↑isname(v)) ⇒ ((y ∈ map(λp.(fst(p));L1)) ∧ (v = outl(apply-alist(CnameDeq;L1;y)) ∈ ℕ2))))

---

Latex:

---

Latex:
.....wf..... 
1.  L  :  (Cname  \mtimes{}  \mBbbN{}2)  List
2.  aaaa  :  Cname  \mtimes{}  \mBbbN{}2
3.  LLLL  :  (Cname  \mtimes{}  \mBbbN{}2)  List
\mvdash{}  istype(\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)))))))


By

---

Latex:
(RenameVar  `L1'  (-1)
  THEN  D  0
  THEN  ((InstLemma  `face-maps-comp\_wf`  [\mkleeneopen{}L1\mkleeneclose{};\mkleeneopen{}I\mkleeneclose{}]\mcdot{}  THENA  Auto)  ORELSE  Auto)
  THEN  D  0
  THEN  ((GenConclTerm  \mkleeneopen{}face-maps-comp(L1)  y\mkleeneclose{}\mcdot{}  THENA  Auto)  ORELSE  Auto))

---

Home Index