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

diff -r 3aafd76f21c1 -r c3a67bb7cbc0 FLComm.agda
--- a/FLComm.agda	Wed Dec 09 14:40:31 2020 +0900
+++ b/FLComm.agda	Wed Dec 09 17:18:05 2020 +0900
@@ -87,16 +87,29 @@
         anyFL6 (cons _ xs  _) (there any) refl = insAny _ (anyFL6 xs any refl )
     anyFL3 {suc i} (s≤s (s≤s i<n)) (x :: y) x<i z with <-cmp (toℕ x) (suc i)
     ... | tri< a ¬b ¬c = anyFL1 (s≤s i<n) where
-        anyFL1 : {i : ℕ } → (i<n : i < suc n) →  Any (_≡_ (x :: y)) (allListF (s≤s i<n) z)
-        anyFL1 i<n = {!!}
+        anyFL1  : {i : ℕ} → (i<n : i < suc n) →  Any (_≡_ (x :: y)) (allListF (s≤s i<n) z)
+        anyFL10 : {j : ℕ} → (i<n : j < suc n ) → (x<i : toℕ x ≤ suc i) → (L : FList (suc n))  
+            → Any (_≡_ (x :: y))  (allListFL (suc (fromℕ< i<n)) L (allListF (<-trans i<n a<sa) z) )
+        anyFL10 {j} (s≤s j<n) x<i [] = anyFL3 (<-trans (s≤s j<n) a<sa) (x :: y) (anyFL11 x<i)  z   where
+             anyFL11 : toℕ x ≤ suc i → toℕ x ≤ j 
+             anyFL11 = {!!}
+        anyFL10 {i} i<n x<i (cons _ xs _)  = insAny _ (anyFL10 {i} i<n x<i xs )
+        anyFL1 (s≤s i<n) = anyFL10 (s≤s i<n ) x<i (allFL (anyFL0 n)) 
     ... | tri≈ ¬a b ¬c = anyFL7 (allFL (anyFL0 n)) (anyP (anyFL0 n) y) where
-        anyFL8 : (L : FList (suc n)) → Any (_≡_ y) L →  Any (_≡_ (x :: y)) (allListFL x L
-                (allListF {!!} z)) -- b : toℕ x ≡ suc i
-        anyFL8 (cons _ xs _) (here refl) = x∈FLins (x :: y)  (allListFL x xs (allListF {!!} z))
+        anyFL9 : toℕ x ≡ suc i → x ≡ suc (fromℕ< (s≤s i<n))
+        anyFL9 x=si = toℕ-injective ( begin
+             toℕ x ≡⟨ x=si ⟩
+             suc i  ≡⟨ cong suc (≡-sym (toℕ-fromℕ< _) ) ⟩
+             suc (toℕ (fromℕ< (s≤s i<n)))  ≡⟨⟩
+             toℕ (suc (fromℕ< (s≤s i<n)))
+          ∎ ) where open ≡-Reasoning
+        anyFL8 : (L : FList (suc n)) → Any (_≡_ y) L → Any (_≡_ (x :: y)) (allListFL x L (allListF (<-trans (s≤s i<n) a<sa) z))
+        anyFL8 (cons _ xs _) (here refl) = x∈FLins (x :: y) (allListFL x xs (allListF (<-trans (s≤s i<n) a<sa) z))
         anyFL8 (cons _ xs _) (there any) = insAny _ (anyFL8 xs any)
         anyFL7 : (L : FList (suc n)) → Any (_≡_ y) L → Any (_≡_ (x :: y)) (allListF (s≤s (s≤s i<n)) z)
         anyFL7 (cons _ xs _) (there any) = anyFL7 xs any
-        anyFL7 (cons _ xs _) (here refl) = subst (λ k →  Any (_≡_ (x :: y)) k) {!!} ( anyFL8 (allFL (anyFL0 n)) (anyP (anyFL0 n) y) )
+        anyFL7 (cons _ xs _) (here refl) = subst (λ k →  Any (_≡_ (x :: y))
+            (allListFL k (allFL (anyFL0 n)) (allListF (<-trans (s≤s i<n) a<sa) z)) ) (anyFL9 b) (anyFL8 (allFL (anyFL0 n)) (anyP (anyFL0 n) y) )
     ... | tri> ¬a ¬b c = ⊥-elim (nat-≤> x<i c)
 
 anyFL :  (n : ℕ) → AnyFL n fmax