# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1598389122 -32400
# Node ID 9cffb308269ade8188eddb13cf1431411412c1f8
# Parent  fba304a25c36d58022b1af2fe4b245c92725f999
...

diff -r fba304a25c36 -r 9cffb308269a sym5.agda
--- a/sym5.agda	Wed Aug 26 04:56:29 2020 +0900
+++ b/sym5.agda	Wed Aug 26 05:58:42 2020 +0900
@@ -56,34 +56,94 @@
 
      record Triple {i j : ℕ } (i<3 : i ≤ 3) (j<4 : j ≤ 4) : Set where
        field 
-         dba0<3 : { i : ℕ } → i < 3
-         dba1<4 : { i : ℕ } → i < 4
-         aec0<3 : { i : ℕ } → i < 3
-         aec1<4 : { i : ℕ } → i < 4
-         abc= : abc i<3 j<4 =p= [ abc dba0<3 dba1<4  , abc aec0<3 aec1<4 ]
+         dba0<3 : Fin 3
+         dba1<4 : Fin 4
+         aec0<3 : Fin 3
+         aec1<4 : Fin 4
+         abc= : abc i<3 j<4 =p= [ abc (fin<n {3} {dba0<3}) (fin<n {4} {dba1<4})  , abc (fin<n {3} {aec0<3}) (fin<n {4} {aec1<4}) ]
 
      open Triple
-     
+     --                                    d   e   a   b   c
+     t1 = plist ( abc (n≤ 0) (n≤ 0) )  -- (  ∷   ∷ 4 ∷ 2 ∷ 3 ∷ []) ∷   abc  dba 2x30x 2,4  cea x422
+       ∷  plist ( abc (n≤ 0) (n≤ 1) )  -- (  ∷   ∷ 4 ∷ 2 ∷ 3 ∷ []) ∷
+       ∷  plist ( abc (n≤ 0) (n≤ 2) )  -- (4 ∷   ∷   ∷ 0 ∷ 3 ∷ []) ∷
+       ∷  plist ( abc (n≤ 0) (n≤ 3) )  -- (4 ∷   ∷ 0 ∷   ∷ 2 ∷ []) ∷
+       ∷  plist ( abc (n≤ 0) (n≤ 4) )  -- (3 ∷   ∷ 0 ∷ 2 ∷   ∷ []) ∷
+       ∷  plist ( abc (n≤ 1) (n≤ 0) )  -- (  ∷ 4 ∷   ∷ 1 ∷ 3 ∷ []) ∷
+       ∷  plist ( abc (n≤ 1) (n≤ 1) )  -- (  ∷ 4 ∷   ∷ 1 ∷ 3 ∷ []) ∷
+       ∷  plist ( abc (n≤ 1) (n≤ 2) )  -- (4 ∷   ∷   ∷ 0 ∷ 3 ∷ []) ∷
+       ∷  plist ( abc (n≤ 1) (n≤ 3) )  -- (4 ∷ 0 ∷   ∷   ∷ 1 ∷ []) ∷
+       ∷  plist ( abc (n≤ 1) (n≤ 4) )  -- (3 ∷ 0 ∷   ∷ 1 ∷   ∷ []) ∷
+       ∷  plist ( abc (n≤ 2) (n≤ 0) )  -- (  ∷ 4 ∷ 1 ∷   ∷ 2 ∷ []) ∷
+       ∷  plist ( abc (n≤ 2) (n≤ 1) )  -- (  ∷ 4 ∷ 1 ∷   ∷ 2 ∷ []) ∷
+       ∷  plist ( abc (n≤ 2) (n≤ 2) )  -- (4 ∷ 1 ∷ 0 ∷   ∷ 2 ∷ []) ∷
+       ∷  plist ( abc (n≤ 2) (n≤ 3) )  -- (4 ∷ 0 ∷   ∷   ∷ 1 ∷ []) ∷
+       ∷  plist ( abc (n≤ 2) (n≤ 4) )  -- (2 ∷ 0 ∷ 1 ∷   ∷   ∷ []) ∷
+       ∷  plist ( abc (n≤ 3) (n≤ 0) )  -- (  ∷ 3 ∷ 1 ∷ 2 ∷   ∷ []) ∷
+       ∷  plist ( abc (n≤ 3) (n≤ 1) )  -- (  ∷ 3 ∷ 1 ∷ 2 ∷   ∷ []) ∷
+       ∷  plist ( abc (n≤ 3) (n≤ 2) )  -- (3 ∷   ∷ 0 ∷ 2 ∷   ∷ []) ∷
+       ∷  plist ( abc (n≤ 3) (n≤ 3) )  -- (3 ∷ 0 ∷   ∷ 1 ∷   ∷ []) ∷
+       ∷  plist ( abc (n≤ 3) (n≤ 4) )  -- (2 ∷ 0 ∷ 1 ∷   ∷   ∷ []) ∷   abc   dba 13204    cea 21430
+       ∷ []
+
+
+     --- 2 ∷ 0 ∷ 1 ∷ 3 ∷ 4 ∷ []     abc
+
+     --- 1 ∷ 0 ∷ 2 ∷ []
+     --- 0 ∷ 2 ∷ 1 ∷ 3 ∷ []
+     --- 1 ∷ 3 ∷ 2 ∷ 0 ∷ 4 ∷ []
+     --  2 ∷ 1 ∷ 3 ∷ 0 ∷ 4 ∷ []  (dba)⁻¹ = abd
+     dba99 = pprep (pprep (pswap (pid {1}))) ∘ₚ pins (n≤ 3)
+     tt1 = plist dba99 ∷ plist (pinv dba99) ∷ []
+     --  1 ∷ 0 ∷ []  
+     --  0 ∷ 2 ∷ 1 ∷ []  
+     --  1 ∷ 0 ∷ 3 ∷ 2 ∷ []  
+     --  2 ∷ 1 ∷ 4 ∷ 3 ∷ 0 ∷ []  
+     --  4 ∷ 1 ∷ 0 ∷ 3 ∷ 2 ∷ []  (aec)⁻¹ = cea
+     aec99 : Permutation 5 5
+     aec99 = pprep (pprep (pprep (pswap (pid {0}))) ∘ₚ pins (n≤ 1)) ∘ₚ pins (n≤ 4)
+     tt2 = plist aec99 ∷ plist (pinv aec99) ∷ []
+     tt3 = plist ([ pinv dba99 , pinv aec99 ])
+
      triple : {i j : ℕ } → (i<3 : i ≤ 3) (j<4 : j ≤ 4) → Triple i<3 j<4
