open import Level hiding ( suc ; zero )
open import Algebra
module sym5n 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._∘ₚ_

-- open import IO
open import Data.String hiding (toList)
open import Data.Unit
open import Agda.Builtin.String 

sym5solvable : (n : ℕ) → String -- ¬ solvable (Symmetric 5)
sym5solvable n = FListtoStr (CommFListN 5 n) where

   open import Data.List using ( List ; [] ; _∷_ )
   open Solvable (Symmetric 5)

   open import FLutil
   open import Data.List.Fresh hiding ([_])
   open import Relation.Nary using (⌊_⌋)

   p0id :  FL→perm (zero :: zero :: zero :: (zero :: (zero :: f0))) =p= pid
   p0id = pleq _ _ refl

   open import Data.List.Fresh.Relation.Unary.Any
   open import FLComm


   stage4FList = CommFListN 5 0 
   stage6FList = CommFListN 5 3 

   -- stage5FList = {!!}
   -- s2=s3 :  CommFListN 5 2 ≡ CommFListN 5 3 
   -- s2=s3 = refl

   FLtoStr : {n : ℕ} → (x : FL n) → String
   FLtoStr f0 = "f0"
   FLtoStr (x :: y) = primStringAppend ( primStringAppend (primShowNat (toℕ x)) " :: " ) (FLtoStr y)

   FListtoStr : {n : ℕ} → (x : FList n) → String
   FListtoStr [] = ""
   FListtoStr (cons a x x₁) = primStringAppend (FLtoStr a) (primStringAppend "\n" (FListtoStr x))

open import IO -- using (IO)

main = run ( putStrLn $ sym5solvable 4)