Step
*
1
5
1
of Lemma
face-map-comp2
1. A : Cname List
2. B : Cname List
3. g : name-morph(A;B)
4. x : nameset(A)
5. y : nameset(A)
6. i : ℕ2
7. j : ℕ2
8. ↑isname(g x)
9. ↑isname(g y)
10. ¬(x = y ∈ Cname)
11. g y ∈ nameset(B)
12. g x ∈ nameset(B)
13. x1 : nameset(A)
⊢ ((g o ((g x:=i) o (g y:=j))) x1) = ((((x:=i) o (y:=j)) o g) x1) ∈ extd-nameset(B-[g x; g 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. A : {Cname List}
2. B : Cname List
3. g : 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. x : ℤ
6. 2 ≤ x
7. (x ∈ A)
8. y : ℤ
9. 2 ≤ y
10. (y ∈ A)
11. i : ℤ
12. 0 ≤ i
13. i < 2
14. j : ℤ
15. 0 ≤ j
16. j < 2
17. ↑isname(g x)
18. ↑isname(g y)
19. g y ∈ nameset(B)
20. g x ∈ nameset(B)
21. a : ℤ
22. 2 ≤ a
23. (a ∈ A)
24. a = x ∈ ℤ
25. a = y ∈ ℤ
26. x = y ∈ ℤ
⊢ y = y ∈ Cname
2
1. A : Cname List
2. B : Cname List
3. g : 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. x : nameset(A)
6. y : nameset(A)
7. i : ℕ2
8. j : ℕ2
9. ↑isname(g x)
10. ↑isname(g y)
11. ¬(x = y ∈ Cname)
12. g y ∈ nameset(B)
13. g x ∈ nameset(B)
14. a : nameset(A)
15. a ≠ y
16. a = x ∈ ℤ
⊢ if isname(g a)
then if isname(if (g a =z g x) then i else g a fi )
       then if (if (g a =z g x) then i else g a fi  =z g y) then j
            if (g a =z g x) then i
            else g a
            fi 
     if (g a =z g x) then i
     else g a
     fi 
else g a
fi 
= if isname(if isname(i) then i else i fi ) then g if isname(i) then i else i fi 
  if isname(i) then i
  else i
  fi 
∈ extd-nameset(B-[g x; g y])
3
1. A : Cname List
2. B : Cname List
3. g : 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. x : nameset(A)
6. y : nameset(A)
7. i : ℕ2
8. j : ℕ2
9. ↑isname(g x)
10. ↑isname(g y)
11. ¬(x = y ∈ Cname)
12. g y ∈ nameset(B)
13. g x ∈ nameset(B)
14. a : nameset(A)
15. a ≠ x
16. a = y ∈ ℤ
⊢ if isname(g a)
then if isname(if (g a =z g x) then i else g a fi )
       then if (if (g a =z g x) then i else g a fi  =z g y) then j
            if (g a =z g x) then i
            else g a
            fi 
     if (g a =z g x) then i
     else g a
     fi 
else g a
fi 
= if isname(if isname(a) then j else a fi ) then g if isname(a) then j else a fi 
  if isname(a) then j
  else a
  fi 
∈ extd-nameset(B-[g x; g y])
4
1. A : Cname List
2. B : Cname List
3. g : 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. x : nameset(A)
6. y : nameset(A)
7. i : ℕ2
8. j : ℕ2
9. ↑isname(g x)
10. ↑isname(g y)
11. ¬(x = y ∈ Cname)
12. g y ∈ nameset(B)
13. g x ∈ nameset(B)
14. a : nameset(A)
15. a ≠ y
16. a ≠ x
⊢ if isname(g a)
then if isname(if (g a =z g x) then i else g a fi )
       then if (if (g a =z g x) then i else g a fi  =z g y) then j
            if (g a =z g x) then i
            else g a
            fi 
     if (g a =z g x) then i
     else g a
     fi 
else g a
fi 
= if isname(if isname(a) then a else a fi ) then g if isname(a) then a else a fi 
  if isname(a) then a
  else a
  fi 
∈ extd-nameset(B-[g x; g 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