---

Step * 2 1 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||
⊢ u = u2 ∈ T
BY
{ ((InstHyp [⌜0⌝] (-2)⋅ THENA Auto) THEN Reduce -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||
11. (f u) = if (0 =z (((||v|| + 1) + 1) + 1) - 1) then u else u1 fi  ∈ T
⊢ 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||
\mvdash{}  u  =  u2


By

---

Latex:
((InstHyp  [\mkleeneopen{}0\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)  THEN  Reduce  -1)

---

Home Index