# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1607481223 -32400
# Node ID f8bfda8d06690e5c2fbbee25e78bb06927a7dcc1
# Parent  d204b7f9b89aaef484d039f1c389dea274dd3173
...

diff -r d204b7f9b89a -r f8bfda8d0669 FLComm.agda
--- a/FLComm.agda	Wed Dec 09 10:45:41 2020 +0900
+++ b/FLComm.agda	Wed Dec 09 11:33:43 2020 +0900
@@ -56,32 +56,45 @@
 --  
 
 -- all FL
-record AnyFL (n : ℕ) {i : ℕ} (i<n : i < suc n) (y : FL n) : Set where
+record AnyFL (n : ℕ) (y : FL n) : Set where
    field
-     allFL : FList (suc n)
-     anyP : (x : FL (suc n)) → Any (x ≡_ ) allFL 
+     allFL : FList n
+     anyP : (x : FL n) → Any (x ≡_ ) allFL 
 
 open import fin
 open AnyFL
 
 -- {-# TERMINATING #-}
-anyFL :  (n : ℕ) → AnyFL n a<sa fmax
-anyFL zero = record { allFL = (zero :: f0) ∷# [] ; anyP = anyFL0 } where 
-    anyFL0 : (x : FL 1) → Any (_≡_ x) (cons (zero :: f0) [] (Level.lift tt))
-    anyFL0 (zero :: f0) = here refl
-anyFL (suc n)  = record { allFL = allListF a<sa []; anyP = λ x → anyFL0 a<sa x (fin≤n (FLpos x)) [] } where 
+anyFL0 :  (n : ℕ) → AnyFL (suc n) fmax
+anyFL0 zero = record { allFL = (zero :: f0) ∷# [] ; anyP = anyFL2 } where 
+    anyFL2 : (x : FL 1) → Any (_≡_ x) (cons (zero :: f0) [] (Level.lift tt))
+    anyFL2 (zero :: f0) = here refl
+anyFL0 (suc n)  = record { allFL = allListF a<sa []; anyP = λ x → anyFL3 a<sa x (fin≤n (FLpos x)) [] } where 
     allListFL : (x : Fin (suc (suc n))) → FList (suc n) → FList (suc (suc n)) → FList (suc (suc n))
     allListFL _ [] y = y
     allListFL x (cons y L yr) z = FLinsert (x :: y) (allListFL x L z) 
     allListF : {i : ℕ} → (i<n : i < suc (suc n)) → FList (suc (suc n)) → FList (suc (suc n))
-    allListF (s≤s z≤n) z = allListFL (fromℕ< a<sa) (allFL (anyFL n)) z
-    allListF (s≤s (s≤s i<n)) z = allListFL (fin+1 (fromℕ< (s≤s i<n ))) (allFL (anyFL n)) (allListF (<-trans (s≤s i<n) a<sa) z)
-    anyFL0 :  {i : ℕ} → (i<n : i < suc (suc n)) (x : FL (suc (suc n))) → (toℕ (FLpos x ) ≤ i) → (z : FList (suc (suc n))) → Any (_≡_ x) (allListF i<n z)
-    anyFL0 {i} (s≤s i<n) (x :: y) x<i z with <-cmp (toℕ x) i
-    ... | tri< a ¬b ¬c = {!!}
+    allListF (s≤s z≤n) z = allListFL zero (allFL (anyFL0 n)) z
+    allListF (s≤s (s≤s i<n)) z = allListFL (suc (fromℕ< (s≤s i<n ))) (allFL (anyFL0 n)) (allListF (<-trans (s≤s i<n) a<sa) z)
+    anyFL3 :  {i : ℕ} → (i<n : i < suc (suc n)) (x : FL (suc (suc n))) → (toℕ (FLpos x ) ≤ i) → (z : FList (suc (suc n))) → Any (_≡_ x) (allListF i<n z)
+    anyFL3 {zero} (s≤s z≤n) (x :: y) x<i z = {!!} where
+        anyFL5 : toℕ x ≤ zero → x ≡ zero
+        anyFL5 lt with <-fcmp x zero
+        ... | tri≈ ¬a b ¬c = b
+        ... | tri> ¬a ¬b c = ⊥-elim (nat-≤> x<i c)
+    anyFL3 {suc i} (s≤s i<n) (x :: y) x<i z with <-cmp (toℕ x) (suc i)
+    ... | tri< a ¬b ¬c = anyFL1 i<n where
+        anyFL1 : {i : ℕ } → (i<n : i < suc n) →  Any (_≡_ (x :: y)) (allListF (s≤s i<n) z)
+        anyFL1 L = {!!}
     ... | tri≈ ¬a b ¬c = {!!}
     ... | tri> ¬a ¬b c = ⊥-elim (nat-≤> x<i c)
 
+anyFL :  (n : ℕ) → AnyFL n fmax
+anyFL zero = record { allFL = f0 ∷# [] ; anyP = anyFL4 } where
+    anyFL4 : (x : FL zero) → Any (_≡_ x) ( f0 ∷# [] )
+    anyFL4 f0 = here refl
+anyFL (suc n) = anyFL0 n
+
 at1 = allFL (anyFL 1)
 at2 = allFL (anyFL 2)
 at3 = allFL (anyFL 3)