Step * 1 5 1 of Lemma face-map-comp2


1. Cname List
2. Cname List
3. name-morph(A;B)
4. nameset(A)
5. nameset(A)
6. : ℕ2
7. : ℕ2
8. ↑isname(g x)
9. ↑isname(g y)
10. ¬(x y ∈ Cname)
11. y ∈ nameset(B)
12. x ∈ nameset(B)
13. x1 nameset(A)
⊢ ((g ((g x:=i) (g y:=j))) x1) ((((x:=i) (y:=j)) g) x1) ∈ extd-nameset(B-[g x; y])
BY
(RenameVar `a' (-1)
   THEN DVar `g'⋅
   THEN RepUR ``name-comp face-map uext`` 0
   THEN (BoolCase ⌜(a =z x)⌝⋅ THENA Auto)
   THEN (BoolCase ⌜(a =z y)⌝⋅ THENA Auto)) }

1
1. {Cname List}
2. Cname List
3. nameset(A) ⟶ extd-nameset(B)
4. ∀i,j:nameset(A).  ((↑isname(g i))  (↑isname(g j))  ((g i) (g j) ∈ extd-nameset(B))  (i j ∈ nameset(A)))
5. : ℤ
6. 2 ≤ x
7. (x ∈ A)
8. : ℤ
9. 2 ≤ y
10. (y ∈ A)
11. : ℤ
12. 0 ≤ i
13. i < 2
14. : ℤ
15. 0 ≤ j
16. j < 2
17. ↑isname(g x)
18. ↑isname(g y)
19. y ∈ nameset(B)
20. x ∈ nameset(B)
21. : ℤ
22. 2 ≤ a
23. (a ∈ A)
24. x ∈ ℤ
25. y ∈ ℤ
26. y ∈ ℤ
⊢ y ∈ Cname

2
1. Cname List
2. Cname List
3. nameset(A) ⟶ extd-nameset(B)
4. ∀i,j:nameset(A).  ((↑isname(g i))  (↑isname(g j))  ((g i) (g j) ∈ extd-nameset(B))  (i j ∈ nameset(A)))
5. nameset(A)
6. nameset(A)
7. : ℕ2
8. : ℕ2
9. ↑isname(g x)
10. ↑isname(g y)
11. ¬(x y ∈ Cname)
12. y ∈ nameset(B)
13. x ∈ nameset(B)
14. nameset(A)
15. a ≠ y
16. x ∈ ℤ
⊢ if isname(g a)
then if isname(if (g =z x) then else fi )
       then if (if (g =z x) then else fi  =z y) then j
            if (g =z x) then i
            else a
            fi 
     if (g =z x) then i
     else a
     fi 
else a
fi 
if isname(if isname(i) then else fi then if isname(i) then else fi 
  if isname(i) then i
  else i
  fi 
∈ extd-nameset(B-[g x; y])

3
1. Cname List
2. Cname List
3. nameset(A) ⟶ extd-nameset(B)
4. ∀i,j:nameset(A).  ((↑isname(g i))  (↑isname(g j))  ((g i) (g j) ∈ extd-nameset(B))  (i j ∈ nameset(A)))
5. nameset(A)
6. nameset(A)
7. : ℕ2
8. : ℕ2
9. ↑isname(g x)
10. ↑isname(g y)
11. ¬(x y ∈ Cname)
12. y ∈ nameset(B)
13. x ∈ nameset(B)
14. nameset(A)
15. a ≠ x
16. y ∈ ℤ
⊢ if isname(g a)
then if isname(if (g =z x) then else fi )
       then if (if (g =z x) then else fi  =z y) then j
            if (g =z x) then i
            else a
            fi 
     if (g =z x) then i
     else a
     fi 
else a
fi 
if isname(if isname(a) then else fi then if isname(a) then else fi 
  if isname(a) then j
  else a
  fi 
∈ extd-nameset(B-[g x; y])

4
1. Cname List
2. Cname List
3. nameset(A) ⟶ extd-nameset(B)
4. ∀i,j:nameset(A).  ((↑isname(g i))  (↑isname(g j))  ((g i) (g j) ∈ extd-nameset(B))  (i j ∈ nameset(A)))
5. nameset(A)
6. nameset(A)
7. : ℕ2
8. : ℕ2
9. ↑isname(g x)
10. ↑isname(g y)
11. ¬(x y ∈ Cname)
12. y ∈ nameset(B)
13. x ∈ nameset(B)
14. nameset(A)
15. a ≠ y
16. a ≠ x
⊢ if isname(g a)
then if isname(if (g =z x) then else fi )
       then if (if (g =z x) then else fi  =z y) then j
            if (g =z x) then i
            else a
            fi 
     if (g =z x) then i
     else a
     fi 
else a
fi 
if isname(if isname(a) then else fi then if isname(a) then else fi 
  if isname(a) then a
  else a
  fi 
∈ extd-nameset(B-[g x; y])


Latex:


Latex:

1.  A  :  Cname  List
2.  B  :  Cname  List
3.  g  :  name-morph(A;B)
4.  x  :  nameset(A)
5.  y  :  nameset(A)
6.  i  :  \mBbbN{}2
7.  j  :  \mBbbN{}2
8.  \muparrow{}isname(g  x)
9.  \muparrow{}isname(g  y)
10.  \mneg{}(x  =  y)
11.  g  y  \mmember{}  nameset(B)
12.  g  x  \mmember{}  nameset(B)
13.  x1  :  nameset(A)
\mvdash{}  ((g  o  ((g  x:=i)  o  (g  y:=j)))  x1)  =  ((((x:=i)  o  (y:=j))  o  g)  x1)


By


Latex:
(RenameVar  `a'  (-1)
  THEN  DVar  `g'\mcdot{}
  THEN  RepUR  ``name-comp  face-map  uext``  0
  THEN  (BoolCase  \mkleeneopen{}(a  =\msubz{}  x)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (BoolCase  \mkleeneopen{}(a  =\msubz{}  y)\mkleeneclose{}\mcdot{}  THENA  Auto))




Home Index