---

Step * 2 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. 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
BY
{ ((D -3 With ⌜0⌝  THENA Auto) THEN (D -1 With ⌜2⌝  THENA 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. 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

---

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.  no\_repeats(T;[u;  u1;  [u2  /  v]])
10.  \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  )
11.  0  \mleq{}  ||v||
\mvdash{}  False


By

---

Latex:
((D  -3  With  \mkleeneopen{}0\mkleeneclose{}    THENA  Auto)  THEN  (D  -1  With  \mkleeneopen{}2\mkleeneclose{}    THENA  Auto))

---

Home Index