Mercurial > hg > Members > kono > Proof > galois

comparison sym3.agda @ 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
comparison
equal deleted inserted replaced
119:2dae51792e1a 120:77cb357b81a9
52 stage1 x = Commutator (λ x₂ → Lift (Level.suc Level.zero) ⊤) x 52 stage1 x = Commutator (λ x₂ → Lift (Level.suc Level.zero) ⊤) x
53 53
54 open import logic 54 open import logic
55 55
56 stage12 : (x : Permutation 3 3) → stage1 x → ( x =p= pid ) ∨ ( x =p= p3 ) ∨ ( x =p= p4 ) 56 stage12 : (x : Permutation 3 3) → stage1 x → ( x =p= pid ) ∨ ( x =p= p3 ) ∨ ( x =p= p4 )
57 stage12 x sx with perm→FL x 57 stage12 x uni = case1 prefl
58 ... | zero :: (zero :: (zero :: f0)) = case1 (pleq _ _ refl) 58 stage12 x (comm x1 y1 ) = {!!}
59 ... | suc zero :: (zero :: (zero :: f0)) = {!!} 59 stage12 _ (gen {x} {y} sx sy) with stage12 x sx | stage12 y sy -- x =p= pid : t , y =p= pid : s
60 ... | suc (suc zero) :: (zero :: (zero :: f0)) = {!!} 60 ... | case1 t | case1 s = case1 ( {!!} )
61 ... | zero :: (suc zero :: (zero :: f0)) = {!!} 61 ... | case1 t | case2 (case1 x₁) = {!!}
62 ... | suc zero :: (suc zero :: (zero :: f0)) = {!!} 62 ... | case1 t | case2 (case2 x₁) = {!!}
63 ... | suc (suc zero) :: (suc zero :: (zero :: f0)) = {!!} 63 ... | case2 t | case1 s = {!!}
64 ... | case2 (case1 s) | case2 (case1 t) = case2 (case2 (pleq _ _ {!!} ))
65 ... | case2 (case1 s) | case2 (case2 t) = {!!}
66 ... | case2 (case2 s) | case2 (case1 t) = {!!}
67 ... | case2 (case2 s) | case2 (case2 t) = {!!}
68 stage12 _ (ccong {y} x=y sx) with stage12 y sx
69 ... | case1 id = case1 ( ptrans (psym x=y ) id )
70 ... | case2 (case1 x₁) = case2 (case1 ( ptrans (psym x=y ) x₁ ))
71 ... | case2 (case2 x₁) = case2 (case2 ( ptrans (psym x=y ) x₁ ))
64 72
65 solved1 : (x : Permutation 3 3) → Commutator (λ x₁ → Commutator (λ x₂ → Lift (Level.suc Level.zero) ⊤) x₁) x → x =p= pid 73 solved1 : (x : Permutation 3 3) → Commutator (λ x₁ → Commutator (λ x₂ → Lift (Level.suc Level.zero) ⊤) x₁) x → x =p= pid
66 solved1 = {!!} 74 solved1 = {!!}