Mercurial > hg > Members > kono > Proof > galois

changeset 182:eb94265d2a39 fresh-list

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Any based proof computation done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 26 Nov 2020 13:13:58 +0900
parents 7423f0fc124a
children 0dce8a009f4a
files FLComm.agda FLutil.agda Putil.agda sym2n.agda sym3n.agda sym4.agda
diffstat 6 files changed, 153 insertions(+), 165 deletions(-) [+]
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/FLComm.agda	Thu Nov 26 13:13:58 2020 +0900
@@ -0,0 +1,57 @@
+{-# OPTIONS --allow-unsolved-metas #-}
+open import Data.Nat -- using (ℕ; suc; zero; s≤s ; z≤n )
+module FLComm (n : ℕ) where
+
+open import Level renaming ( suc to Suc ; zero to Zero ) hiding (lift)
+open import Data.Fin hiding ( _<_  ; _≤_ ; _-_ ; _+_ ; _≟_)
+open import Data.Fin.Properties hiding ( <-trans ; ≤-refl ; ≤-trans ; ≤-irrelevant ; _≟_ ) renaming ( <-cmp to <-fcmp )
+open import Data.Fin.Permutation  
+open import Data.Nat.Properties 
+open import Relation.Binary.PropositionalEquality hiding ( [_] )
+open import Data.List using (List; []; _∷_ ; length ; _++_ ; tail ) renaming (reverse to rev )
+open import Data.Product hiding (_,_ )
+open import Relation.Nullary 
+open import Data.Unit
+open import Data.Empty
+open import  Relation.Binary.Core 
+open import  Relation.Binary.Definitions hiding (Symmetric )
+open import logic
+open import nat
+
+open import FLutil
+open import Putil
+import Solvable 
+open import Symmetric
+
+-- infixr  100 _::_
+
+open import Data.List.Fresh hiding ([_])
+open import Data.List.Fresh.Relation.Unary.Any
+
+open Solvable (Symmetric n)
+
+CommFList  :  FList n →  FList n
+CommFList x =  tl2 x x [] where
+   tl3 : (FL n) → ( z : FList n) → FList n → FList n
+   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 n) → FList n →  FList n
+   tl2 [] _ x = x
+   tl2 (h ∷# x) z w = tl2 x z (tl3 h z w)
+
+CommFListN  : ℕ  →  FList n
+CommFListN  0 = ∀Flist fmax
+CommFListN  (suc i) = CommFList (CommFListN i)
+
+open import Algebra 
+open Group (Symmetric n)
+
+CommStage→ : (i : ℕ) → (x : Permutation n n ) → deriving i x → Any (perm→FL x ≡_) ( CommFListN i )
+CommStage→ zero x (Level.lift tt) = AnyFList (perm→FL x)
+CommStage→ (suc i) x uni = {!!}
+CommStage→ (suc i) x (comm {g} {h} p q) = {!!}
+CommStage→ (suc i) x (gen {f} {g} p q) = {!!}
+CommStage→ (suc i) x (ccong {f} {g} eq p) = {!!}
+
+CommSolved : (x : Permutation n n) → (y : FList n) → y ≡ FL0 ∷# [] → (perm→FL x ≡ FL0 → x =p= pid ) → Any (perm→FL x ≡_) y → x =p= pid
+CommSolved x .(cons FL0 [] (Level.lift tt)) refl fl0→pid (here eq) = fl0→pid eq
--- a/FLutil.agda	Thu Nov 26 08:58:12 2020 +0900
+++ b/FLutil.agda	Thu Nov 26 13:13:58 2020 +0900
@@ -231,23 +231,10 @@
 -- fr7 = append ( ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) ∷# [] ) fr1 ( ({!!} , {!!} ) ∷ [] )
 
 Flist :  {n : ℕ } (i : ℕ) → i < suc n → FList n → FList n → FList (suc n)
-Ffresh0 : {n : ℕ } → (i<n : zero < suc n) → (a : FL n) → (x z : FList n )
-    →  fresh (FL n) ⌊ _f<?_ ⌋ a x →  fresh (FL (suc n)) ⌊ _f<?_ ⌋ (zero :: a) (Flist zero i<n x z)
-Ffresh1 : {n : ℕ } → (i : ℕ) → (i<n : i < suc n) → 0 < i → (a : FL n) → (x z : FList n )
-     →  (a₂ : FL (suc n)) (t : FList (suc n)) → fresh (FL (suc n)) ⌊ _f<?_ ⌋ a₂ t 
-     →  fresh (FL n) ⌊ _f<?_ ⌋ a x →  fresh (FL (suc n)) ⌊ _f<?_ ⌋ (fromℕ< i<n :: a) t
 Flist zero i<n [] _ = []
-Flist zero i<n (cons a x xr) z  = cons ( zero :: a ) (Flist zero i<n x z ) (Ffresh0 i<n a x z xr)
+Flist zero i<n (a ∷# x ) z  = FLinsert ( zero :: a ) (Flist zero i<n x z )
 Flist (suc i) (s≤s i<n) [] z  = Flist i (<-trans i<n a<sa) z z 
-Flist (suc i) (s≤s i<n) (cons a [] xr) z = cons ((fromℕ< (s≤s i<n)) :: a) (Flist i (<-trans i<n a<sa) z z)  {!!}
-Flist (suc i) (s≤s i<n) (cons a (cons a₁ x x₁) xr) z with Flist (suc i) (s≤s i<n) x z 
-... | [] = cons ((fromℕ< (s≤s i<n)) :: a) [] (Level.lift tt)
-... | cons a₂ t x₂ = cons ((fromℕ< (s≤s i<n)) :: a) t (Ffresh1 (suc i) (s≤s i<n) 0<s a x z a₂ t x₂ ?)
-Ffresh0 i<n a [] z xr = Level.lift tt
-Ffresh0 i<n a (cons a₁ x x₁) z (lift a<a₁ , ar) = Fr0 , Ffresh0 i<n a x z ar where
-   Fr0 : ⌊ _f<?_ ⌋ (zero :: a) (zero :: a₁)
-   Fr0 = Level.lift (fromWitness (f<t (toWitness a<a₁)))
-Ffresh1 = {!!}
+Flist (suc i) i<n (a ∷# x ) z  = FLinsert ((fromℕ< i<n ) :: a ) (Flist (suc i) i<n x z )
 
 ∀Flist : {n : ℕ } → FL n → FList n
 ∀Flist {zero} f0 = f0 ∷# [] 
@@ -265,9 +252,6 @@
 open import Data.List.Fresh.Relation.Unary.Any 
 open import Data.List.Fresh.Relation.Unary.All 
 
-AnyFList : {n : ℕ }  → (x : FL (suc n) ) →  Any (x ≡_ ) (∀Flist fmax)
-AnyFList {n} = {!!}
-
 x∈FLins : {n : ℕ} → (x : FL n ) → (xs : FList n)  → Any (x ≡_ ) (FLinsert x xs)
 x∈FLins {zero} f0 [] = here refl
 x∈FLins {zero} f0 (cons f0 xs x) = here refl
@@ -282,15 +266,8 @@
 nextAny (here x₁) = there (here x₁)
 nextAny (there any) = there (there any)
 
-record ∀FListP (n : ℕ ) : Set (Level.suc Level.zero) where
-  field
-    ∀list :   FList n 
-    x∈∀list : (x : FL n ) → Any (x ≡_ ) ∀list 
-
-open ∀FListP
-
--- tt1 : FList 3
--- tt1 = ∀FListP.∀list (∀FList 3)
+postulate
+   AnyFList : {n : ℕ }  → (x : FL n ) →  Any (x ≡_ ) (∀Flist fmax)
 
 -- FLinsert membership
 
--- a/Putil.agda	Thu Nov 26 08:58:12 2020 +0900
+++ b/Putil.agda	Thu Nov 26 13:13:58 2020 +0900
@@ -676,6 +676,7 @@
         h ⟨$⟩ʳ q
      ∎  ) }
 
+-- FLpid : (n : ℕ) → (x : Permutation n n) → perm→FL x ≡ FL0 → x =p= pid
 
 lem2 : {i n : ℕ } → i ≤ n → i ≤ suc n
 lem2 i≤n = ≤-trans i≤n ( a≤sa )
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/sym2n.agda	Thu Nov 26 13:13:58 2020 +0900
@@ -0,0 +1,58 @@
+open import Level hiding ( suc ; zero )
+open import Algebra
+module sym2n where
+
+open import Symmetric 
+open import Data.Unit
+open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_)
+open import Function
+open import Data.Nat hiding (_⊔_) -- using (ℕ; suc; zero)
+open import Relation.Nullary
+open import Data.Empty
+open import Data.Product
+
+open import Gutil 
+open import Putil 
+open import Solvable using (solvable)
+open import  Relation.Binary.PropositionalEquality hiding ( [_] )
+
+open import Data.Fin
+open import Data.Fin.Permutation hiding (_∘ₚ_)
+
+infixr  200 _∘ₚ_
+_∘ₚ_ = Data.Fin.Permutation._∘ₚ_
+
+
+sym2solvable : solvable (Symmetric 2)
+solvable.dervied-length sym2solvable = 1
+solvable.end sym2solvable x d = solved1 x d where
+
+   open import Data.List using ( List ; [] ; _∷_ )
+
+   open Solvable (Symmetric 2)
+   open import FLutil
+   open import Data.List.Fresh hiding ([_])
+   open import Relation.Nary using (⌊_⌋)
+
+   p0id :  FL→perm ((# 0) :: ((# 0) :: f0)) =p= pid
+   p0id = pleq _ _ refl
+
+   open import Data.List.Fresh.Relation.Unary.Any
+   open import FLComm
+
+   stage2FList : CommFListN 2 1 ≡ cons (zero :: zero :: f0) [] (Level.lift tt)
+   stage2FList = refl
+
+   solved1 :  (x : Permutation 2 2) → deriving 1 x → x =p= pid
+   solved1 x dr = CommSolved 2 x ( CommFListN 2 1 ) stage2FList pf solved0 where
+      --    p0id :  FL→perm ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) =p= pid
+      pf : perm→FL x ≡ FL0 → x =p= pid
+      pf eq = ptrans pf1 (ptrans pf0 p0id ) where
+         pf1 : x =p= FL→perm (perm→FL x)
+         pf1 = psym (FL←iso x)
+         pf0 : FL→perm (perm→FL x) =p= FL→perm FL0
+         pf0 = pcong-Fp eq
+      solved0 : Any (perm→FL x ≡_) ( CommFListN 2 1 )
+      solved0 = CommStage→ 2 1 x dr
+
+
--- 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) = {!!}
-
--- a/sym4.agda	Thu Nov 26 08:58:12 2020 +0900
+++ b/sym4.agda	Thu Nov 26 13:13:58 2020 +0900
@@ -24,7 +24,7 @@
 
 sym4solvable : solvable (Symmetric 4)
 solvable.dervied-length sym4solvable = 3
