Mercurial > hg > Members > kono > Proof > galois

changeset 117:540d109b599c

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 Thu, 03 Sep 2020 13:40:21 +0900
parents 6022d00a0690
children 019b98d398ee
files sym5.agda
diffstat 1 files changed, 15 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- 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)))