---

Step * 2 1 of Lemma orbit-of-involution


1. T : Type
2. f : T ⟶ T
3. ∀x:T. ((f (f x)) = x ∈ T)
4. u : T
5. u1 : T
6. u2 : T
7. v : T List
8. orbit(T;f;[u; u1; [u2 / v]])
9. 0 ≤ ||v||
⊢ False
BY
{ (D -2 THEN ExRepD) }

1
1. T : Type
2. f : T ⟶ T
3. ∀x:T. ((f (f x)) = x ∈ T)
4. u : T
5. u1 : T
6. u2 : T
7. v : T List
8. 0 < ||[u; u1; [u2 / v]]||
9. no_repeats(T;[u; u1; [u2 / v]])
10. ∀i:ℕ||[u; u1; [u2 / v]]||
      ((f [u; u1; [u2 / v]][i])
      = if (i =z ||[u; u1; [u2 / v]]|| - 1) then [u; u1; [u2 / v]][0] else [u; u1; [u2 / v]][i + 1] fi 
      ∈ T)
11. 0 ≤ ||v||
⊢ False

---

Latex:

---

Latex:

1.  T  :  Type
2.  f  :  T  {}\mrightarrow{}  T
3.  \mforall{}x:T.  ((f  (f  x))  =  x)
4.  u  :  T
5.  u1  :  T
6.  u2  :  T
7.  v  :  T  List
8.  orbit(T;f;[u;  u1;  [u2  /  v]])
9.  0  \mleq{}  ||v||
\mvdash{}  False


By

---

Latex:
(D  -2  THEN  ExRepD)

---

Home Index