# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1607347829 -32400
# Node ID 71e08656273b6441e52d99f09748e8bd816448ce
# Parent  9da456c2bfe393ff4eac5cb37429ac59025c8288
...

diff -r 9da456c2bfe3 -r 71e08656273b FLComm.agda
--- a/FLComm.agda	Mon Dec 07 20:29:13 2020 +0900
+++ b/FLComm.agda	Mon Dec 07 22:30:29 2020 +0900
@@ -101,34 +101,39 @@
 CommFListN  (suc i) = CommFList (CommFListN i)
 
 -- all comm cobmbination in P and Q
-record AnyComm (P Q : FList n) : Set where
+record AnyComm (p0 q0 : FL n) (P Q : FList n) : Set where
    field
      commList : FList n
-     commAny : (p q : FL n) → Any ( p ≡_ ) P →  Any ( q ≡_ ) Q → Any (perm→FL [ FL→perm p , FL→perm q ] ≡_) commList
+     commAny : (p q : FL n)
+         → Any ( p ≡_ ) P →  Any ( q ≡_ ) Q
+         → p0 f≤ p → q0 f≤ q
+         → Any (perm→FL [ FL→perm p , FL→perm q ] ≡_) commList
 
 open AnyComm -- q₂
-anyComm : (P Q : FList n) → AnyComm P Q
+anyComm : (P Q : FList n) → AnyComm FL0 FL0 P Q
 anyComm [] [] = record { commList = [] ; commAny = λ _ _ () }
 anyComm [] (cons q Q qr) = record { commList = [] ; commAny = λ _ _ () }
 anyComm (cons p P pr) [] = record { commList = [] ; commAny = λ _ _ _ () }
 anyComm (cons p P pr) (cons q Q qr) = anyc0n (cons q Q qr) where
-  anyc0n : (Q1 : FList n) → AnyComm (cons p P pr) (cons q Q qr)
+  anyc0n : (Q1 : FList n) → AnyComm {!!} {!!} (cons p P pr) (cons q Q qr)
   anyc0n [] = record { commList = FLinsert (perm→FL [ FL→perm p , FL→perm q ]) (commList (anyComm P (cons q Q qr))) ; commAny = anyc03 } where
     anyc03 :  (p₁ q₁ : FL n) →
         Any ( p₁ ≡_) (cons p P pr) → Any (q₁ ≡_) (cons q Q qr)
+        → {!!} → {!!}
         → Any ((perm→FL [ FL→perm p₁ , FL→perm q₁ ]) ≡_) (FLinsert (perm→FL [ FL→perm p , FL→perm q ]) (commList (anyComm P (cons q Q qr))))
-    anyc03 p₁ q₁ (there anyp) (here x)     = insAny _ (commAny (anyComm P (cons q Q qr)) p₁ q₁ anyp (here x))
-    anyc03 p₁ q₁ (there anyp) (there anyq) = insAny _ (commAny (anyComm P (cons q Q qr)) p₁ q₁ anyp (there anyq))
-    anyc03 p₁ q₁ (here refl)  (there anyq) = insAny _ (commAny (anyComm P (cons q Q qr)) p₁ q₁ (here refl) (there anyq))
-    anyc03 p₁ q₁ (here refl)  (here x) = {!!}
+    anyc03 p₁ q₁ (there anyp) (here x)     _ _ = insAny _ (commAny (anyComm P (cons q Q qr)) p₁ q₁ anyp (here x)  {!!} {!!} )
+    anyc03 p₁ q₁ (there anyp) (there anyq) _ _ = insAny _ (commAny (anyComm P (cons q Q qr)) p₁ q₁ anyp (there anyq) {!!} {!!} )
+    anyc03 p₁ q₁ (here refl)  (there anyq) _ _ = insAny _ (commAny (anyComm P (cons q Q qr)) p₁ q₁ {!!} (there anyq) {!!} {!!} )
+    anyc03 p₁ q₁ (here refl)  (here x) _ _ = {!!}
   anyc0n (cons q₂ Q1 qr₂ ) = record { commList = FLinsert (perm→FL [ FL→perm p , FL→perm q₂ ]) (commList (anyc0n Q1)) 
                                  ; commAny = anyc01 Q1 q₂ qr₂ } where
-    anyc01 :  (Q1 : FList n)  (q₂ : FL n) → (qr₂ : fresh (FL n) ⌊ _f<?_ ⌋ q₂ Q1 ) → (p₁ q₁ : FL n) → Any (p₁ ≡_) (cons p P pr) → Any (q₁ ≡_) (cons q Q qr) →
-      Any (perm→FL [ FL→perm p₁ , FL→perm q₁ ] ≡_) (FLinsert (perm→FL [ FL→perm p , FL→perm q₂ ])  (commList (anyc0n Q1)) ) 
-    anyc01 Q1 q₂ qr₂ p₁ q₁ (here refl) (there anyq)  = insAny _ (commAny (anyc0n Q1)  p₁ q₁ (here refl)  (there anyq))
-    anyc01 Q1 q₂ qr₂ p₁ q₁ (there anyp) (here refl)  = insAny _ (commAny (anyc0n Q1)  p₁ q₁ (there anyp) (here refl))
-    anyc01 Q1 q₂ qr₂ p₁ q₁ (there anyp) (there anyq) = insAny _ (commAny (anyc0n Q1)  p₁ q₁ (there anyp) (there anyq) )
-    anyc01 Q1 q₂ qr₂ p₁ q₁ (here refl) (here refl) with  x∈FLins (perm→FL [ FL→perm p , FL→perm q₂ ])  (commList (anyc0n Q1)) 
+    anyc01 :  (Q1 : FList n)  (q₂ : FL n) → (qr₂ : fresh (FL n) ⌊ _f<?_ ⌋ q₂ Q1 ) → (p₁ q₁ : FL n) → Any (p₁ ≡_) (cons p P pr) → Any (q₁ ≡_) (cons q Q qr)
+      → {!!} → {!!} 
+      → Any (perm→FL [ FL→perm p₁ , FL→perm q₁ ] ≡_) (FLinsert (perm→FL [ FL→perm p , FL→perm q₂ ])  (commList (anyc0n Q1)) ) 
+    anyc01 Q1 q₂ qr₂ p₁ q₁ (here refl) (there anyq)  _ _ = insAny _ (commAny (anyc0n Q1)  p₁ q₁ (here refl)  (there anyq) {!!} {!!} )
+    anyc01 Q1 q₂ qr₂ p₁ q₁ (there anyp) (here refl)  _ _ = insAny _ (commAny (anyc0n Q1)  p₁ q₁ (there anyp) (here refl) {!!} {!!} )
+    anyc01 Q1 q₂ qr₂ p₁ q₁ (there anyp) (there anyq) _ _ = insAny _ (commAny (anyc0n Q1)  p₁ q₁ (there anyp) (there anyq)  {!!} {!!} )
+    anyc01 Q1 q₂ qr₂ p₁ q₁ (here refl) (here refl) _ _ with  x∈FLins (perm→FL [ FL→perm p , FL→perm q₂ ])  (commList (anyc0n Q1)) 
     ... | t = {!!}    -- t : p₁ q₂ → p₁ q₁  
 
 -- {-# TERMINATING #-}