---

Step * 1 1 2 3 of Lemma wilson-theorem


1. n : {i:ℤ| 1 < i} 
2. prime(n)
3. ∀b:ℕn. ((rotate-by(n;1) (rotate-by(n;n - 1) b)) = b ∈ ℕn)
4. ∀b:ℕn. ((rotate-by(n;n - 1) (rotate-by(n;1) b)) = b ∈ ℕn)
5. cyclic-map(ℕn) ~ ℕ(n - 1)!
6. Inj(cyclic-map(ℕn);cyclic-map(ℕn);λf.(rotate-by(n;n - 1) o (f o rotate-by(n;1))))
7. {x:cyclic-map(ℕn)| (rotate-by(n;n - 1) o (x o rotate-by(n;1))) = x ∈ cyclic-map(ℕn)}  ~ ℕn - 1
8. x : cyclic-map(ℕn)
⊢ (λf.(rotate-by(n;n - 1) o (f o rotate-by(n;1)))^n x) = x ∈ cyclic-map(ℕn)
BY
{ (Symmetry THEN D -1 THEN EqTypeCD) }

1
1. n : {i:ℤ| 1 < i} 
2. prime(n)
3. ∀b:ℕn. ((rotate-by(n;1) (rotate-by(n;n - 1) b)) = b ∈ ℕn)
4. ∀b:ℕn. ((rotate-by(n;n - 1) (rotate-by(n;1) b)) = b ∈ ℕn)
5. cyclic-map(ℕn) ~ ℕ(n - 1)!
6. Inj(cyclic-map(ℕn);cyclic-map(ℕn);λf.(rotate-by(n;n - 1) o (f o rotate-by(n;1))))
7. {x:cyclic-map(ℕn)| (rotate-by(n;n - 1) o (x o rotate-by(n;1))) = x ∈ cyclic-map(ℕn)}  ~ ℕn - 1
8. x : ℕn →⟶ ℕn
9. ∀x@0,y:ℕn.  ∃n@0:ℕ. ((x^n@0 x@0) = y ∈ ℕn)
⊢ x = (λf.(rotate-by(n;n - 1) o (f o rotate-by(n;1)))^n x) ∈ ℕn →⟶ ℕn

2
.....set predicate..... 
1. n : {i:ℤ| 1 < i} 
2. prime(n)
3. ∀b:ℕn. ((rotate-by(n;1) (rotate-by(n;n - 1) b)) = b ∈ ℕn)
4. ∀b:ℕn. ((rotate-by(n;n - 1) (rotate-by(n;1) b)) = b ∈ ℕn)
5. cyclic-map(ℕn) ~ ℕ(n - 1)!
6. Inj(cyclic-map(ℕn);cyclic-map(ℕn);λf.(rotate-by(n;n - 1) o (f o rotate-by(n;1))))
7. {x:cyclic-map(ℕn)| (rotate-by(n;n - 1) o (x o rotate-by(n;1))) = x ∈ cyclic-map(ℕn)}  ~ ℕn - 1
8. x : ℕn →⟶ ℕn
9. ∀x@0,y:ℕn.  ∃n@0:ℕ. ((x^n@0 x@0) = y ∈ ℕn)
⊢ ∀x@0,y:ℕn.  ∃n@0:ℕ. ((x^n@0 x@0) = y ∈ ℕn)

3
.....wf..... 
1. n : {i:ℤ| 1 < i} 
2. prime(n)
3. ∀b:ℕn. ((rotate-by(n;1) (rotate-by(n;n - 1) b)) = b ∈ ℕn)
4. ∀b:ℕn. ((rotate-by(n;n - 1) (rotate-by(n;1) b)) = b ∈ ℕn)
5. cyclic-map(ℕn) ~ ℕ(n - 1)!
6. Inj(cyclic-map(ℕn);cyclic-map(ℕn);λf.(rotate-by(n;n - 1) o (f o rotate-by(n;1))))
7. {x:cyclic-map(ℕn)| (rotate-by(n;n - 1) o (x o rotate-by(n;1))) = x ∈ cyclic-map(ℕn)}  ~ ℕn - 1
8. x : ℕn →⟶ ℕn
9. ∀x@0,y:ℕn.  ∃n@0:ℕ. ((x^n@0 x@0) = y ∈ ℕn)
10. f : ℕn →⟶ ℕn
⊢ istype(∀x,y:ℕn.  ∃n@0:ℕ. ((f^n@0 x) = y ∈ ℕn))

---

Latex:

---

Latex:

1.  n  :  \{i:\mBbbZ{}|  1  <  i\} 
2.  prime(n)
3.  \mforall{}b:\mBbbN{}n.  ((rotate-by(n;1)  (rotate-by(n;n  -  1)  b))  =  b)
4.  \mforall{}b:\mBbbN{}n.  ((rotate-by(n;n  -  1)  (rotate-by(n;1)  b))  =  b)
5.  cyclic-map(\mBbbN{}n)  \msim{}  \mBbbN{}(n  -  1)!
6.  Inj(cyclic-map(\mBbbN{}n);cyclic-map(\mBbbN{}n);\mlambda{}f.(rotate-by(n;n  -  1)  o  (f  o  rotate-by(n;1))))
7.  \{x:cyclic-map(\mBbbN{}n)|  (rotate-by(n;n  -  1)  o  (x  o  rotate-by(n;1)))  =  x\}    \msim{}  \mBbbN{}n  -  1
8.  x  :  cyclic-map(\mBbbN{}n)
\mvdash{}  (\mlambda{}f.(rotate-by(n;n  -  1)  o  (f  o  rotate-by(n;1)))\^{}n  x)  =  x


By

---

Latex:
(Symmetry  THEN  D  -1  THEN  EqTypeCD)

---

Home Index