---

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

.....equality..... 
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)
⊢ ((a1:=a2) o face-maps-comp(L)) y ~ face-maps-comp(L) y
BY
{ (RepUR ``name-comp uext face-map`` 0
   THEN (BoolCase ⌜(y =z a1)⌝⋅ THENA Auto)
   THEN Try (Trivial)
   THEN Assert ⌜↑isname(y)⌝⋅) }

1
.....assertion..... 
1. a1 : ℤ
2. 2 ≤ a1
3. a2 : ℤ
4. 0 ≤ a2
5. a2 < 2
6. L : (Cname × ℕ2) List
7. ∀[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))))
8. I : Cname List
9. y : ℤ
10. 2 ≤ y
11. (y ∈ [a1 / (map(λp.(fst(p));L) @ I)])
12. y = a1 ∈ ℤ
13. y = a1 ∈ ℤ
⊢ ↑isname(y)

2
1. a1 : ℤ
2. 2 ≤ a1
3. a2 : ℤ
4. 0 ≤ a2
5. a2 < 2
6. L : (Cname × ℕ2) List
7. ∀[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))))
8. I : Cname List
9. y : ℤ
10. 2 ≤ y
11. (y ∈ [a1 / (map(λp.(fst(p));L) @ I)])
12. y = a1 ∈ ℤ
13. y = a1 ∈ ℤ
14. ↑isname(y)
⊢ a1 = a1 ∈ Cname

3
.....assertion..... 
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
8. ¬(y = a1 ∈ Cname)
⊢ ↑isname(y)

4
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
8. ¬(y = a1 ∈ Cname)
9. ↑isname(y)
⊢ if isname(y) then face-maps-comp(L) y else y fi  ~ face-maps-comp(L) y

---

Latex:

---

Latex:
.....equality..... 
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)
\mvdash{}  ((a1:=a2)  o  face-maps-comp(L))  y  \msim{}  face-maps-comp(L)  y


By

---

Latex:
(RepUR  ``name-comp  uext  face-map``  0
  THEN  (BoolCase  \mkleeneopen{}(y  =\msubz{}  a1)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Try  (Trivial)
  THEN  Assert  \mkleeneopen{}\muparrow{}isname(y)\mkleeneclose{}\mcdot{})

---

Home Index