Mercurial > hg > Members > kono > Proof > galois

comparison sym3.agda @ 111:d3da6e2c0d90

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 Tue, 01 Sep 2020 21:58:15 +0900
parents 405c1f727ffe
children 2dae51792e1a
comparison
equal deleted inserted replaced
110:cb3281e83229 111:d3da6e2c0d90
24 solvable.end sym3solvable x d = solved1 x d where 24 solvable.end sym3solvable x d = solved1 x d where
25 25
26 open import Data.List using ( List ; [] ; _∷_ ) 26 open import Data.List using ( List ; [] ; _∷_ )
27 27
28 open Solvable (Symmetric 3) 28 open Solvable (Symmetric 3)
29 -- open Group (Symmetric 2) using (_⁻¹)
30 29
31 p0 : FL→perm ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) =p= pid 30 p0id : FL→perm ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) =p= pid
32 p0 = record { peq = p00 } where 31 p0id = pleq _ _ refl
33 p00 : (q : Fin 3) → (FL→perm ((# 0) :: ((# 0) :: ((# 0) :: f0))) ⟨$⟩ʳ q) ≡ (pid ⟨$⟩ʳ q)
34 p00 zero = refl
35 p00 (suc zero) = refl
36 p00 (suc (suc zero)) = refl
37 32
38 p1 = FL→perm ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) 33 p0 = FL→perm ((# 0) :: ((# 0) :: ((# 0 ) :: f0)))
34 p1 = FL→perm ((# 0) :: ((# 1) :: ((# 0 ) :: f0)))
35 p2 = FL→perm ((# 1) :: ((# 0) :: ((# 0 ) :: f0)))
36 p3 = FL→perm ((# 1) :: ((# 1) :: ((# 0 ) :: f0)))
37 p4 = FL→perm ((# 2) :: ((# 0) :: ((# 0 ) :: f0)))
38 p5 = FL→perm ((# 2) :: ((# 1) :: ((# 0 ) :: f0)))
39 t0 = plist p0 ∷ plist p1 ∷ plist p2 ∷ plist p3 ∷ plist p4 ∷ plist p5 ∷ []
39 40
40 open _=p=_ 41 open _=p=_
41 42
42 solved1 : (x : Permutation 3 3) → Commutator (λ x₁ → Commutator (λ x₂ → Lift (Level.suc Level.zero) ⊤) x₁) x → x =p= pid 43 solved1 : (x : Permutation 3 3) → Commutator (λ x₁ → Commutator (λ x₂ → Lift (Level.suc Level.zero) ⊤) x₁) x → x =p= pid
43 solved1 = {!!} 44 solved1 = {!!}