# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1607588154 -32400
# Node ID f1f76eed9335b4b6cf03f3a59f8966450e23d65b
# Parent  326221cf402beb6612775ecab0e505ae851daae3
...

diff -r 326221cf402b -r f1f76eed9335 FLComm.agda
--- a/FLComm.agda	Thu Dec 10 12:06:33 2020 +0900
+++ b/FLComm.agda	Thu Dec 10 17:15:54 2020 +0900
@@ -55,10 +55,11 @@
 open import fin
 open AnyFL
 
+anyFL2 : (x : FL 1) → (y : FList 1) → y ≡ ((zero :: f0) ∷# []) → Any (_≡_ x) y
+anyFL2 (zero :: f0) .(cons (zero :: f0) [] (Level.lift tt)) refl = here refl
+
 anyFL0 :  (n : ℕ) → AnyFL (suc n) 
-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 zero = record { allFL = (zero :: f0) ∷# [] ; anyP = λ x → anyFL2 x ((zero :: f0) ∷# []) 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
@@ -184,17 +185,22 @@
 open AnyFin
 
 anyFL01 :  (n : ℕ) → AnyFL (suc n) 
-anyFL01 zero    = record { allFL = (zero :: f0) ∷# [] ; anyP = {!!} } 
-anyFL01 (suc n) = record { allFL = ? commList  (anyFL02 (suc n)) ; anyP =  {!!} } where
+anyFL01 zero    = record { allFL = (zero :: f0) ∷# [] ; anyP = λ x → anyFL2 x ((zero :: f0) ∷# []) refl } 
+anyFL01 (suc n) = record { allFL = commList anyC ;  anyP =  anyFL02 } where
      anyFL04 :  (n : ℕ) → AnyFin n
-     anyFL04 0 = record { allFin = zero :: f0 ∷# [] ; anyF = {!!} }
-     anyFL04 (suc n) = record { allFin = {!!} ; anyF = {!!} }
-     anyFL02 : (n : ℕ ) → AnyComm (allFin (anyFL04 (suc n))) (allFL (anyFL01 n)) (λ p q → FLpos p :: q )
-     anyFL02 n = anyComm (allFin (anyFL04 (suc n))) (allFL (anyFL01 n)) (λ p q → FLpos p :: q) 
-     anyFL03 : (n : ℕ ) → (x : FL (suc (suc n))) → Any (_≡_  x) (commList (anyFL02 n))
-     anyFL03 zero x = {!!}
-     anyFL03 n (x :: y) with commAny (anyFL02 (suc n)) ({!!} :: FL0) {!!} {!!} --(anyFL03 {!!})
-     ... | t = {!!}
+     anyFL04 n = record { allFin = anyFL05 a<sa ; anyF = anyFL06 a<sa} where
+         anyFL05 : {i : ℕ} → (i < suc n) → FList (suc n)
+         anyFL05 {0} (s≤s z≤n) = zero :: FL0 ∷# []
+         anyFL05 {suc i} (s≤s i<n) = FLinsert (fromℕ< (s≤s i<n) :: FL0) (anyFL05 {i} (<-trans i<n a<sa))
+         anyFL06 : {i j : ℕ} (i<n : i < suc n) → (j<n : j < suc n) → Any (_≡_ (fromℕ< j<n :: FL0)) (anyFL05 i<n)
+         anyFL06 {0} (s≤s z≤n) = here refl
+         anyFL06 {i} i<n = {!!}
+     anyC = anyComm (allFin (anyFL04 (suc n))) (allFL (anyFL01 n)) (λ p q → FLpos p :: q )
+     anyFL02 : (x : FL (suc (suc n))) → Any (_≡_ x) (commList anyC)
+     anyFL02 (x :: y) = commAny anyC (x :: FL0) y
+                       (subst (λ k → Any (_≡_ (k :: FL0) ) _) (fromℕ<-toℕ _ _) (anyF (anyFL04 (suc n)) x≤n )) (anyP (anyFL01 n) y) where
+         x≤n : suc (toℕ x)  ≤ suc (suc n)
+         x≤n = toℕ<n x
 
 CommFListN  : ℕ →  FList n
 CommFListN  zero = allFL (anyFL n)