---

Step * 1 of Lemma flip-conjugation


1. n : ℕ
2. k : ℕn
3. j : ℕk
4. l : ℕn - k
5. x : ℕn
⊢ ((j, k + l) x) = (((k, k + l) o ((j, k) o (k, k + l))) x) ∈ ℕn
BY
{ xxxEqTypeCDxxx }

1
1. n : ℕ
2. k : ℕn
3. j : ℕk
4. l : ℕn - k
5. x : ℕn
⊢ ((j, k + l) x) = (((k, k + l) o ((j, k) o (k, k + l))) x) ∈ ℤ

2
.....set predicate..... 
1. n : ℕ
2. k : ℕn
3. j : ℕk
4. l : ℕn - k
5. x : ℕn
⊢ 0 ≤ (j, k + l) x < n

3
.....wf..... 
1. n : ℕ
2. k : ℕn
3. j : ℕk
4. l : ℕn - k
5. x : ℕn
6. k1 : ℤ
⊢ 0 ≤ k1 < n = 0 ≤ k1 < n ∈ Type

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  k  :  \mBbbN{}n
3.  j  :  \mBbbN{}k
4.  l  :  \mBbbN{}n  -  k
5.  x  :  \mBbbN{}n
\mvdash{}  ((j,  k  +  l)  x)  =  (((k,  k  +  l)  o  ((j,  k)  o  (k,  k  +  l)))  x)


By

---

Latex:
xxxEqTypeCDxxx

---

Home Index