# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1607398007 -32400
# Node ID 5a06df3e05d7cc635ceab5a8c7489a09363f0393
# Parent  4cce0c52ec9f5df419abedc3e6c3837027911ac9
allListFL

diff -r 4cce0c52ec9f -r 5a06df3e05d7 FLComm.agda
--- a/FLComm.agda	Tue Dec 08 12:13:56 2020 +0900
+++ b/FLComm.agda	Tue Dec 08 12:26:47 2020 +0900
@@ -60,18 +60,19 @@
 
 open import fin
 open AnyFL
+
+{-# TERMINATING #-}
 anyFL :  AnyFL a<sa
-anyFL  = record { anyList = FLinsert (fromℕ< a<sa :: fmax ) (anyListF {n} a<sa) ; anyP = {!!} }  where
-  anyListFL : (P1 : FL n) → FList (suc n)
-  anyListFL f0 = {!!}
-  anyListFL (zero :: y) = {!!}
-  anyListFL (suc x :: y) = {!!}
-  -- anyListFL (zero :: _)  = anyList anyFL 
-  -- anyListFL (suc p :: P1) =  FLinsert (fromℕ< a<sa  :: (suc p :: P1)) (anyListFL (fin+1 p :: P1))
-  anyListF : {i : ℕ} → (Q1 : i < suc n) → FList (suc n)
-  anyListF (s≤s z≤n) = anyListFL fmax
-  anyListF (s≤s (s≤s i<n)) = FLinsert (fromℕ< {!!} :: fmax) (anyListF ? )
-  
+anyFL  = record { anyList = FLinsert (fromℕ< a<sa :: fmax ) (allListF {n} a<sa) ; anyP = anyFLP }  where
+  allListFL : (P1 : FL n) → FList (suc n)
+  allListFL f0 = []
+  allListFL (zero :: y) = cons (fromℕ< a<sa :: zero :: y) [] {!!}
+  allListFL (suc x :: y) = cons (fromℕ< a<sa :: suc x :: y) (allListFL (fin+1 x :: y)) {!!}
+  allListF : {i : ℕ} → (Q1 : i < suc n) → FList (suc n)
+  allListF (s≤s z≤n) = allListFL fmax
+  allListF (s≤s (s≤s i<n)) = cons (fin+1 (fromℕ< (s≤s i<n)) :: fmax) (allListF  (<-trans (s≤s i<n) a<sa)) {!!}
+  anyFLP :  (x : FL n) → Any (_≡_ (fromℕ< a<sa :: x)) (FLinsert (fromℕ< a<sa :: fmax) (allListF a<sa))
+  anyFLP = {!!}
 
 tl3 : (FL n) → ( z : FList n) → FList n → FList n
 tl3 h [] w = w