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

diff -r 1a08ad5d0b4e -r 326221cf402b FLComm.agda
--- a/FLComm.agda	Thu Dec 10 09:53:52 2020 +0900
+++ b/FLComm.agda	Thu Dec 10 12:06:33 2020 +0900
@@ -185,14 +185,16 @@
 
 anyFL01 :  (n : ℕ) → AnyFL (suc n) 
 anyFL01 zero    = record { allFL = (zero :: f0) ∷# [] ; anyP = {!!} } 
-anyFL01 (suc n) = record { allFL = commList  anyFL02 ; anyP =  {!!} } where
+anyFL01 (suc n) = record { allFL = ? commList  (anyFL02 (suc n)) ; anyP =  {!!} } where
      anyFL04 :  (n : ℕ) → AnyFin n
      anyFL04 0 = record { allFin = zero :: f0 ∷# [] ; anyF = {!!} }
      anyFL04 (suc n) = record { allFin = {!!} ; anyF = {!!} }
-     anyFL02 : {!!}
-     anyFL02 = anyComm (allFin (anyFL04 (suc n))) (allFL (anyFL01 n)) (λ p q → FLpos p :: q)
-     anyFL03 : {!!}
-     anyFL03 = commAny anyFL02 
+     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 = {!!}
 
 CommFListN  : ℕ →  FList n
 CommFListN  zero = allFL (anyFL n)