Mercurial > hg > Members > kono > Proof > galois

changeset 312:e6e8fc55b1bf

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 22:00:32 +0900
parents 423efbcf6a09
children 12fe78751331
files src/sym5h.agda
diffstat 1 files changed, 4 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/src/sym5h.agda	Fri Sep 15 21:55:32 2023 +0900
+++ b/src/sym5h.agda	Fri Sep 15 22:00:32 2023 +0900
@@ -147,10 +147,10 @@
               dba = ?
               aec : Permutation 5 5
               aec = ?
-              Cdba : deriving (Symmetric 5) i dba
-              Cdba = ?
-              Caec : deriving (Symmetric 5) i aec
-              Caec = ?
+              Cdba : deriving (Symmetric 5) i ?
+              Cdba = Pcomm _ {dba} {?} i ?
+              Caec : deriving (Symmetric 5) i ?
+              Caec = Pcomm _ {aec} {?} 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