--- a/sym5.agda	Mon Aug 24 23:06:10 2020 +0900
+++ b/sym5.agda	Tue Aug 25 11:07:39 2020 +0900
@@ -1,6 +1,6 @@
 open import Level hiding ( suc ; zero )
 open import Algebra
-module sym3 where
+module sym5 where
 
 open import Symmetric 
 open import Data.Unit
@@ -18,6 +18,50 @@
 
 open import Data.Fin
 open import Data.Fin.Permutation
+open import Data.List  hiding ( [_] )
 
 ¬sym5solvable : ¬ ( solvable (Symmetric 5) )
-¬sym5solvable sol = {!!}
+¬sym5solvable sol = counter-example (end5  [ dba , aec ] d ) where
+
+--
+--    dba       1320      d → b → a → d
+--    (dba)⁻¹   3021      a → b → d → a
+--    aec       21430
+--    (aec)⁻¹   41032
+--    (abd)(cea)(dba)(aec)
+-- 
+
+     open solvable
+     open Solvable (Symmetric 5) 
+     end5 : (x : Permutation 5 5) → deriving (dervied-length sol) x →  x =p= pid  
+     end5 x der = end sol x der
+
+     --- 1 ∷ 0 ∷ 2 ∷ []
+     --- 0 ∷ 2 ∷ 1 ∷ 3 ∷ []
+     --- 1 ∷ 3 ∷ 2 ∷ 0 ∷ 4 ∷ []
+     --  2 ∷ 1 ∷ 3 ∷ 0 ∷ 4 ∷ []  (dba)⁻¹ = abd
+     dba : Permutation 5 5
+     dba = pprep (pprep (pswap (pid {1}))) ∘ₚ pins (n≤ 3)
+     t1 = plist dba ∷ plist (pinv dba) ∷ []
+     --  1 ∷ 0 ∷ []  
+     --  0 ∷ 2 ∷ 1 ∷ []  
+     --  1 ∷ 0 ∷ 3 ∷ 2 ∷ []  
+     --  2 ∷ 1 ∷ 4 ∷ 3 ∷ 0 ∷ []  
+     --  4 ∷ 1 ∷ 0 ∷ 3 ∷ 2 ∷ []  (aec)⁻¹ = cea
+     aec : Permutation 5 5
+     aec = pprep (pprep (pprep (pswap (pid {0}))) ∘ₚ pins (n≤ 1)) ∘ₚ pins (n≤ 4)
+     tt2 = plist aec ∷ plist (pinv aec) ∷ []
+
+     open _=p=_
+     postulate counter-example : ¬ ( [ dba , aec ] =p= pid )
+     -- counter-example eq with peq eq zero
+     -- counter-example eq | ()
+
+     d : deriving (dervied-length sol) [ dba , aec ] 
+     d = {!!}
+     -- d with dervied-length sol
+     -- ... | zero = Lift.lift tt
+     -- ... | suc i = comm {?} {dba} {aec} ? ?
+
+
+