--- a/sym3n.agda	Thu Nov 26 08:58:12 2020 +0900
+++ b/sym3n.agda	Thu Nov 26 13:13:58 2020 +0900
@@ -37,83 +37,22 @@
    p0id :  FL→perm ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) =p= pid
    p0id = pleq _ _ refl
 
-   t1  : FList 3 →  FList 3
-   t1  x =  tl2 x x [] where
-       tl3 : (FL 3) → ( z : FList 3) → FList 3 → FList 3
-       tl3 h [] w = w
-       tl3 h (x ∷# z) w = tl3 h z (FLinsert ( perm→FL [ FL→perm h , FL→perm x ] ) w )
-       tl2 : ( x z : FList 3) → FList 3 →  FList 3
-       tl2 [] _ x = x
-       tl2 (h ∷# x) z w = tl2 x z (tl3 h z w)
+   open import Data.List.Fresh.Relation.Unary.Any
+   open import FLComm
 
-   stage10  :  FList 3
-   stage10  =  {!!} -- t1 (Flist (fmax ))
-
-   p0 =  FL→perm ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) 
-   p1 =  FL→perm ((# 0) :: ((# 1) :: ((# 0 ) :: f0))) 
-   p2 =  FL→perm ((# 1) :: ((# 0) :: ((# 0 ) :: f0))) 
-   p3 =  FL→perm ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) 
-   p4 =  FL→perm ((# 2) :: ((# 0) :: ((# 0 ) :: f0))) 
-   p5 =  FL→perm ((# 2) :: ((# 1) :: ((# 0 ) :: f0))) 
-   t0  =  plist p0 ∷ plist p1 ∷  plist p2 ∷ plist p3 ∷ plist p4 ∷  plist p5 ∷ [] 
+   stage3FList : CommFListN 3 2 ≡ cons (zero :: zero :: zero :: f0) [] (Level.lift tt)
+   stage3FList = refl
 
-   tt4  = plist [ p0 , p0 ] ∷ plist [ p1 , p0 ] ∷  plist [ p2 , p0 ] ∷ plist [ p3 , p0 ] ∷ plist [ p4 , p0 ] ∷  plist [ p5 , p1 ] ∷ 
-          plist [ p0 , p1 ] ∷ plist [ p1 , p1 ] ∷  plist [ p2 , p1 ] ∷ plist [ p3 , p1 ] ∷ plist [ p4 , p1 ] ∷  plist [ p5 , p1 ] ∷ 
-          plist [ p0 , p2 ] ∷ plist [ p1 , p2 ] ∷  plist [ p2 , p2 ] ∷ plist [ p3 , p2 ] ∷ plist [ p4 , p2 ] ∷  plist [ p5 , p2 ] ∷ 
-          plist [ p0 , p3 ] ∷ plist [ p1 , p3 ] ∷  plist [ p3 , p3 ] ∷ plist [ p3 , p3 ] ∷ plist [ p4 , p3 ] ∷  plist [ p5 , p3 ] ∷ 
-          plist [ p0 , p4 ] ∷ plist [ p1 , p4 ] ∷  plist [ p3 , p4 ] ∷ plist [ p3 , p4 ] ∷ plist [ p4 , p4 ] ∷  plist [ p5 , p4 ] ∷ 
-          plist [ p0 , p5 ] ∷ plist [ p1 , p5 ] ∷  plist [ p3 , p5 ] ∷ plist [ p3 , p5 ] ∷ plist [ p4 , p4 ] ∷  plist [ p5 , p5 ] ∷ 
-          []
-
-   open _=p=_
-   
-   stage1 :  (x : Permutation 3 3) →  Set (Level.suc Level.zero)
-   stage1 x = Commutator (λ x₂ → Lift (Level.suc Level.zero) ⊤)  x 
-
-   open import logic
-
-   pFL : ( g : Permutation 3 3) → { x : FL 3 } →  perm→FL g ≡ x → g =p=  FL→perm x
-   pFL g {x} refl = ptrans (psym (FL←iso g)) ( FL-inject refl ) 
-
-   open ≡-Reasoning
-
---   st01 : ( x y : Permutation 3 3) →   x =p= p3 →  y =p= p3 → x ∘ₚ  y =p= p4 
---   st01 x y s t = record { peq = λ q → ( begin
---         (x ∘ₚ y) ⟨$⟩ʳ q
---       ≡⟨ peq ( presp s t ) q ⟩
---          ( p3  ∘ₚ p3 ) ⟨$⟩ʳ q
---       ≡⟨ peq  p33=4 q  ⟩
---         p4 ⟨$⟩ʳ q
---       ∎ ) }
-
-   st00 = perm→FL [ FL→perm ((suc zero) :: (suc zero :: (zero :: f0 ))) , FL→perm  ((suc (suc zero)) :: (suc zero) :: (zero :: f0))  ]
-
-   
-   stage12  :  (x : Permutation 3 3) → stage1 x →  ( x =p= pid ) ∨ ( x =p= p3 ) ∨ ( x =p= p4 )
-   stage12 = {!!}
+   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
+      solved2 : Any (perm→FL x ≡_) ( CommFListN 3 2 )
+      solved2 = CommStage→ 3 2 x dr
 
 
-   solved1 :  (x : Permutation 3 3) →  Commutator (λ x₁ → Commutator (λ x₂ → Lift (Level.suc Level.zero) ⊤) x₁) x → x =p= pid
-   solved1 _ uni = prefl
-   solved1 x (gen {f} {g} d d₁) with solved1 f d | solved1 g d₁
-   ... | record { peq = f=e } | record { peq = g=e } = record { peq = λ q → genlem q } where
-      genlem : ( q : Fin 3 ) → g ⟨$⟩ʳ ( f ⟨$⟩ʳ q ) ≡ q
-      genlem q = begin
-             g ⟨$⟩ʳ ( f ⟨$⟩ʳ q )
-          ≡⟨ g=e ( f ⟨$⟩ʳ q ) ⟩
-             f ⟨$⟩ʳ q 
-          ≡⟨ f=e q ⟩
-             q
-          ∎ 
-   solved1 x (ccong {f} {g} (record {peq = f=g}) d) with solved1 f d
-   ... | record { peq = f=e }  =  record  { peq = λ q → cc q } where
-      cc : ( q : Fin 3 ) → x ⟨$⟩ʳ q ≡ q
-      cc q = begin
-             x ⟨$⟩ʳ q
-          ≡⟨ sym (f=g q) ⟩
-             f ⟨$⟩ʳ q
-          ≡⟨ f=e q ⟩
-             q
-          ∎ 
-   solved1 _ (comm {g} {h} x y) = {!!}
-