# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1607430068 -32400
# Node ID 8f7c09ff96bd62fc304191dbb9e121806468b1a7
# Parent  5a06df3e05d7cc635ceab5a8c7489a09363f0393
...

diff -r 5a06df3e05d7 -r 8f7c09ff96bd FLComm.agda
--- a/FLComm.agda	Tue Dec 08 12:26:47 2020 +0900
+++ b/FLComm.agda	Tue Dec 08 21:21:08 2020 +0900
@@ -11,7 +11,7 @@
 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.Unit hiding (_≤_)
 open import Data.Empty
 open import  Relation.Binary.Core 
 open import  Relation.Binary.Definitions hiding (Symmetric )
@@ -53,26 +53,33 @@
 --    (suc n :: (zero :: p)
 
 -- all FL
-record AnyFL {i : ℕ} (i<n : i < suc n) : Set where
+record AnyFL {i : ℕ} (i<n : i < suc n) (y : FL n) : Set where
    field
-     anyList : FList (suc n)
-     anyP : (x : FL n) → Any (fromℕ< i<n  :: x ≡_ ) anyList 
+     anyList : FList (suc (suc n))
+     anyP : {x : FL (suc n)} → {j : ℕ}  → x f≤ (fromℕ< a<sa :: y) → (j≤i : j ≤ i)  → Any (fromℕ< (<-trans (s≤s j≤i) (s≤s i<n)) :: x ≡_ ) anyList 
 
 open import fin
 open AnyFL
 
 {-# TERMINATING #-}
-anyFL :  AnyFL a<sa
-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 = {!!}
+anyFL :  AnyFL a<sa fmax
+anyFL  = record { anyList = allListF a<sa ; anyP = {!!} } where 
+    allListFL : (x : FL (suc n)) → FList (suc (suc n))
+    allListFL (zero :: y) = {!!}
+    allListFL (suc x :: y) = FLinsert {!!} (allListFL (fin+1 x :: y))
+    allListF : {i : ℕ} → (i<n : i < suc n) → FList (suc (suc n))
+    allListF (s≤s z≤n) = allListFL fmax
+    allListF (s≤s (s≤s i<n)) = FLinsert {!!} (allListF  (<-trans (s≤s i<n) a<sa)) 
+--  allListFL : (P1 : FL n) → FList (suc n)
+--  allListFL f0 = []
+--  allListFL (zero :: y) = cons (fromℕ< a<sa :: zero :: y) [] (Level.lift tt)
+--  allListFL (suc x :: y) = FLinsert (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)) = FLinsert (fin+1 (fromℕ< (s≤s i<n)) :: fmax) (allListF  (<-trans (s≤s i<n) a<sa)) 
+--  anyFLP :  {i : ℕ } → (i<n : i < suc n) → (x : FL n) → Any (_≡_ (fromℕ< a<sa :: x)) (FLinsert (fromℕ< i<n :: fmax) (allListF i<n))
+--  anyFLP (s≤s z≤n) x = {!!}
+--  anyFLP (s≤s (s≤s i<n)) x = {!!}
 
 tl3 : (FL n) → ( z : FList n) → FList n → FList n
 tl3 h [] w = w