Mercurial > hg > Members > kono > Proof > galois

diff sym3n.agda @ 184:59d12d02dfa8

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, 26 Nov 2020 14:09:54 +0900
parents eb94265d2a39
children
line wrap: on
line diff
--- a/sym3n.agda	Thu Nov 26 13:19:42 2020 +0900
+++ b/sym3n.agda	Thu Nov 26 14:09:54 2020 +0900
@@ -44,14 +44,7 @@
    stage3FList = refl
 
    solved1 :  (x : Permutation 3 3) → deriving 2 x → x =p= pid
-   solved1 x dr = CommSolved 3 x ( CommFListN 3 2 ) stage3FList pf solved2 where
-      --    p0id :  FL→perm ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) =p= pid
-      pf : perm→FL x ≡ FL0 → x =p= pid
-      pf eq = ptrans pf2 (ptrans pf0 p0id ) where
-         pf2 : x =p= FL→perm (perm→FL x)
-         pf2 = psym (FL←iso x)
-         pf0 : FL→perm (perm→FL x) =p= FL→perm FL0
-         pf0 = pcong-Fp eq
+   solved1 x dr = CommSolved 3 x ( CommFListN 3 2 ) stage3FList p0id solved2 where
       solved2 : Any (perm→FL x ≡_) ( CommFListN 3 2 )
       solved2 = CommStage→ 3 2 x dr