-solvable.end sym4solvable x d = solved1 x {!!} where
+solvable.end sym4solvable x d = solved1 x d where
 
    open import Data.List using ( List ; [] ; _∷_ )
 
@@ -39,79 +39,35 @@
    --  0 ∷ 1 ∷ 2 ∷ 3 ∷ [] ,  1 ∷ 0 ∷ 3 ∷ 2 ∷ [] ,  2 ∷ 3 ∷ 0 ∷ 1 ∷ [] ,  3 ∷ 2 ∷ 1 ∷ 0 ∷ [] ,  
 
 
-   data Klein : (x : Permutation 4 4 ) → Set where
-       kid : Klein pid
-       ka  : Klein (pswap (pswap pid))
-       kb  : Klein (pid {4} ∘ₚ pins (n≤ 3) ∘ₚ pins (n≤ 3 ) )
-       kc  : Klein (pins (n≤ 3)  ∘ₚ  pins (n≤ 2) ∘ₚ pswap (pid {2}))
-
    a0 =  pid {4}
    a1 =  pswap (pswap (pid {0}))
    a2 =  pid {4} ∘ₚ pins (n≤ 3) ∘ₚ pins (n≤ 3 ) 
    a3 =  pins (n≤ 3)  ∘ₚ  pins (n≤ 2) ∘ₚ pswap (pid {2})
 
