Mercurial > hg > Members > kono > Proof > galois

changeset 114:eb1dcba4752e

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 Wed, 02 Sep 2020 19:20:20 +0900
parents d8a21c5db0e0
children 32df4073746e
files sym5.agda
diffstat 1 files changed, 26 insertions(+), 21 deletions(-) [+]
line wrap: on
line diff
--- a/sym5.agda	Wed Sep 02 18:55:15 2020 +0900
+++ b/sym5.agda	Wed Sep 02 19:20:20 2020 +0900
@@ -27,7 +27,7 @@
 open _∧_
 
 ¬sym5solvable : ¬ ( solvable (Symmetric 5) )
-¬sym5solvable sol = counter-example (end5 (abc 0<3 0<4 ) (proj1 (dervie-any-3rot (dervied-length sol) 0<3 0<4 ) )) where
+¬sym5solvable sol = counter-example (end5 (abc 0<3 0<4 ) (proj1 (dervie-any-3rot0 (dervied-length sol) 0<3 0<4 ) )) where
 
 --
 --    dba       1320      d → b → a → d
@@ -198,29 +198,34 @@
      
 
 
-     dervie-any-3rot : (n : ℕ ) → {i j : ℕ }  → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 )
-          → deriving n (abc i<3 j<4 ) ∧ deriving n (dba i<3 j<4 ) ∧ deriving n (aec i<3 j<4 )
-     dervie-any-3rot 0 i<3 j<4 = ⟪ lift tt , ⟪ lift tt , lift tt ⟫ ⟫
-     dervie-any-3rot (suc i) i<3 j<4 =  ⟪ d0 , ⟪ d1 , d2 ⟫ ⟫ where
-        tc : Triple i<3 j<4 3rot
+     dervie-any-3rot0 : (n : ℕ ) → {i j : ℕ }  → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 )
+          → deriving n (abc i<3 j<4 ) 
+     dervie-any-3rot1 : (n : ℕ ) → {i j : ℕ }  → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 )
+          → deriving n (dba i<3 j<4 ) 
+     dervie-any-3rot2 : (n : ℕ ) → {i j : ℕ }  → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 )
+          → deriving n (aec i<3 j<4 )
+
+     dervie-any-3rot0 0 i<3 j<4 = lift tt 
+     dervie-any-3rot0 (suc i) i<3 j<4 =  
+       ccong {deriving i} ( psym (abc= tc)) (
+          comm {deriving i} {dba (fin≤n {3} (dba0<3 tc)) (fin≤n {4} (dba1<4 tc))} {aec (fin≤n {3} (aec0<3 tc)) (fin≤n {4} (aec1<4 tc))}
+              ( dervie-any-3rot1 i  (fin≤n {3} (dba0<3 tc)) (fin≤n {4} (dba1<4 tc)))
+              ( dervie-any-3rot2 i  (fin≤n {3} (aec0<3 tc)) (fin≤n {4} (aec1<4 tc)))) where
         tc = triple i<3 j<4
-        d0 : deriving (suc i) (abc i<3 j<4)
-        d0 = ccong {deriving i} ( psym (abc= tc)) (
-          comm {deriving i} {dba (fin≤n {3} (dba0<3 tc)) (fin≤n {4} (dba1<4 tc))} {aec (fin≤n {3} (aec0<3 tc)) (fin≤n {4} (aec1<4 tc))}
-              (proj1 (proj2 ( dervie-any-3rot i  (fin≤n {3} (dba0<3 tc)) (fin≤n {4} (dba1<4 tc)))))
-              (proj2 (proj2 ( dervie-any-3rot i  (fin≤n {3} (aec0<3 tc)) (fin≤n {4} (aec1<4 tc))))))
+
+     dervie-any-3rot1 (suc i) i<3 j<4 = {!!} 
+      ccong {deriving i} ( psym (abc= tdba )) (   
+          comm {deriving i} {aec (fin≤n {3} (dba0<3 tdba)) (fin≤n {4} (dba1<4 tdba))}  {abc (fin≤n {3} (aec0<3 tdba)) (fin≤n {4} (aec1<4 tdba))}
+              (dervie-any-3rot2 i  (fin≤n {3} (dba0<3 tdba) (fin≤n {4} (dba1<4 tdba) )))
+              (dervie-any-3rot0 i  (fin≤n {3} (aec0<3 tdba)) (fin≤n {4} (aec1<4 tdba) ))) where
         tdba = dba-triple i<3 j<4
-        d1 : deriving (suc i) (dba i<3 j<4)
-        d1 = ccong {deriving i} ( psym (abc= tdba )) (   
-          comm {deriving i} {aec (fin≤n {3} (dba0<3 tdba)) (fin≤n {4} (dba1<4 tdba))}  {abc (fin≤n {3} (aec0<3 tdba)) (fin≤n {4} (aec1<4 tdba))}
-              (proj2 (proj2 ( dervie-any-3rot i  (fin≤n {3} (dba0<3 tdba) (fin≤n {4} (dba1<4 tdba) )))))
-              (proj1 ( dervie-any-3rot i  (fin≤n {3} (aec0<3 tdba)) (fin≤n {4} (aec1<4 tdba) ))))
+
+     dervie-any-3rot2 (suc i) i<3 j<4 = {!!} 
+        ccong {deriving i} ( psym  (abc= (aec-triple i<3 j<4) )) (   
+          comm {deriving i} {abc (fin≤n {3} (dba0<3 taec)) (fin≤n {4} (dba1<4 taec) )} {dba (fin≤n {3} (aec0<3 taec)) (fin≤n {4} (aec1<4 taec))}
+              ( dervie-any-3rot0 i   (fin≤n {3} (dba0<3 taec) (fin≤n {4} (dba1<4 taec)  )))
+              ( dervie-any-3rot1 i  (fin≤n {3} (aec0<3 taec) (fin≤n {4} (aec1<4 taec))))) where
         taec = aec-triple i<3 j<4
-        d2 : deriving (suc i) (aec i<3 j<4)
-        d2 = ccong {deriving i} ( psym  (abc= (aec-triple i<3 j<4) )) (   
-          comm {deriving i} {abc (fin≤n {3} (dba0<3 taec)) (fin≤n {4} (dba1<4 taec) )} {dba (fin≤n {3} (aec0<3 taec)) (fin≤n {4} (aec1<4 taec))}
-              (proj1 ( dervie-any-3rot i   (fin≤n {3} (dba0<3 taec) (fin≤n {4} (dba1<4 taec)  ))))
-              (proj1 (proj2 ( dervie-any-3rot i  (fin≤n {3} (aec0<3 taec) (fin≤n {4} (aec1<4 taec)))))))
 
      open _=p=_
      counter-example :  ¬ (abc 0<3 0<4  =p= pid )