---

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


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))))
5. [I] : Cname List
6. y : nameset([a1 / (map(λp.(fst(p));L) @ I)])
7. ¬(y = a1 ∈ Cname)
8. y ∈ nameset(map(λp.(fst(p));L) @ I)
9. ((↑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)))
⊢ ((↑isname(face-maps-comp(L) y)) ⇒ ((¬(y ∈ [a1 / map(λp.(fst(p));L)])) ∧ ((face-maps-comp(L) y) = y ∈ nameset(I))))
∧ ((¬↑isname(face-maps-comp(L) y))
  ⇒ ((y ∈ [a1 / map(λp.(fst(p));L)])
     ∧ ((face-maps-comp(L) y) = outl(if eqof(CnameDeq) a1 y then inl a2 else apply-alist(CnameDeq;L;y) fi ) ∈ ℕ2)))
BY
{ TACTIC:((Subst' eqof(CnameDeq) a1 y ~ ff 0 THENA (DVar `y' THEN MoveToConcl 8 THEN All Thin THEN Auto))
          THEN Reduce 0
          ) }

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

---

Latex:

---

Latex:

1.  a1  :  Cname
2.  a2  :  \mBbbN{}2
3.  L  :  (Cname  \mtimes{}  \mBbbN{}2)  List
4.  \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))))))
5.  [I]  :  Cname  List
6.  y  :  nameset([a1  /  (map(\mlambda{}p.(fst(p));L)  @  I)])
7.  \mneg{}(y  =  a1)
8.  y  \mmember{}  nameset(map(\mlambda{}p.(fst(p));L)  @  I)
9.  ((\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)))))
\mvdash{}  ((\muparrow{}isname(face-maps-comp(L)  y))
{}\mRightarrow{}  ((\mneg{}(y  \mmember{}  [a1  /  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{}  [a1  /  map(\mlambda{}p.(fst(p));L)])
          \mwedge{}  ((face-maps-comp(L)  y)
              =  outl(if  eqof(CnameDeq)  a1  y  then  inl  a2  else  apply-alist(CnameDeq;L;y)  fi  ))))


By

---

Latex:
TACTIC:((Subst'  eqof(CnameDeq)  a1  y  \msim{}  ff  0
                  THENA  (DVar  `y'  THEN  MoveToConcl  8  THEN  All  Thin  THEN  Auto)
                  )
                THEN  Reduce  0
                )

---

Home Index