---

Step * 1 of Lemma orbit-of-involution


1. [T] : Type
2. [f] : T ⟶ T
3. [%] : ∀x:T. ((f (f x)) = x ∈ T)
4. [%1] : orbit(T;f;[])
⊢ (||[]|| = 1 ∈ ℤ) ∨ (||[]|| = 2 ∈ ℤ)
BY
{ ((Assert ⌜False⌝⋅ THEN Auto) THEN D -1 THEN Reduce -2 THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [f]  :  T  {}\mrightarrow{}  T
3.  [\%]  :  \mforall{}x:T.  ((f  (f  x))  =  x)
4.  [\%1]  :  orbit(T;f;[])
\mvdash{}  (||[]||  =  1)  \mvee{}  (||[]||  =  2)


By

---

Latex:
((Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)  THEN  D  -1  THEN  Reduce  -2  THEN  Auto)

---

Home Index