# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1599962082 -32400
# Node ID be888cb9fe1bf226a8a72779860e011d2c559f67
# Parent  c00eac825964dc3f2a666e0e3953fad4e4805caa
...

diff -r c00eac825964 -r be888cb9fe1b FLutil.agda
--- a/FLutil.agda	Sun Sep 13 09:48:33 2020 +0900
+++ b/FLutil.agda	Sun Sep 13 10:54:42 2020 +0900
@@ -146,7 +146,7 @@
 
 open import Data.Product
 open import Relation.Nullary.Decidable hiding (⌊_⌋)
-open import Data.Bool -- hiding (T)
+open import Data.Bool hiding (_<_)
 open import Data.Unit.Base using (⊤ ; tt)
 
 --  fresh a []        = ⊤
@@ -195,3 +195,31 @@
 
 fr6 = FLinsert ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) fr1 
 
+-- open import Data.List.Fresh.Relation.Unary.All
+-- fr7 = append ( ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) ∷# [] ) fr1 ( ({!!} , {!!} ) ∷ [] )
+
+Flist1 :  {n : ℕ } (i : ℕ) → i < suc n → FList {n} → FList {n} → FList {suc n} 
+Flist1 zero i<n [] _ = []
+Flist1 zero i<n (a ∷# x ) z  = FLinsert ( zero :: a ) (Flist1 zero i<n x z )
+Flist1 (suc i) (s≤s i<n) [] z  = Flist1 i (Data.Nat.Properties.<-trans i<n a<sa) z z 
+Flist1 (suc i) i<n (a ∷# x ) z  = FLinsert ((fromℕ< i<n ) :: a ) (Flist1 (suc i) i<n x z )
+
+Flist : {n : ℕ } → FL n → FList {n}
+Flist {zero} f0 = f0 ∷# [] 
+Flist {suc n} (x :: y)  = Flist1 n a<sa (Flist y) (Flist y)   
+
+fr8 : FList {4}
+fr8 = Flist (fmax {4}) 
+
+-- FLinsert membership
+
+module FLMB { n : ℕ } where
+
+  FL-Setoid : Setoid Level.zero Level.zero
+  FL-Setoid  = record { Carrier = FL n ; _≈_ = _≡_ ; isEquivalence = record { sym = sym ; refl = refl ; trans = trans }}
+
+  open import Data.List.Fresh.Membership.Setoid FL-Setoid
+  open import Data.List.Fresh.Relation.Unary.Any 
+
+  FLinsert-mb :  (x : FL n ) → (xs : FList {n})  → x ∈ FLinsert x xs
+  FLinsert-mb x xs = {!!}