--- a/FLutil.agda	Mon Sep 07 09:39:50 2020 +0900
+++ b/FLutil.agda	Mon Sep 07 20:27:35 2020 +0900
@@ -19,7 +19,6 @@
 
 open import Symmetric
 
-
 open import Relation.Nullary
 open import Data.Empty
 open import  Relation.Binary.Core
@@ -29,26 +28,6 @@
 open import Gutil
 open import Solvable
 
-open import Relation.Nary using (⌊_⌋; fromWitness)
-open import Data.List.Fresh
--- open import Data.List.Fresh.Relation.Unary.All
--- open import Data.List.Fresh.Membership.Setoid
--- open import Data.List.Fresh.Properties
-
-
-FList : {n : ℕ } → Set
-FList {n} = List# (FL n) ⌊ _f<?_ ⌋
-
-fr1 : FList
-fr1 =
-   ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) ∷# 
-   ((# 0) :: ((# 1) :: ((# 0 ) :: f0))) ∷# 
-   ((# 1) :: ((# 0) :: ((# 0 ) :: f0))) ∷# 
-   ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) ∷# 
-   ((# 2) :: ((# 0) :: ((# 0 ) :: f0))) ∷# 
-   ((# 2) :: ((# 1) :: ((# 0 ) :: f0))) ∷# 
-   []
-
 fmax : { n : ℕ } →  FL n
 fmax {zero} = f0
 fmax {suc n} = fromℕ< a<sa :: fmax {n}
@@ -74,10 +53,14 @@
 
 open import logic
 
-FL0< : {n : ℕ } → FL0 {suc n} f≤ fmax
-FL0< {zero} = case1 refl
-FL0< {suc (suc zero)} = case1 (cong (λ k → zero :: k) ? )
-FL0< {suc n} = {!!}
+FL0≤ : {n : ℕ } → FL0 {n} f≤ fmax
+FL0≤ {zero} = case1 refl
+FL0≤ {suc zero} = case1 refl
+FL0≤ {suc n} with <-fcmp zero (fromℕ< {n} a<sa)
+... | tri< a ¬b ¬c = case2 (f<n a)
+... | tri≈ ¬a b ¬c with FL0≤ {n}
+... | case1 x = case1 (subst₂ (λ j k → (zero :: FL0) ≡ (j :: k ) ) b x refl )
+... | case2 x = case2 (subst (λ k →  (zero :: FL0) f< (k :: fmax)) b (f<t x)  )
 
 fsuc : { n : ℕ } → (x : FL n ) → x f< fmax → FL n 
 fsuc {n} (x :: y) (f<n lt) = fromℕ< fsuc1 :: y where
@@ -87,20 +70,23 @@
     fsuc1 =  ≤-trans (s≤s lt) ( s≤s ( toℕ≤pred[n] (fromℕ< a<sa)) )
 fsuc (x :: y) (f<t lt) = x :: fsuc y lt
 
-flist : {n : ℕ } → FList {n}
-flist {zero} = []
-flist {suc n} = flist0 FL0 {!!} where
-   flist0 : (x : FL n) → x f< fmax → FList {suc n}
-   flist0 = {!!}
+open import Data.List
+
+flist1 :  {n : ℕ } (i : ℕ) → i < suc n → List (FL n) → List (FL n) → List (FL (suc n)) 
+flist1 zero i<n [] _ = []
+flist1 zero i<n (a ∷ x ) z  = ( zero :: a ) ∷ flist1 zero i<n x z 
+flist1 (suc i) (s≤s i<n) [] z  = flist1 i (<-trans i<n a<sa) z z 
+flist1 (suc i) i<n (a ∷ x ) z  = ((fromℕ< i<n ) :: a ) ∷ flist1 (suc i) i<n x z 
+
+flist : {n : ℕ } → FL n → List (FL n) 
+flist {zero} f0 = f0 ∷ [] 
+flist {suc n} (x :: y)  = flist1 n a<sa (flist y) (flist y)   
 
 fr22 : fsuc (zero :: zero :: f0) (fmax¬ (λ ())) ≡ (suc zero :: zero :: f0)
 fr22 = refl
 
-fr2 = uncons fr1
+fr4 : List (FL 4)
+fr4 = Data.List.reverse (flist (fmax {4}) )
 
-fr3 : FList
-fr3 =
-   ((# 2) :: ((# 1) :: ((# 0 ) :: f0))) ∷#  []
-
--- fr4 : FList
--- fr4 = append-# ? ? fr2 fr3
+fr5 : List (List ℕ)
+fr5 = map plist (map FL→perm  (Data.List.reverse (flist (fmax {4}) )))