Mercurial > hg > Members > kono > Proof > galois

changeset 127:43d00372bdc9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 05 Sep 2020 08:59:57 +0900
parents d5f093061b46
children 206fc12e5c36
files sym4.agda
diffstat 1 files changed, 38 insertions(+), 13 deletions(-) [+]
line wrap: on
line diff
--- a/sym4.agda	Fri Sep 04 20:20:34 2020 +0900
+++ b/sym4.agda	Sat Sep 05 08:59:57 2020 +0900
@@ -66,20 +66,45 @@
    p0id :  FL→perm ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) =p= pid
    p0id = pleq _ _ refl
 
-   p0 =  FL→perm ((# 0) :: ((# 0) :: ((# 0) :: ((# 0 ) :: f0))))
-   p1 =  FL→perm ((# 0) :: ((# 0) :: ((# 1) :: ((# 0 ) :: f0))))
-   p2 =  FL→perm ((# 0) :: ((# 1) :: ((# 0) :: ((# 0 ) :: f0))))
-   p3 =  FL→perm ((# 0) :: ((# 1) :: ((# 1) :: ((# 0 ) :: f0))))
-   p4 =  FL→perm ((# 0) :: ((# 2) :: ((# 0) :: ((# 0 ) :: f0))))
-   p5 =  FL→perm ((# 0) :: ((# 2) :: ((# 1) :: ((# 0 ) :: f0))))
-   p6 =  FL→perm ((# 1) :: ((# 0) :: ((# 0) :: ((# 0 ) :: f0))))
-   p7 =  FL→perm ((# 1) :: ((# 0) :: ((# 1) :: ((# 0 ) :: f0))))
-   p8 =  FL→perm ((# 1) :: ((# 1) :: ((# 0) :: ((# 0 ) :: f0))))
-   p9 =  FL→perm ((# 1) :: ((# 1) :: ((# 1) :: ((# 0 ) :: f0))))
-   pa =  FL→perm ((# 1) :: ((# 2) :: ((# 0) :: ((# 0 ) :: f0))))
-   pb =  FL→perm ((# 1) :: ((# 2) :: ((# 1) :: ((# 0 ) :: f0))))
-   t0  =  plist p0 ∷ plist p1 ∷  plist p2 ∷ plist p3 ∷ plist p4 ∷  plist p5 ∷ []
+   -- stage 1 (A4)
+   p0 =  (zero :: zero :: zero :: zero :: f0 )
+   p1 =  (zero :: suc zero :: suc zero :: zero :: f0 )
+   p2 =  (zero :: suc (suc zero) :: zero :: zero :: f0 )
+   p3 =  (suc zero :: zero :: suc zero :: zero :: f0 )
+   p4 =  (suc zero :: suc zero :: zero :: zero :: f0 ) 
+   p5 =  (suc zero :: suc (suc zero) :: suc zero :: zero :: f0 )
+   p6 =  (suc (suc zero) :: zero :: zero :: zero :: f0 )
+   p7 =  (suc (suc zero) :: suc zero :: suc zero :: zero :: f0 )
+   p8 =  (suc (suc zero) :: suc (suc zero) :: zero :: zero :: f0 )
+   p9 =  (suc (suc (suc zero)) :: zero :: suc zero :: zero :: f0 )
+   pa =  (suc (suc (suc zero)) :: suc zero :: zero :: zero :: f0 )
+   pb =  (suc (suc (suc zero)) :: suc (suc zero) :: suc zero :: zero :: f0 )
+
+   t0  =  plist (FL→perm p0 ) ∷ plist (FL→perm p1 ) ∷  plist (FL→perm p2 ) ∷ plist (FL→perm p3 ) ∷ plist (FL→perm p4 ) ∷  plist (FL→perm p5 ) ∷ 
+          plist (FL→perm p6 ) ∷ plist (FL→perm p7 ) ∷  plist (FL→perm p8 ) ∷ plist (FL→perm p9 ) ∷ plist (FL→perm pa ) ∷  plist (FL→perm pb ) ∷ []
 
+   t1  : List (FL 4) →  List (FL 4) 
+   t1  x =  tl2 x x [] where
+       tl3 : (FL 4) → ( z : List (FL 4)) → List (FL 4) → List (FL 4)
+       tl3 h [] w = w
+       tl3 h (x ∷ z) w = tl3 h z (( perm→FL [ FL→perm h , FL→perm x ] ) ∷ w )
+       tl2 : ( x z : List (FL 4)) → List (FL 4) →  List (FL 4)
+       tl2 [] _ x = x
+       tl2 (h ∷ x) z w = tl2 x z (tl3 h z w)
+
+   stage1  :  List (FL 4)
+   stage1  =  t1 ( ∀-FL 3 ) 
+
+   -- stage2 ( Kline )
+   --  k0  p0  zero :: zero :: zero :: zero :: f0 ∷                                   (0 ∷ 1 ∷ 2 ∷ 3 ∷ []) ∷
+   --  k1  p3  suc zero :: zero :: suc zero :: zero :: f0 ∷                           (1 ∷ 0 ∷ 3 ∷ 2 ∷ []) ∷
+   --  k2  p8  suc (suc zero) :: suc (suc zero) :: zero :: zero :: f0 ∷               (2 ∷ 3 ∷ 0 ∷ 1 ∷ []) 
+   --  k3  pb  suc (suc (suc zero)) :: suc (suc zero) :: suc zero :: zero :: f0 ∷     (3 ∷ 2 ∷ 1 ∷ 0 ∷ [])
+
+   tb = plist ( FL→perm p0) ∷ plist ( FL→perm p3) ∷ plist ( FL→perm p8) ∷ plist ( FL→perm pb) ∷ []
+
+   stage2  :   List (FL 4)
+   stage2   =  t1 ( p0 ∷ p1 ∷ p2 ∷ p3 ∷ p4 ∷ p5 ∷ p6 ∷ p7 ∷ p8 ∷ p9 ∷ pa ∷ pb ∷ [] ) 
    
    solved1 :  (x : Permutation 4 4) →  Commutator (λ x₁ → Commutator (λ x₂ → Lift (Level.suc Level.zero) ⊤) x₁) x → x =p= pid
    solved1 = {!!}