---

Step * 1 2 of Lemma face-maps-commute


1. I : Cname List
2. x : nameset(I)
3. i : ℕ2
4. y : nameset(I)
5. j : ℕ2
6. ¬(x = y ∈ Cname)
7. (y:=j) ∈ name-morph(I-[x];I-[x; y])
⊢ ((x:=i) o (y:=j)) = ((y:=j) o (x:=i)) ∈ (nameset(I) ⟶ extd-nameset(I-[x; y]))
BY
{ ((Ext THENA Auto)
   THEN RenameVar `a' (-1)
   THEN RepUR ``name-comp face-map uext`` 0
   THEN (BoolCase ⌜(a =z x)⌝⋅ THENA Auto)
   THEN (BoolCase ⌜(a =z y)⌝⋅ THENA Auto)) }

1
1. I : {Cname List}
2. x : ℤ
3. 2 ≤ x
4. (x ∈ I)
5. i : ℤ
6. 0 ≤ i
7. i < 2
8. y : ℤ
9. 2 ≤ y
10. (y ∈ I)
11. j : ℤ
12. 0 ≤ j
13. j < 2
14. (y:=j) ∈ name-morph(I-[x];I-[x; y])
15. a : ℤ
16. 2 ≤ a
17. (a ∈ I)
18. a = x ∈ ℤ
19. a = y ∈ ℤ
20. x = y ∈ ℤ
⊢ y = y ∈ Cname

2
1. I : Cname List
2. x : nameset(I)
3. i : ℕ2
4. y : nameset(I)
5. j : ℕ2
6. ¬(x = y ∈ Cname)
7. (y:=j) ∈ name-morph(I-[x];I-[x; y])
8. a : nameset(I)
9. a ≠ y
10. a = x ∈ ℤ
⊢ if isname(i) then i else i fi  = if isname(a) then i else a fi  ∈ extd-nameset(I-[x; y])

3
1. I : Cname List
2. x : nameset(I)
3. i : ℕ2
4. y : nameset(I)
5. j : ℕ2
6. ¬(x = y ∈ Cname)
7. (y:=j) ∈ name-morph(I-[x];I-[x; y])
8. a : nameset(I)
9. a ≠ x
10. a = y ∈ ℤ
⊢ if isname(a) then j else a fi  = if isname(j) then j else j fi  ∈ extd-nameset(I-[x; y])

4
1. I : Cname List
2. x : nameset(I)
3. i : ℕ2
4. y : nameset(I)
5. j : ℕ2
6. ¬(x = y ∈ Cname)
7. (y:=j) ∈ name-morph(I-[x];I-[x; y])
8. a : nameset(I)
9. a ≠ y
10. a ≠ x
⊢ if isname(a) then a else a fi  = if isname(a) then a else a fi  ∈ extd-nameset(I-[x; y])

---

Latex:

---

Latex:

1.  I  :  Cname  List
2.  x  :  nameset(I)
3.  i  :  \mBbbN{}2
4.  y  :  nameset(I)
5.  j  :  \mBbbN{}2
6.  \mneg{}(x  =  y)
7.  (y:=j)  \mmember{}  name-morph(I-[x];I-[x;  y])
\mvdash{}  ((x:=i)  o  (y:=j))  =  ((y:=j)  o  (x:=i))


By

---

Latex:
((Ext  THENA  Auto)
  THEN  RenameVar  `a'  (-1)
  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