Mercurial > hg > Members > kono > Proof > galois

comparison 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
comparison
equal deleted inserted replaced
183:0dce8a009f4a 184:59d12d02dfa8
42 42
43 stage3FList : CommFListN 3 2 ≡ cons (zero :: zero :: zero :: f0) [] (Level.lift tt) 43 stage3FList : CommFListN 3 2 ≡ cons (zero :: zero :: zero :: f0) [] (Level.lift tt)
44 stage3FList = refl 44 stage3FList = refl
45 45
46 solved1 : (x : Permutation 3 3) → deriving 2 x → x =p= pid 46 solved1 : (x : Permutation 3 3) → deriving 2 x → x =p= pid
47 solved1 x dr = CommSolved 3 x ( CommFListN 3 2 ) stage3FList pf solved2 where 47 solved1 x dr = CommSolved 3 x ( CommFListN 3 2 ) stage3FList p0id solved2 where
48 -- p0id : FL→perm ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) =p= pid
49 pf : perm→FL x ≡ FL0 → x =p= pid
50 pf eq = ptrans pf2 (ptrans pf0 p0id ) where
51 pf2 : x =p= FL→perm (perm→FL x)
52 pf2 = psym (FL←iso x)
53 pf0 : FL→perm (perm→FL x) =p= FL→perm FL0
54 pf0 = pcong-Fp eq
55 solved2 : Any (perm→FL x ≡_) ( CommFListN 3 2 ) 48 solved2 : Any (perm→FL x ≡_) ( CommFListN 3 2 )
56 solved2 = CommStage→ 3 2 x dr 49 solved2 = CommStage→ 3 2 x dr
57 50
58 51