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

diff -r 9cffb308269a -r 75e2dd8f4e00 sym5.agda
--- a/sym5.agda	Wed Aug 26 05:58:42 2020 +0900
+++ b/sym5.agda	Wed Aug 26 12:31:04 2020 +0900
@@ -45,14 +45,22 @@
      0<3 : 0 < 3
      0<3 = s≤s z≤n
 
-     --- 2 ∷ 0 ∷ 1 ∷ []      abc
+     --- 1 ∷ 2 ∷ 0 ∷ []      abc
      3rot : Permutation 3 3
-     3rot = pprep (pswap (pid {0}) ) ∘ₚ pins (n≤ 1)
+     3rot = pid {3} ∘ₚ pins (n≤ 2)
+
+     ins2 : {i j : ℕ }  → Permutation 3 3  → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation  5 5
+     ins2 abc i<3 j<4 = (save2 ∘ₚ (pprep (pprep abc))) ∘ₚ flip save2  where
+          save2 : Permutation  5 5
+          save2 = ( (( pid {5} ∘ₚ flip (pins (s≤s i<3) ) )) ∘ₚ flip (pins j<4)) 
 
      abc : {i j : ℕ }  → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation  5 5
-     abc i<3 j<4 = (save2 ∘ₚ (pprep (pprep 3rot))) ∘ₚ flip save2  where
-          save2 : Permutation  5 5
-          save2 = ( (( pid {5} ∘ₚ flip (pins (s≤s i<3) ) )) ∘ₚ flip (pins j<4)) 
+     abc i<3 j<4 = ins2 3rot i<3 j<4
+
+     dba : {i j : ℕ }  → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation  5 5
+     dba i<3 j<4 = ins2 (3rot ∘ₚ 3rot) i<3 j<4
+     aec : {i j : ℕ }  → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation  5 5
+     aec i<3 j<4 = ins2 (pinv 3rot) i<3 j<4
 
      record Triple {i j : ℕ } (i<3 : i ≤ 3) (j<4 : j ≤ 4) : Set where
        field 
@@ -60,50 +68,54 @@
          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}) ]
