# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1607387377 -32400
# Node ID 08a99237e56ee80329a56995dec81b8892cf6b03
# Parent  71e08656273b6441e52d99f09748e8bd816448ce
restart anyComm

diff -r 71e08656273b -r 08a99237e56e FLComm.agda
--- a/FLComm.agda	Mon Dec 07 22:30:29 2020 +0900
+++ b/FLComm.agda	Tue Dec 08 09:29:37 2020 +0900
@@ -109,32 +109,35 @@
          → p0 f≤ p → q0 f≤ q
          → Any (perm→FL [ FL→perm p , FL→perm q ] ≡_) commList
 
+-------------
+--    (p,q)   (p,qn) ....           (p,q0)
+--    pn,q       
+--     :        AnyComm FL0 FL0 P  Q
+--    p0,q       
+
 open AnyComm -- 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 [] = 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₁ {!!} (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)) 
-    ... | t = {!!}    -- t : p₁ q₂ → p₁ q₁  
+anyComm (cons p P pr) (cons q Q qr) = record { commList = FLinsert (fpq p q) (commListQ Q)  ; commAny = anyc0n } where 
+  fpq : (p q : FL n) → FL n
+  fpq p q = perm→FL [ FL→perm p , FL→perm q ]
+  commListP : (P1 : FList n) → FList n
+  commListP [] = commList (anyComm P Q)
+  commListP (cons p₁ P1 x) =  FLinsert (fpq p₁ q) (commListP P1)
+  commListQ : (Q1 : FList n) → FList n
+  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) →
+    FL0 f≤ p₁ → FL0 f≤ q₁ → Any (_≡_ (perm→FL [ FL→perm p₁ , FL→perm q₁ ])) (FLinsert (fpq p q) (commListQ Q))
+  anyc0n p₁ q₁ anyp anyq _ _ with FLcmp q q₁ | FLcmp p p₁
+  ... | tri< a ¬b ¬c | _             = {!!} -- can't happen
+  ... | _            | tri< a ¬b ¬c₁ = {!!}  -- can't happen
+  ... | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = x∈FLins (fpq p q)  (commListQ Q) -- p,q case
+  ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c = {!!} --  p,qi case
+  ... | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c = {!!}   --- pi,q case
+  ... | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ = {!!} --  previous case
 
 -- {-# TERMINATING #-}
 CommStage→ : (i : ℕ) → (x : Permutation n n ) → deriving i x → Any (perm→FL x ≡_) ( CommFListN i )