Mercurial > hg > Members > kono > Proof > galois

changeset 119:2dae51792e1a

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 Thu, 03 Sep 2020 16:13:39 +0900
parents 019b98d398ee
children 77cb357b81a9
files sym3.agda
diffstat 1 files changed, 22 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/sym3.agda	Thu Sep 03 14:06:18 2020 +0900
+++ b/sym3.agda	Thu Sep 03 16:13:39 2020 +0900
@@ -38,7 +38,29 @@
    p5 =  FL→perm ((# 2) :: ((# 1) :: ((# 0 ) :: f0))) 
    t0  =  plist p0 ∷ plist p1 ∷  plist p2 ∷ plist p3 ∷ plist p4 ∷  plist p5 ∷ [] 
 
+   t1  =  plist [ p0 , p0 ] ∷ plist [ p1 , p0 ] ∷  plist [ p2 , p0 ] ∷ plist [ p3 , p0 ] ∷ plist [ p4 , p0 ] ∷  plist [ p5 , p1 ] ∷ 
+          plist [ p0 , p1 ] ∷ plist [ p1 , p1 ] ∷  plist [ p2 , p1 ] ∷ plist [ p3 , p1 ] ∷ plist [ p4 , p1 ] ∷  plist [ p5 , p1 ] ∷ 
+          plist [ p0 , p2 ] ∷ plist [ p1 , p2 ] ∷  plist [ p2 , p2 ] ∷ plist [ p3 , p2 ] ∷ plist [ p4 , p2 ] ∷  plist [ p5 , p2 ] ∷ 
+          plist [ p0 , p3 ] ∷ plist [ p1 , p3 ] ∷  plist [ p3 , p3 ] ∷ plist [ p3 , p3 ] ∷ plist [ p4 , p3 ] ∷  plist [ p5 , p3 ] ∷ 
+          plist [ p0 , p4 ] ∷ plist [ p1 , p4 ] ∷  plist [ p3 , p4 ] ∷ plist [ p3 , p4 ] ∷ plist [ p4 , p4 ] ∷  plist [ p5 , p4 ] ∷ 
+          plist [ p0 , p5 ] ∷ plist [ p1 , p5 ] ∷  plist [ p3 , p5 ] ∷ plist [ p3 , p5 ] ∷ plist [ p4 , p4 ] ∷  plist [ p5 , p5 ] ∷ 
+          []
+
    open _=p=_
    
+   stage1 :  (x : Permutation 3 3) →  Set (Level.suc Level.zero)
+   stage1 x = Commutator (λ x₂ → Lift (Level.suc Level.zero) ⊤)  x 
+
+   open import logic
+   
+   stage12  :  (x : Permutation 3 3) → stage1 x →  ( x =p= pid ) ∨ ( x =p= p3 ) ∨ ( x =p= p4 )
+   stage12 x sx with perm→FL x 
+   ... | zero :: (zero :: (zero :: f0)) = case1 (pleq _ _ refl)
+   ... | suc zero :: (zero :: (zero :: f0)) = {!!}
+   ... | suc (suc zero) :: (zero :: (zero :: f0)) = {!!}
+   ... | zero :: (suc zero :: (zero :: f0)) = {!!}
+   ... | suc zero :: (suc zero :: (zero :: f0)) = {!!}
+   ... | suc (suc zero) :: (suc zero :: (zero :: f0)) = {!!}
+
    solved1 :  (x : Permutation 3 3) →  Commutator (λ x₁ → Commutator (λ x₂ → Lift (Level.suc Level.zero) ⊤) x₁) x → x =p= pid
    solved1 = {!!}