---

Step * 1 1 2 2 2 2 2 1 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. ∀f:{x:ℕn ⟶ ℕn| (rotate-by(n;n - 1) o (x o rotate-by(n;1))) = x ∈ (ℕn ⟶ ℕn)} . (f = rotate-by(n;f 0) ∈ (ℕn ⟶ ℕn))
8. ∀f:{x:cyclic-map(ℕn)| (rotate-by(n;n - 1) o (x o rotate-by(n;1))) = x ∈ (ℕn ⟶ ℕn)} . (¬((f 0) = 0 ∈ ℤ))
⊢ Inj({x:cyclic-map(ℕn)| (rotate-by(n;n - 1) o (x o rotate-by(n;1))) = x ∈ cyclic-map(ℕn)} ;ℕn - 1;λf.((f 0) - 1))
BY
{ ((D 0 THENA (Auto THEN BLemma `cyclic-map-conjugate` THEN Auto))
   THEN skip{(Reduce 0
              THEN RepeatFor 2 ((InstHyp [⌜a1⌝] (-3)⋅
                                 THENA (Auto
                                        THEN RepeatFor 3 (DVar `a1')
                                        THEN MemTypeCD
                                        THEN Auto
                                        THEN D -1
                                        THEN D -2
                                        THEN Auto)
                                 ))
              THEN ((D 0 THENA (Auto THEN BLemma `cyclic-map-conjugate` THEN Auto))
                    THEN Reduce 0
                    THEN RepeatFor 2 ((InstHyp [⌜a2⌝] (-6)⋅
                                       THENA (Auto
                                              THEN RepeatFor 3 (DVar `a2')
                                              THEN MemTypeCD
                                              THEN Auto
                                              THEN D -1
                                              THEN D -2
                                              THEN Auto)
                                       )))⋅)}
   )⋅ }

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. ∀f:{x:ℕn ⟶ ℕn| (rotate-by(n;n - 1) o (x o rotate-by(n;1))) = x ∈ (ℕn ⟶ ℕn)} . (f = rotate-by(n;f 0) ∈ (ℕn ⟶ ℕn))
8. ∀f:{x:cyclic-map(ℕn)| (rotate-by(n;n - 1) o (x o rotate-by(n;1))) = x ∈ (ℕn ⟶ ℕn)} . (¬((f 0) = 0 ∈ ℤ))
9. a1 : {x:cyclic-map(ℕn)| (rotate-by(n;n - 1) o (x o rotate-by(n;1))) = x ∈ cyclic-map(ℕn)} 
⊢ ∀a2:{x:cyclic-map(ℕn)| (rotate-by(n;n - 1) o (x o rotate-by(n;1))) = x ∈ cyclic-map(ℕn)} 
    ((((λf.((f 0) - 1)) a1) = ((λf.((f 0) - 1)) a2) ∈ ℕn - 1)
    ⇒ (a1 = a2 ∈ {x:cyclic-map(ℕn)| (rotate-by(n;n - 1) o (x o rotate-by(n;1))) = x ∈ cyclic-map(ℕ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.  \mforall{}f:\{x:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  (rotate-by(n;n  -  1)  o  (x  o  rotate-by(n;1)))  =  x\}  .  (f  =  rotate-by(n;f  0))
8.  \mforall{}f:\{x:cyclic-map(\mBbbN{}n)|  (rotate-by(n;n  -  1)  o  (x  o  rotate-by(n;1)))  =  x\}  .  (\mneg{}((f  0)  =  0))
\mvdash{}  Inj(\{x:cyclic-map(\mBbbN{}n)|  (rotate-by(n;n  -  1)  o  (x  o  rotate-by(n;1)))  =  x\}  ;\mBbbN{}n  -  1;\mlambda{}f.((f  0)  -  1))


By

---

Latex:
((D  0  THENA  (Auto  THEN  BLemma  `cyclic-map-conjugate`  THEN  Auto))
  THEN  skip\{(Reduce  0
                        THEN  RepeatFor  2  ((InstHyp  [\mkleeneopen{}a1\mkleeneclose{}]  (-3)\mcdot{}
                                                              THENA  (Auto
                                                                            THEN  RepeatFor  3  (DVar  `a1')
                                                                            THEN  MemTypeCD
                                                                            THEN  Auto
                                                                            THEN  D  -1
                                                                            THEN  D  -2
                                                                            THEN  Auto)
                                                              ))
                        THEN  ((D  0  THENA  (Auto  THEN  BLemma  `cyclic-map-conjugate`  THEN  Auto))
                                    THEN  Reduce  0
                                    THEN  RepeatFor  2  ((InstHyp  [\mkleeneopen{}a2\mkleeneclose{}]  (-6)\mcdot{}
                                                                          THENA  (Auto
                                                                                        THEN  RepeatFor  3  (DVar  `a2')
                                                                                        THEN  MemTypeCD
                                                                                        THEN  Auto
                                                                                        THEN  D  -1
                                                                                        THEN  D  -2
                                                                                        THEN  Auto)
                                                                          )))\mcdot{})\}
  )\mcdot{}

---

Home Index