-     triple = {!!}
+     triple z≤n z≤n = record { dba0<3 = {!!} ; dba1<4 = {!!} ; aec0<3 = {!!} ; aec1<4 = {!!} ; abc= = {!!} }
+     triple z≤n (s≤s z≤n) = {!!}
+     triple z≤n (s≤s (s≤s z≤n)) = {!!}
+     triple z≤n (s≤s (s≤s (s≤s z≤n))) = {!!}
+     triple z≤n (s≤s (s≤s (s≤s (s≤s z≤n)))) = {!!}
+     triple (s≤s z≤n) z≤n = {!!}
+     triple (s≤s z≤n) (s≤s z≤n) = {!!}
+     triple (s≤s z≤n) (s≤s (s≤s z≤n)) = {!!}
+     triple (s≤s z≤n) (s≤s (s≤s (s≤s z≤n))) = {!!}
+     triple (s≤s z≤n) (s≤s (s≤s (s≤s (s≤s z≤n)))) = {!!}
+     triple (s≤s (s≤s z≤n)) z≤n = {!!}
+     triple (s≤s (s≤s z≤n)) (s≤s z≤n) = {!!}
+     triple (s≤s (s≤s z≤n)) (s≤s (s≤s z≤n)) = {!!}
+     triple (s≤s (s≤s z≤n)) (s≤s (s≤s (s≤s z≤n))) = {!!}
+     triple (s≤s (s≤s z≤n)) (s≤s (s≤s (s≤s (s≤s z≤n)))) = {!!}
+     triple (s≤s (s≤s (s≤s z≤n))) z≤n = {!!}
+     triple (s≤s (s≤s (s≤s z≤n))) (s≤s z≤n) = {!!}
+     triple (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s z≤n)) = {!!}
+     triple (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s (s≤s z≤n))) = {!!}
+     triple (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s (s≤s (s≤s z≤n)))) = {!!}
 
      dervie-any-3rot : (n : ℕ ) → {i j : ℕ }  → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 ) → deriving n (abc i<3 j<4 )
      dervie-any-3rot 0 i<3 j<4 = lift tt
-     dervie-any-3rot (suc i) i<3 j<4 =  
-         ccong {deriving i} ( abc= (triple  i<3 j<4 ) ) (
-         comm {deriving i} {dba} {aec} 
-              ( dervie-any-3rot i (dba0<3 tc) (dba1<4 tc) ) 
-              ( dervie-any-3rot i (aec0<3 tc) (aec1<4 tc) )) where
-                  tc : Triple i<3 j<4
-                  tc = triple i<3 j<4
-                  dba : Permutation 5 5
-                  dba = abc (dba0<3 tc) (dba1<4   tc)
-                  aec : Permutation 5 5
-                  aec = abc (aec0<3 tc) (aec1<4   tc)
+     dervie-any-3rot (suc i) i<3 j<4 =  {!!}
+     --    ccong {deriving i} ( abc= (triple  i<3 j<4 ) ) (
+     --    comm {deriving i} {dba} {aec} 
+     --         ( dervie-any-3rot i (fin<n {3} {dba0<3 tc}) (fin<n {4} {dba1<4 tc}) ) 
+     --         ( dervie-any-3rot i (fin<n {3} {aec0<3 tc}) (fin<n {4} {aec1<4 tc}) )) where
+     --             tc : Triple i<3 j<4
+     --             tc = triple i<3 j<4
+     --             dba : Permutation 5 5
+     --             dba = abc (fin<n {3} {dba0<3 tc}) (fin<n {4} {dba1<4   tc})
+     --             aec : Permutation 5 5
+     --             aec = abc (fin<n {3} {aec0<3 tc}) (fin<n {4} {aec1<4   tc})
 
      open _=p=_
      counter-example :  ¬ (abc 0<3 0<4  =p= pid )
-     counter-example p with peq p (# 1)
-     ...  | ()
+     counter-example = {!!} -- p with peq p (# 1)
+     -- ...  | ()