# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1599214059 -32400
# Node ID 803a45b280ef85f56326c20bf5bbffd743b22de8
# Parent  465c42c9a99ef4712e31d4673bd15b41f84227a4
...

diff -r 465c42c9a99e -r 803a45b280ef sym3.agda
--- a/sym3.agda	Fri Sep 04 18:33:25 2020 +0900
+++ b/sym3.agda	Fri Sep 04 19:07:39 2020 +0900
@@ -97,18 +97,24 @@
 --       ∎ ) }
 
    st02 :  ( g h : Permutation 3 3) →  ([ g , h ] =p= pid) ∨ ([ g , h ] =p= p3) ∨ ([ g , h ] =p= p4)
-   st02 = {!!}
---   st02 g h with perm→FL g | perm→FL h | inspect perm→FL g | inspect perm→FL h
---   ... | (zero :: (zero :: (zero :: f0))) | t | record { eq = ge } | te = case1 (ptrans (comm-resp {g} {h} {pid} (FL-inject ge ) prefl ) (idcomtl h) )
---   ... | s | (zero :: (zero :: (zero :: f0))) | se |  record { eq = he } = case1 (ptrans (comm-resp {g} {h} {_} {pid} prefl (FL-inject he ))(idcomtr g) )
---   ... | (zero :: (suc zero) :: (zero :: f0 )) |  (zero :: (suc zero) :: (zero :: f0 )) |  record { eq = ge } |  record { eq = he } = {!!}
---   ... | (suc zero) :: (zero :: (zero :: f0 )) | (suc zero) :: (zero :: (zero :: f0 )) |  record { eq = ge } |  record { eq = he } = {!!}
---   ... | (suc zero) :: (suc zero :: (zero :: f0 )) |  (suc zero) :: (suc zero :: (zero :: f0 )) |  record { eq = ge } |  record { eq = he } = {!!}
---   ... | (zero :: (suc zero) :: (zero :: f0 )) | t | se | te = {!!}
---   ... | (suc zero) :: (zero :: (zero :: f0 )) | t | se | te = {!!}
---   ... | (suc zero) :: (suc zero :: (zero :: f0 )) | t | se | te = {!!}
---   ... | (suc (suc zero)) :: (zero :: (zero :: f0 )) | t | se | te = {!!}
---   ... | (suc (suc zero)) :: (suc zero) :: (zero :: f0) | t | se | te = {!!}
+   st02 g h with perm→FL g | perm→FL h | inspect perm→FL g | inspect perm→FL h
+   ... | (zero :: (zero :: (zero :: f0))) | t | record { eq = ge } | te = case1 (ptrans (comm-resp {g} {h} {pid} (FL-inject ge ) prefl ) (idcomtl h) )
+   ... | s | (zero :: (zero :: (zero :: f0))) | se |  record { eq = he } = case1 (ptrans (comm-resp {g} {h} {_} {pid} prefl (FL-inject he ))(idcomtr g) )
+   ... | (zero :: (suc zero) :: (zero :: f0 )) |  (zero :: (suc zero) :: (zero :: f0 )) |  record { eq = ge } |  record { eq = he } =
+        case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )
+   ... | (suc zero) :: (zero :: (zero :: f0 )) | (suc zero) :: (zero :: (zero :: f0 )) |  record { eq = ge } |  record { eq = he } = 
+        case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )
+   ... | (suc zero) :: (suc zero :: (zero :: f0 )) |  (suc zero) :: (suc zero :: (zero :: f0 )) |  record { eq = ge } |  record { eq = he } = 
+        case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )
+   ... | (suc (suc zero)) :: (zero :: (zero :: f0 )) | (suc (suc zero)) :: (zero :: (zero :: f0 )) | record { eq = ge } |  record { eq = he } =
+        case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )
+   ... | (suc (suc zero)) :: (suc zero) :: (zero :: f0) | (suc (suc zero)) :: (suc zero) :: (zero :: f0) | record { eq = ge } |  record { eq = he } =
+        case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )
+   ... | (zero :: (suc zero) :: (zero :: f0 )) | t | se | te = {!!}
+   ... | (suc zero) :: (zero :: (zero :: f0 )) | t | se | te = {!!}
+   ... | (suc zero) :: (suc zero :: (zero :: f0 )) | t | se | te = {!!}
+   ... | (suc (suc zero)) :: (zero :: (zero :: f0 )) | t | se | te = {!!}
+   ... | (suc (suc zero)) :: (suc zero) :: (zero :: f0) | t | se | te = {!!}
    
    stage12  :  (x : Permutation 3 3) → stage1 x →  ( x =p= pid ) ∨ ( x =p= p3 ) ∨ ( x =p= p4 )
    stage12 = {!!}
@@ -152,13 +158,14 @@
           ≡⟨ f=e q ⟩
              q
           ∎ 
-   solved1 _ (comm {g} {h} x y) with stage12 g x | stage12 h y
-   ... | case1 t | case1 s = ptrans (comm-resp t s) (comm-refl {pid} prefl)
-   ... | case1 t | case2 s = ptrans (comm-resp {g} {h} {pid} t prefl) (idcomtl h)
-   ... | case2 t | case1 s = ptrans (comm-resp {g} {h} {_} {pid} prefl s) (idcomtr g)
-   ... | case2 (case1 t) | case2 (case1 s) = record { peq = λ q → trans ( peq ( comm-resp {g} {h}  t s ) q ) (peq com33 q) }
-   ... | case2 (case2 t) | case2 (case2 s) = record { peq = λ q → trans ( peq ( comm-resp {g} {h}  t s ) q ) (peq com44 q) }
-   ... | case2 (case1 t) | case2 (case2 s) = record { peq = λ q → trans ( peq ( comm-resp {g} {h}  t s ) q ) (peq com34 q) }
-   ... | case2 (case2 t) | case2 (case1 s) = record { peq = λ q → trans ( peq ( comm-resp {g} {h}  t s ) q ) (peq com43 q) }
+   solved1 _ (comm {g} {h} x y) = {!!}
+--   solved1 _ (comm {g} {h} x y) with stage12 g x | stage12 h y
+--   ... | case1 t | case1 s = ptrans (comm-resp t s) (comm-refl {pid} prefl)
+--   ... | case1 t | case2 s = ptrans (comm-resp {g} {h} {pid} t prefl) (idcomtl h)
+--   ... | case2 t | case1 s = ptrans (comm-resp {g} {h} {_} {pid} prefl s) (idcomtr g)
+--   ... | case2 (case1 t) | case2 (case1 s) = record { peq = λ q → trans ( peq ( comm-resp {g} {h}  t s ) q ) (peq com33 q) }
+--   ... | case2 (case2 t) | case2 (case2 s) = record { peq = λ q → trans ( peq ( comm-resp {g} {h}  t s ) q ) (peq com44 q) }
+--   ... | case2 (case1 t) | case2 (case2 s) = record { peq = λ q → trans ( peq ( comm-resp {g} {h}  t s ) q ) (peq com34 q) }
+--   ... | case2 (case2 t) | case2 (case1 s) = record { peq = λ q → trans ( peq ( comm-resp {g} {h}  t s ) q ) (peq com43 q) }
 
    -- = ptrans ( comm-resp {g} {h}  t s ) ( comm-refl ? )