---

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


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))))
BY
{ InstLemma `list_induction` [⌜Cname × ℕ2⌝;⌜λ2L.∀[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))))⌝]⋅ }

1
.....wf..... 
1. L : (Cname × ℕ2) List
⊢ Cname × ℕ2 ∈ Type

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

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

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

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

1.  L  :  (Cname  \mtimes{}  \mBbbN{}2)  List
\mvdash{}  \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:
InstLemma  `list\_induction`  [\mkleeneopen{}Cname  \mtimes{}  \mBbbN{}2\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}L.\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))))))\mkleeneclose{}]\mcdot{}

---

Home Index