+         abc= : abc i<3 j<4 =p= [ dba (fin<n {3} {dba0<3}) (fin<n {4} {dba1<4})  , aec (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
+     t1 = plist ( abc (n≤ 0) (n≤ 0) )  -- (  ∷   ∷ 3 ∷ 4 ∷ 2 ∷ []) ∷    no 4 on top
+       ∷  plist ( abc (n≤ 0) (n≤ 1) )  -- (  ∷   ∷ 3 ∷ 4 ∷ 2 ∷ []) ∷ 
+       ∷  plist ( abc (n≤ 0) (n≤ 2) )  -- (3 ∷   ∷   ∷ 4 ∷ 0 ∷ []) ∷
+       ∷  plist ( abc (n≤ 0) (n≤ 3) )  -- (2 ∷   ∷ 4 ∷   ∷ 0 ∷ []) ∷   
+       ∷  plist ( abc (n≤ 0) (n≤ 4) )  -- (2 ∷   ∷ 3 ∷ 0 ∷   ∷ []) ∷  
+       ∷  plist ( abc (n≤ 1) (n≤ 0) )  -- (  ∷ 3 ∷   ∷ 4 ∷ 1 ∷ []) ∷ 
+       ∷  plist ( abc (n≤ 1) (n≤ 1) )  -- (  ∷ 3 ∷   ∷ 4 ∷ 1 ∷ []) ∷
+       ∷  plist ( abc (n≤ 1) (n≤ 2) )  -- (3 ∷   ∷   ∷ 4 ∷ 0 ∷ []) ∷   
+       ∷  plist ( abc (n≤ 1) (n≤ 3) )  -- (1 ∷ 4 ∷   ∷   ∷ 0 ∷ []) ∷  
+       ∷  plist ( abc (n≤ 1) (n≤ 4) )  -- (1 ∷ 3 ∷   ∷ 0 ∷   ∷ []) ∷ 
+       ∷  plist ( abc (n≤ 2) (n≤ 0) )  -- (  ∷ 2 ∷ 4 ∷   ∷ 1 ∷ []) ∷
+       ∷  plist ( abc (n≤ 2) (n≤ 1) )  -- (  ∷ 2 ∷ 4 ∷   ∷ 1 ∷ []) ∷   
+       ∷  plist ( abc (n≤ 2) (n≤ 2) )  -- (2 ∷   ∷ 4 ∷   ∷ 0 ∷ []) ∷  
+       ∷  plist ( abc (n≤ 2) (n≤ 3) )  -- (1 ∷ 4 ∷   ∷   ∷ 0 ∷ []) ∷ 
+       ∷  plist ( abc (n≤ 2) (n≤ 4) )  -- (1 ∷ 2 ∷ 0 ∷   ∷   ∷ []) ∷
+       ∷  plist ( abc (n≤ 3) (n≤ 0) )  -- (  ∷ 2 ∷ 3 ∷ 1 ∷   ∷ []) ∷   
+       ∷  plist ( abc (n≤ 3) (n≤ 1) )  -- (  ∷ 2 ∷ 3 ∷ 1 ∷   ∷ []) ∷  
+       ∷  plist ( abc (n≤ 3) (n≤ 2) )  -- (2 ∷   ∷ 3 ∷ 0 ∷   ∷ []) ∷ 
+       ∷  plist ( abc (n≤ 3) (n≤ 3) )  -- (1 ∷ 3 ∷   ∷ 0 ∷   ∷ []) ∷
+       ∷  plist ( abc (n≤ 3) (n≤ 4) )  -- (1 ∷ 2 ∷ 0 ∷   ∷   ∷ []) ∷ []
        ∷ []
 
 
-     --- 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)
+     --- 1 ∷ 2 ∷ 0 ∷   ∷   ∷ []      abc    --  abc (n≤ 3) (n≤ 4)
+     --- 3 ∷ 0 ∷   ∷ 1 ∷   ∷ []      dba
+     dba99 = ins2 (3rot ∘ₚ 3rot) (n≤ 1) (n≤ 4)
+     --- 4 ∷   ∷ 0 ∷   ∷ 2 ∷ []      aec
+     aec99 = ins2 (pinv 3rot) (n≤ 0) (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 ])
+     tt5 = plist  [ dba99 , aec99  ]  -- =p=  abc  
+     tt6 : [ dba99 , aec99  ]  =p=  abc (n≤ 3) (n≤ 4)
+     tt6 = record { peq = λ q → lll q } where
+        lll : (q : Fin 5) →  ([ dba99 , aec99 ] ⟨$⟩ʳ q) ≡ (abc (n≤ 3) (n≤ 4) ⟨$⟩ʳ q)
+        lll zero = refl
+        lll (suc zero) = refl
+        lll (suc (suc zero)) = refl
+        lll (suc (suc (suc zero))) = refl
+        lll (suc (suc (suc (suc zero)))) = refl
+     tt8  = plist ( dba (fin<n  {3} {# 0}) (fin<n  {4} {# 3}))
+     tt9  : fin<n  {4} {# 3} ≡ n≤ 4
+     tt9  = refl
+     tta  : fin<n  {3} {# 0} ≡ n≤ 1
+     tta  = refl
 
      triple : {i j : ℕ } → (i<3 : i ≤ 3) (j<4 : j ≤ 4) → Triple i<3 j<4
      triple z≤n z≤n = record { dba0<3 = {!!} ; dba1<4 = {!!} ; aec0<3 = {!!} ; aec1<4 = {!!} ; abc= = {!!} }
@@ -125,7 +137,18 @@
      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)))) = {!!}
+     triple (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s (s≤s (s≤s z≤n)))) = ?
+     --   record { dba0<3 = # 0 ; dba1<4 = # 3 ; aec0<3 = # 0 ; aec1<4 = # 3 ; abc= = ? } 
+     --        tt7 : abc (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s (s≤s (s≤s z≤n)))) =p=
+     --              [ dba (fin<n  {3} {# 1})(fin<n  {4} {# 4}) , aec (fin<n  {3} {# 0}) (fin<n {4} {# 3})  ]  
+     --        tt7 = record { peq = λ q → lll q } where
+     --           lll : (q : Fin 5) →  {!!}
+     --           lll zero = {!!}
+     --           lll (suc zero) = refl
+     --           lll (suc (suc zero)) = {!!}
+     --           lll (suc (suc (suc zero))) = {!!}
+     --           lll (suc (suc (suc (suc zero)))) = refl
+
 
      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