---

Step * 2 of Lemma orbit-of-involution


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 ∈ ℤ)
BY
{ ((D -2 THEN Reduce 0)
   THEN Auto
   THEN OrRight
   THEN Auto
   THEN D -2
   THEN Reduce 0
   THEN Auto
   THEN Assert ⌜False⌝⋅
   THEN Auto
   THEN (Assert 0 ≤ ||v|| BY
               Auto)) }

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. orbit(T;f;[u; u1; [u2 / v]])
9. 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.  v  :  T  List
6.  [\%1]  :  orbit(T;f;[u  /  v])
\mvdash{}  (||[u  /  v]||  =  1)  \mvee{}  (||[u  /  v]||  =  2)


By

---

Latex:
((D  -2  THEN  Reduce  0)
  THEN  Auto
  THEN  OrRight
  THEN  Auto
  THEN  D  -2
  THEN  Reduce  0
  THEN  Auto
  THEN  Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  (Assert  0  \mleq{}  ||v||  BY
                          Auto))

---

Home Index