# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1599108021 -32400
# Node ID 540d109b599c451c0c0df4aa02fc3e65019e937f
# Parent  6022d00a0690aaa2841f269c9902bd9dd58014d9
...

diff -r 6022d00a0690 -r 540d109b599c sym5.agda
--- a/sym5.agda	Thu Sep 03 11:45:42 2020 +0900
+++ b/sym5.agda	Thu Sep 03 13:40:21 2020 +0900
@@ -198,8 +198,21 @@
         tc = triple i<3 j<4
         dba0 = dba (fin≤n {3} (dba0<3 tc)) (fin≤n {4} (dba1<4 tc))
         aec0 = dba (fin≤n {3} (aec0<3 tc)) (fin≤n {4} (aec1<4 tc))
+        --
+        -- abc= : ins2 rot i<3 j<4 =p= [ ins2 (rot ∘ₚ rot)  (fin≤n {3} dba0<3) (fin≤n {4} dba1<4)  , ins2 (rot ∘ₚ rot) (fin≤n {3} aec0<3) (fin≤n {4} aec1<4) ]
+        --
+        ceq'  : ins2 3rot i<3 j<4 =p= [ ins2 (3rot ∘ₚ 3rot)  (fin≤n {3} (dba0<3 tc)) (fin≤n {4} (dba1<4 tc))  , ins2 (3rot ∘ₚ 3rot) (fin≤n {3} (aec0<3 tc )) (fin≤n {4} (aec1<4 tc)) ]
+        ceq'  = abc= tc
         ceq : abc i<3 j<4  =p=  [ dba0 , aec0 ]  
-        ceq = {!!} -- abc= tc
+        ceq = record { peq = λ q → begin 
+                 abc i<3 j<4 ⟨$⟩ʳ q
+              ≡⟨ peq (abc= tc) q ⟩
+                 [ ins2 (3rot ∘ₚ 3rot) (fin≤n (dba0<3 tc)) (fin≤n (dba1<4 tc)) , ins2 (3rot ∘ₚ 3rot) (fin≤n (aec0<3 tc)) (fin≤n (aec1<4 tc)) ] ⟨$⟩ʳ q
+              ≡⟨ {!!} ⟩
+                 {!!}
+              ≡⟨ {!!} ⟩
+                 [ dba0 , aec0 ] ⟨$⟩ʳ q
+              ∎ }
         df =  dervie-any-3rot1 i  (fin≤n {3} (dba0<3 tc)) (fin≤n {4} (dba1<4 tc))
         dg =  dervie-any-3rot1 i  (fin≤n {3} (aec0<3 tc)) (fin≤n {4} (aec1<4 tc)) 
 
@@ -209,7 +222,7 @@
         aec0 = ins2 ((3rot ∘ₚ 3rot) ∘ₚ (3rot ∘ₚ 3rot )) (fin≤n {3} (dba0<3 tdba)) (fin≤n {4} (dba1<4 tdba))
         abc0 = ins2 ((3rot ∘ₚ 3rot) ∘ₚ (3rot ∘ₚ 3rot )) (fin≤n {3} (aec0<3 tdba)) (fin≤n {4} (aec1<4 tdba))
         ceq : dba i<3 j<4 =p=  [ aec0 , abc0 ]  
-        ceq = abc= tdba
+        ceq = {!!} -- abc= tdba
         df : deriving n (ins2 ((3rot ∘ₚ 3rot) ∘ₚ (3rot ∘ₚ 3rot )) (fin≤n {3} (dba0<3 tdba)) (fin≤n {4} (dba1<4 tdba)))
         df = deriving-subst (psym (ins2cong {toℕ (dba0<3 (dba-triple i<3 j<4))} {toℕ (dba1<4 (dba-triple i<3 j<4))} 4=1 ))
              (dervie-any-3rot0 n  (fin≤n {3} (dba0<3 tdba)) (fin≤n {4} (dba1<4 tdba)))