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

diff -r 2a7d092e1240 -r 1a08ad5d0b4e FLComm.agda
--- a/FLComm.agda	Wed Dec 09 18:59:20 2020 +0900
+++ b/FLComm.agda	Thu Dec 10 09:53:52 2020 +0900
@@ -43,9 +43,11 @@
 --    # 0 :: # 1 :: # 1 : # 0 :: f0
 --    # 0 :: # 2 :: # 0 : # 0 :: f0
 --       ...
+--    # 3 :: # 2 :: # 0 : # 0 :: f0
+--    # 3 :: # 2 :: # 1 : # 0 :: f0
 
 -- all FL
-record AnyFL (n : ℕ) (y : FL n) : Set where
+record AnyFL (n : ℕ) : Set where
    field
      allFL : FList n
      anyP : (x : FL n) → Any (x ≡_ ) allFL 
@@ -53,7 +55,7 @@
 open import fin
 open AnyFL
 
-anyFL0 :  (n : ℕ) → AnyFL (suc n) fmax
+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
@@ -98,22 +100,27 @@
             (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
+anyFL :  (n : ℕ) → AnyFL n 
 anyFL zero = record { allFL = f0 ∷# [] ; anyP = anyFL4 } where
     anyFL4 : (x : FL zero) → Any (_≡_ x) ( f0 ∷# [] )
     anyFL4 f0 = here refl
 anyFL (suc n) = anyFL0 n
 
-at1 = toList (allFL (anyFL 1))
-at2 = toList (allFL (anyFL 2))
-at3 = toList (allFL (anyFL 3))
-at4 = toList (allFL (anyFL 4))
+at1 = proj₁ (toList (allFL (anyFL 1)))
+at2 = proj₁ (toList (allFL (anyFL 2)))
+at3 = proj₁ (toList (allFL (anyFL 3)))
+at4 = proj₁ (toList (allFL (anyFL 4)))
+
+-- open import Data.List.Fresh.Relation.Unary.All
+-- at6 : All (_# allFL (anyFL 2)) (allFL (anyFL 2))
+-- at6 = {!!}
+-- at5 = append (allFL (anyFL 2)) (allFL (anyFL 2)) at6
 
 -- all cobmbination in P and Q
-record AnyComm {n : ℕ}  (P Q : FList n) (fpq : (p q : FL n) → FL n) : Set where
+record AnyComm {n m l : ℕ}  (P : FList n) (Q : FList m) (fpq : (p : FL n) (q : FL m) → FL l) : Set where
    field
-     commList : FList n
-     commAny : (p q : FL n)
+     commList : FList l
+     commAny : (p : FL n) (q : FL m)
          → Any ( p ≡_ ) P →  Any ( q ≡_ ) Q
          → Any (fpq p q ≡_) commList
 
@@ -135,39 +142,58 @@
 ... | case2 x = x
 
 open AnyComm 
-anyComm : {n : ℕ } → (P Q : FList n) → (fpq : (p q : FL n) → FL n)  → AnyComm P Q fpq
+anyComm : {n m l : ℕ } → (P : FList n) (Q : FList m) → (fpq : (p : FL n) (q : FL m) → FL l)  → AnyComm P Q fpq
 anyComm [] [] _ = record { commList = [] ; commAny = λ _ _ () }
 anyComm [] (cons q Q qr) _ = record { commList = [] ; commAny = λ _ _ () }
 anyComm (cons p P pr) [] _ = record { commList = [] ; commAny = λ _ _ _ () }
-anyComm {n} (cons p P pr) (cons q Q qr) fpq = record { commList = FLinsert (fpq p q) (commListQ Q)  ; commAny = anyc0n } where 
-  commListP : (P1 : FList n) → FList n
-  commListP [] = commList (anyComm {n} P Q fpq)
+anyComm {n} {m} {l} (cons p P pr) (cons q Q qr) fpq = record { commList = FLinsert (fpq p q) (commListQ Q)  ; commAny = anyc0n } where 
+  commListP : (P1 : FList n) → FList l
+  commListP [] = commList (anyComm P Q fpq)
   commListP (cons p₁ P1 x) =  FLinsert (fpq p₁ q) (commListP P1)
-  commListQ : (Q1 : FList n) → FList n
+  commListQ : (Q1 : FList m) → FList l
   commListQ [] = commListP P
   commListQ (cons q₁ Q1 qr₁) = FLinsert (fpq p q₁) (commListQ Q1)
-  anyc0n : (p₁ q₁ : FL n) → Any (_≡_ p₁) (cons p P pr) → Any (_≡_ q₁) (cons q Q qr)
+  anyc0n : (p₁ : FL n) (q₁ : FL m) → Any (_≡_ p₁) (cons p P pr) → Any (_≡_ q₁) (cons q Q qr)
     → Any (_≡_ (fpq p₁ q₁)) (FLinsert (fpq p q) (commListQ Q))
   anyc0n p₁ q₁ (here refl) (here refl) = x∈FLins _ (commListQ Q )
   anyc0n p₁ q₁ (here refl) (there anyq) = insAny (commListQ Q) (anyc01 Q anyq) where 
-     anyc01 : (Q1 : FList n) → Any (_≡_ q₁) Q1 → Any (_≡_ (fpq p₁ q₁)) (commListQ Q1)
+     anyc01 : (Q1 : FList m) → Any (_≡_ q₁) Q1 → Any (_≡_ (fpq p₁ q₁)) (commListQ Q1)
      anyc01 (cons q Q1 qr₂) (here refl) = x∈FLins _ _
      anyc01 (cons q₂ Q1 qr₂) (there any) = insAny _ (anyc01 Q1 any)
   anyc0n p₁ q₁ (there anyp) (here refl) = insAny _ (anyc02 Q) where
      anyc03 : (P1 : FList n) → Any (_≡_ p₁) P1  → Any (_≡_ (fpq p₁ q₁)) (commListP P1)
      anyc03 (cons a P1 x) (here refl) = x∈FLins _ _ 
      anyc03 (cons a P1 x) (there any) = insAny _ ( anyc03 P1 any) 
-     anyc02 : (Q1 : FList n) → Any (_≡_ (fpq p₁ q₁)) (commListQ Q1)
+     anyc02 : (Q1 : FList m) → Any (_≡_ (fpq p₁ q₁)) (commListQ Q1)
      anyc02 [] = anyc03 P anyp
      anyc02 (cons a Q1 x) = insAny _ (anyc02 Q1)
   anyc0n p₁ q₁ (there anyp) (there anyq) = insAny (commListQ Q) (anyc04 Q) where
      anyc05 : (P1 : FList n) → Any (_≡_ (fpq p₁ q₁)) (commListP P1)
      anyc05 [] = commAny (anyComm P Q fpq) p₁ q₁ anyp anyq
      anyc05 (cons a P1 x) = insAny _ (anyc05 P1)
-     anyc04 : (Q1 : FList n) → Any (_≡_ (fpq p₁ q₁)) (commListQ Q1)
+     anyc04 : (Q1 : FList m) → Any (_≡_ (fpq p₁ q₁)) (commListQ Q1)
      anyc04 [] = anyc05 P 
      anyc04 (cons a Q1 x) = insAny _ (anyc04 Q1)
 
+--   anyComm ( #0 :: FL0 ... # n : FL0 ) (all n) (λ p q → FLpos p :: q ) = all (suc n)
+record AnyFin (n : ℕ)  : Set where
+   field
+     allFin : FList (suc n)
+     anyF : {i : ℕ} → (i<n : i < suc n) → Any (fromℕ< i<n :: FL0 ≡_ ) allFin 
+
+open AnyFin
+
+anyFL01 :  (n : ℕ) → AnyFL (suc n) 
+anyFL01 zero    = record { allFL = (zero :: f0) ∷# [] ; anyP = {!!} } 
+anyFL01 (suc n) = record { allFL = commList  anyFL02 ; 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 
+
 CommFListN  : ℕ →  FList n
 CommFListN  zero = allFL (anyFL n)
 CommFListN (suc i ) = commList (anyComm ( CommFListN i ) ( CommFListN i ) (λ p q →  perm→FL [ FL→perm p , FL→perm q ] ))