-   --   1 0  
-   --   2 1 0 
-   --   3 2 1 0
-
-   k1 : { x :  Permutation 4 4 } → Klein x → List ℕ
-   k1 {x} kid = plist x
-   k1 {x} ka = plist x
-   k1 {x} kb = plist x
-   k1 {x} kc = plist x
-
-   k2 = k1 kid ∷ k1 ka ∷ k1 kb ∷ k1 kc ∷ []
    k3 = plist  (a1  ∘ₚ a2 ) ∷ plist (a1 ∘ₚ a3)  ∷ plist (a2 ∘ₚ a1 ) ∷  []
 
    open import FLutil
    open import Data.List.Fresh hiding ([_])
    open import Relation.Nary using (⌊_⌋)
 
-   p0id :  FL→perm ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) =p= pid
+   p0id :  FL→perm ((# 0) :: (# 0) :: ((# 0) :: ((# 0 ) :: f0))) =p= pid
    p0id = pleq _ _ refl
 
-   -- stage 1 (A4)
-   p0 =  (zero :: zero :: zero :: zero :: f0 )
-   p1 =  (zero :: suc zero :: suc zero :: zero :: f0 )
-   p2 =  (zero :: suc (suc zero) :: zero :: zero :: f0 )
-   p3 =  (suc zero :: zero :: suc zero :: zero :: f0 )
-   p4 =  (suc zero :: suc zero :: zero :: zero :: f0 ) 
-   p5 =  (suc zero :: suc (suc zero) :: suc zero :: zero :: f0 )
-   p6 =  (suc (suc zero) :: zero :: zero :: zero :: f0 )
-   p7 =  (suc (suc zero) :: suc zero :: suc zero :: zero :: f0 )
-   p8 =  (suc (suc zero) :: suc (suc zero) :: zero :: zero :: f0 )
-   p9 =  (suc (suc (suc zero)) :: zero :: suc zero :: zero :: f0 )
-   pa =  (suc (suc (suc zero)) :: suc zero :: zero :: zero :: f0 )
-   pb =  (suc (suc (suc zero)) :: suc (suc zero) :: suc zero :: zero :: f0 )
 
-   t0  =  plist (FL→perm p0 ) ∷ plist (FL→perm p1 ) ∷  plist (FL→perm p2 ) ∷ plist (FL→perm p3 ) ∷ plist (FL→perm p4 ) ∷  plist (FL→perm p5 ) ∷ 
-          plist (FL→perm p6 ) ∷ plist (FL→perm p7 ) ∷  plist (FL→perm p8 ) ∷ plist (FL→perm p9 ) ∷ plist (FL→perm pa ) ∷  plist (FL→perm pb ) ∷ []
+   open import Data.List.Fresh.Relation.Unary.Any
+   open import FLComm
 
-   t1  : FList 4 →  FList 4
-   t1  x =  tl2 x x [] where
-       tl3 : (FL 4) → ( z : FList 4) → FList 4 → FList 4
-       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 4) → FList 4 →  FList 4
-       tl2 [] _ x = x
-       tl2 (h ∷# x) z w = tl2 x z (tl3 h z w)
-
-   Flist : FL 4 → FList 4
-   Flist = {!!}
-   
-   stage1  :  FList 4
-   stage1  =  t1 (Flist (fmax ))
-
-   -- stage2 ( Kline )
-   --  k0  p0  zero :: zero :: zero :: zero :: f0 ∷                                   (0 ∷ 1 ∷ 2 ∷ 3 ∷ []) ∷
-   --  k1  p3  suc zero :: zero :: suc zero :: zero :: f0 ∷                           (1 ∷ 0 ∷ 3 ∷ 2 ∷ []) ∷
-   --  k2  p8  suc (suc zero) :: suc (suc zero) :: zero :: zero :: f0 ∷               (2 ∷ 3 ∷ 0 ∷ 1 ∷ []) 
-   --  k3  pb  suc (suc (suc zero)) :: suc (suc zero) :: suc zero :: zero :: f0 ∷     (3 ∷ 2 ∷ 1 ∷ 0 ∷ [])
-
-   tb = plist ( FL→perm p0) ∷ plist ( FL→perm p3) ∷ plist ( FL→perm p8) ∷ plist ( FL→perm pb) ∷ []
-
-   stage2  :   FList 4
-   stage2   =  t1 (t1 (Flist (fmax ))) -- ( p0 ∷# p1 ∷# p2 ∷# p3 ∷# p4 ∷# p5 ∷# p6 ∷# p7 ∷# p8 ∷# p9 ∷# pa ∷# pb ∷# [] ) 
-   
-   solved1 :  (x : Permutation 4 4) →  Commutator (λ x₁ → Commutator (λ x₂ → Lift (Level.suc Level.zero) ⊤) x₁) x → x =p= pid
-   solved1 = {!!}
+   stage3FList : CommFListN 4 3 ≡ cons (zero :: zero :: zero :: zero :: f0) [] (Level.lift tt)
+   stage3FList = refl
+ 
+   solved1 :  (x : Permutation 4 4) → deriving 3 x → x =p= pid 
+   solved1 x dr = CommSolved 4 x ( CommFListN 4 3 ) 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 4 3 )
+      solved2 = CommStage→ 4 3 x dr