Mercurial > hg > Members > kono > Proof > galois

changeset 313:12fe78751331

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 Fri, 15 Sep 2023 23:36:43 +0900
parents e6e8fc55b1bf
children 891869ead775
files src/sym5h.agda
diffstat 1 files changed, 2 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/src/sym5h.agda	Fri Sep 15 22:00:32 2023 +0900
+++ b/src/sym5h.agda	Fri Sep 15 23:36:43 2023 +0900
@@ -148,9 +148,9 @@
               aec : Permutation 5 5
               aec = ?
               Cdba : deriving (Symmetric 5) i ?
-              Cdba = Pcomm _ {dba} {?} i ?
+              Cdba = Pcomm _ {pprep (pprep abc)} {?} i ?
               Caec : deriving (Symmetric 5) i ?
-              Caec = Pcomm _ {aec} {?} i ?
+              Caec = Pcomm _ {pinv (pprep (pprep abc))} {?} i ?
               s18 :  iCommutator (Symmetric 5) (suc i) (pprep (pprep abc))
               s18 = iunit (ccong ? ( comm Cdba Caec ))
            s17 : (abc : Permutation 3 3 ) →  s15 (s16 abc) =p= abc