---

Step * 2 1 1 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. 0 < ||[u; u1; [u2 / v]]||
9. ∀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)
10. 0 ≤ ||v||
11. (¬([u; u1; [u2 / v]][0] = [u; u1; [u2 / v]][2] ∈ T)) supposing 
       ((¬(0 = 2 ∈ ℕ)) and 
       2 < ||[u; u1; [u2 / v]]|| and 
       0 < ||[u; u1; [u2 / v]]||)
⊢ False
BY
{ (Reduce -1 THEN RepeatFor 3 ((D -1 THENA Auto)) THEN D -1) }

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. ∀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)
10. 0 ≤ ||v||
⊢ u = u2 ∈ T

---

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.  0  <  ||[u;  u1;  [u2  /  v]]||
9.  \mforall{}i:\mBbbN{}||[u;  u1;  [u2  /  v]]||
          ((f  [u;  u1;  [u2  /  v]][i])
          =  if  (i  =\msubz{}  ||[u;  u1;  [u2  /  v]]||  -  1)
              then  [u;  u1;  [u2  /  v]][0]
              else  [u;  u1;  [u2  /  v]][i  +  1]
              fi  )
10.  0  \mleq{}  ||v||
11.  (\mneg{}([u;  u1;  [u2  /  v]][0]  =  [u;  u1;  [u2  /  v]][2]))  supposing 
              ((\mneg{}(0  =  2))  and 
              2  <  ||[u;  u1;  [u2  /  v]]||  and 
              0  <  ||[u;  u1;  [u2  /  v]]||)
\mvdash{}  False


By

---

Latex:
(Reduce  -1  THEN  RepeatFor  3  ((D  -1  THENA  Auto))  THEN  D  -1)

---

Home Index