---

Step * 1 of Lemma name-morph-flips-commute


1. I : Cname List
2. x : name-morph(I;[])
3. i : nameset(I)
4. j : nameset(I)
5. x1 : nameset(I)
⊢ (flip(flip(x;j);i) x1) = (flip(flip(x;i);j) x1) ∈ extd-nameset([])
BY
{ Assert ⌜(flip(flip(x;j);i) x1) = (flip(flip(x;i);j) x1) ∈ ℕ2⌝⋅ }

1
.....assertion..... 
1. I : Cname List
2. x : name-morph(I;[])
3. i : nameset(I)
4. j : nameset(I)
5. x1 : nameset(I)
⊢ (flip(flip(x;j);i) x1) = (flip(flip(x;i);j) x1) ∈ ℕ2

2
1. I : Cname List
2. x : name-morph(I;[])
3. i : nameset(I)
4. j : nameset(I)
5. x1 : nameset(I)
6. (flip(flip(x;j);i) x1) = (flip(flip(x;i);j) x1) ∈ ℕ2
⊢ (flip(flip(x;j);i) x1) = (flip(flip(x;i);j) x1) ∈ extd-nameset([])

---

Latex:

---

Latex:

1.  I  :  Cname  List
2.  x  :  name-morph(I;[])
3.  i  :  nameset(I)
4.  j  :  nameset(I)
5.  x1  :  nameset(I)
\mvdash{}  (flip(flip(x;j);i)  x1)  =  (flip(flip(x;i);j)  x1)


By

---

Latex:
Assert  \mkleeneopen{}(flip(flip(x;j);i)  x1)  =  (flip(flip(x;i);j)  x1)\mkleeneclose{}\mcdot{}

---

Home Index