---

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

.....antecedent..... 
1. L : (Cname × ℕ2) List
⊢ ∀aaaa:Cname × ℕ2. ∀LLLL:(Cname × ℕ2) List.
    ((∀[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
{ (RepeatFor 2 ((D 0 THENA Auto)) THEN D 0) }

1
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))))

2
.....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)))))

---

Latex:

---

Latex:
.....antecedent..... 
1.  L  :  (Cname  \mtimes{}  \mBbbN{}2)  List
\mvdash{}  \mforall{}aaaa:Cname  \mtimes{}  \mBbbN{}2.  \mforall{}LLLL:(Cname  \mtimes{}  \mBbbN{}2)  List.
        ((\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)))))))
        {}\mRightarrow{}  (\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:
(RepeatFor  2  ((D  0  THENA  Auto))  THEN  D  0)

---

Home Index