Mercurial > hg > Members > kono > Proof > galois

changeset 120:77cb357b81a9

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 20:24:00 +0900
parents 2dae51792e1a
children 54035eed6b9b
files sym3.agda
diffstat 1 files changed, 15 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
--- a/sym3.agda	Thu Sep 03 16:13:39 2020 +0900
+++ b/sym3.agda	Thu Sep 03 20:24:00 2020 +0900
@@ -54,13 +54,21 @@
    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)) = {!!}
+   stage12 x uni = case1 prefl
+   stage12 x (comm x1 y1 ) = {!!}
+   stage12 _ (gen {x} {y} sx sy) with stage12 x sx | stage12 y sy --  x =p= pid : t , y =p= pid : s
+   ... | case1 t | case1 s = case1 ( {!!} )
+   ... | case1 t | case2 (case1 x₁) = {!!}
+   ... | case1 t | case2 (case2 x₁) = {!!}
+   ... | case2 t | case1 s = {!!}
+   ... | case2 (case1 s) | case2 (case1 t) = case2 (case2 (pleq _ _ {!!} ))
+   ... | case2 (case1 s) | case2 (case2 t) = {!!}
+   ... | case2 (case2 s) | case2 (case1 t) = {!!}
+   ... | case2 (case2 s) | case2 (case2 t) = {!!}
+   stage12 _ (ccong {y} x=y sx) with stage12 y sx
+   ... | case1 id = case1 ( ptrans (psym x=y ) id )
+   ... | case2 (case1 x₁) = case2 (case1 ( ptrans (psym x=y ) x₁ ))
+   ... | case2 (case2 x₁) = case2 (case2 ( ptrans (psym x=y ) x₁ ))
 
    solved1 :  (x : Permutation 3 3) →  Commutator (λ x₁ → Commutator (λ x₂ → Lift (Level.suc Level.zero) ⊤) x₁) x → x =p= pid
    solved1 = {!!}