Mercurial > hg > Members > kono > Proof > galois

changeset 118:019b98d398ee

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
sym5 done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 03 Sep 2020 14:06:18 +0900
parents 540d109b599c
children 2dae51792e1a
files sym5.agda
diffstat 1 files changed, 2 insertions(+), 12 deletions(-) [+]
line wrap: on
line diff
--- a/sym5.agda	Thu Sep 03 13:40:21 2020 +0900
+++ b/sym5.agda	Thu Sep 03 14:06:18 2020 +0900
@@ -74,8 +74,6 @@
      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) (rot : Permutation 3 3) : Set where
        field 
@@ -204,15 +202,7 @@
         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 = 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
-              ∎ }
+        ceq = record { peq = peq (abc= tc) }
         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)) 
 
@@ -222,7 +212,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 = record { peq = peq (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)))