---

Step * of Lemma orbit-of-involution

∀[T:Type]. ∀[f:T ⟶ T].
  ∀o:T List. (||o|| = 1 ∈ ℤ) ∨ (||o|| = 2 ∈ ℤ) supposing orbit(T;f;o) supposing ∀x:T. ((f (f x)) = x ∈ T)
BY
{ (Intros THEN D 4) }

1
1. [T] : Type
2. [f] : T ⟶ T
3. [%] : ∀x:T. ((f (f x)) = x ∈ T)
4. [%1] : orbit(T;f;[])
⊢ (||[]|| = 1 ∈ ℤ) ∨ (||[]|| = 2 ∈ ℤ)

2
1. [T] : Type
2. [f] : T ⟶ T
3. [%] : ∀x:T. ((f (f x)) = x ∈ T)
4. u : T
5. v : T List
6. [%1] : orbit(T;f;[u / v])
⊢ (||[u / v]|| = 1 ∈ ℤ) ∨ (||[u / v]|| = 2 ∈ ℤ)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[f:T  {}\mrightarrow{}  T].
    \mforall{}o:T  List.  (||o||  =  1)  \mvee{}  (||o||  =  2)  supposing  orbit(T;f;o)  supposing  \mforall{}x:T.  ((f  (f  x))  =  x)


By

---

Latex:
(Intros  THEN  D  4)

---

Home Index