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

diff -r 3c3619b196dc -r d204b7f9b89a FLComm.agda
--- a/FLComm.agda	Wed Dec 09 07:12:01 2020 +0900
+++ b/FLComm.agda	Wed Dec 09 10:45:41 2020 +0900
@@ -58,26 +58,33 @@
 -- all FL
 record AnyFL (n : ℕ) {i : ℕ} (i<n : i < suc n) (y : FL n) : Set where
    field
-     anyList : FList (suc n)
-     anyP : (x : FL (suc n)) → Any (x ≡_ ) anyList 
+     allFL : FList (suc n)
+     anyP : (x : FL (suc n)) → Any (x ≡_ ) allFL 
 
 open import fin
 open AnyFL
 
 -- {-# TERMINATING #-}
 anyFL :  (n : ℕ) → AnyFL n a<sa fmax
-anyFL zero = record { anyList = (zero :: f0) ∷# [] ; anyP = anyFL0 } where 
+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 { anyList = allListF a<sa []; anyP = {!!} } where 
+anyFL (suc n)  = record { allFL = allListF a<sa []; anyP = λ x → anyFL0 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 = z
-    allListF (s≤s (s≤s i<n)) z = allListFL (fin+1 (fromℕ< (s≤s i<n ))) (anyList (anyFL n)) (allListF (<-trans (s≤s i<n) a<sa) z)
-    anyFL0 :  (x : FL (suc (suc n))) → Any (_≡_ x) (allListF a<sa [])
-    anyFL0 = ?
+    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 = {!!}
+    ... | tri≈ ¬a b ¬c = {!!}
+    ... | tri> ¬a ¬b c = ⊥-elim (nat-≤> x<i c)
+
+at1 = allFL (anyFL 1)
+at2 = allFL (anyFL 2)
+at3 = allFL (anyFL 3)
 
 tl3 : (FL n) → ( z : FList n) → FList n → FList n
 tl3 h [] w = w
diff -r 3c3619b196dc -r d204b7f9b89a FLutil.agda
--- a/FLutil.agda	Wed Dec 09 07:12:01 2020 +0900
+++ b/FLutil.agda	Wed Dec 09 10:45:41 2020 +0900
@@ -93,14 +93,11 @@
 ... | tri≈ ¬a b ¬c = ⊥-elim ( ne b)
 ... | tri> ¬a ¬b c = ⊥-elim (fmax< c)
 
-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)  )
+x≤fmax : {n : ℕ } → {x : FL n} → x f≤ fmax
+x≤fmax {n} {x} with FLcmp x fmax
+... | tri< a ¬b ¬c = case2 a
+... | tri≈ ¬a b ¬c = case1 b
+... | tri> ¬a ¬b c = ⊥-elim ( fmax< c )
 
 open import Data.Nat.Properties using ( ≤-trans ; <-trans )
 fsuc : { n : ℕ } → (x : FL n ) → x f< fmax → FL n