# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1606264910 -32400
# Node ID c8345c4a4c4b6fa064758dfd70776c443c401724
# Parent  cf7622b185a6e0c4c5d38e15f85362f2d5297d0b
...

diff -r cf7622b185a6 -r c8345c4a4c4b FLutil.agda
--- a/FLutil.agda	Wed Nov 25 07:18:05 2020 +0900
+++ b/FLutil.agda	Wed Nov 25 09:41:50 2020 +0900
@@ -247,7 +247,7 @@
 ∀Flist : {n : ℕ } → (x : FL n ) → (L : FList n ) → fresh (FL n) ⌊ _f<?_ ⌋ x L → FList n 
 ∀Flist x L xr with FLcmp x FL0
 ... | tri< a ¬b ¬c = ⊥-elim (¬x<FL0 a)
-... | tri≈ ¬a b ¬c = L
+... | tri≈ ¬a refl ¬c = cons FL0 L xr
 ... | tri> ¬a ¬b c = ∀Flist (fpred x c) (cons x L xr) ( Level.lift (fromWitness (fpred< x c)) , ttf (fpred< x c) L xr) 
 
 fr8 : FList 4
@@ -259,9 +259,26 @@
 open import Data.List.Fresh.Relation.Unary.Any 
 open import Data.List.Fresh.Relation.Unary.All 
 
-AnyFList : (n : ℕ )  → (x : FL n ) →  Any (x ≡_ ) (∀Flist fmax [] (Level.lift tt))
-AnyFList 0 f0 = ?
-AnyFList (suc n) (x :: y) = {!!}
+AnyFList0 : {n : ℕ} (x : FL n ) → (L : FList n ) → (fr : fresh (FL n) ⌊ _f<?_ ⌋ x L ) → Any (x ≡_ ) (∀Flist x L fr)
+AnyFList0 x L fr with FLcmp x FL0
+... | tri< a ¬b ¬c = ⊥-elim (¬x<FL0 a)
+... | tri≈ ¬a refl ¬c = here refl
+AnyFList0 x [] fr | tri> ¬a ¬b c = {!!}
+AnyFList0 x (cons a L ar) fr | tri> ¬a ¬b c = {!!}
+
+{-# TERMINATING #-}
+AnyFList : {n : ℕ }  → (x : FL (suc n) ) →  Any (x ≡_ ) (∀Flist fmax [] (Level.lift tt))
+AnyFList {n} x with FLcmp x fmax
+... | tri> ¬a ¬b c = ⊥-elim (fmax< c)
+... | tri≈ ¬a refl ¬c = AnyFList0 x [] (Level.lift tt)
+... | tri< a ¬b ¬c = AnyFList1 fmax x a [] (Level.lift tt) where
+   AnyFList1 : {n : ℕ} (x y : FL n ) → y f< x  → (L : FList n ) → (fr : fresh (FL n) ⌊ _f<?_ ⌋ x L ) → Any (y ≡_ ) (∀Flist x L fr)
+   AnyFList1 x y y<x L fr with FLcmp x FL0
+   ... | tri< a ¬b ¬c = ⊥-elim (¬x<FL0 a)
+   ... | tri≈ ¬a refl ¬c = ⊥-elim (¬x<FL0 y<x)
+   ... | tri> ¬a ¬b c = af1 where
+        af1 : Any (_≡_ y) (∀Flist (fpred x c)  (cons x L fr)  ( Level.lift (fromWitness (fpred< x c)) , ttf (fpred< x c) L fr) ) 
+        af1 = {!!}
 
 x∈FLins : {n : ℕ} → (x : FL n ) → (xs : FList n)  → Any (x ≡_ ) (FLinsert x xs)
 x∈FLins {zero} f0 [] = here refl