# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1607391901 -32400
# Node ID 8c20b6710f1d028aeb4ac49b9fac0ad99a1ccf22
# Parent  adcbf19410fe4082137c9510a6d0dbd1450447ff
anyComm done

diff -r adcbf19410fe -r 8c20b6710f1d FLComm.agda
--- a/FLComm.agda	Tue Dec 08 10:07:50 2020 +0900
+++ b/FLComm.agda	Tue Dec 08 10:45:01 2020 +0900
@@ -141,16 +141,25 @@
   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)
     → 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 | _             = ⊥-elim (¬a (p<anyL1 anyq ¬b)) -- can't happen
-  ... | _            | tri> ¬a ¬b c = ⊥-elim (¬a (p<anyL1 anyp ¬b)) -- 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₁ = insAny (commListQ Q) (anyc01 Q anyq ) where --  p,qi case
-     anyc01 : (Q1 : FList n) → Any (_≡_ q₁ ) Q1 → Any (_≡_ (fpq p₁ q₁)) (commListQ Q1)
-     anyc01 [] any = {!!}
-     anyc01 (cons a Q1 x) anyq = {!!}
-  ... | tri< a ¬b ¬c | tri≈ ¬a₁ b ¬c₁ = {!!}   --- pi,q case
-  ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = {!!} --  previous case
+  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 (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 [] = 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) p₁ q₁ anyp anyq
+     anyc05 (cons a P1 x) = insAny _ (anyc05 P1)
+     anyc04 : (Q1 : FList n) → Any (_≡_ (fpq p₁ q₁)) (commListQ Q1)
+     anyc04 [] = anyc05 P 
+     anyc04 (cons a Q1 x) = insAny _ (anyc04 Q1)
 
 -- {-# TERMINATING #-}
 CommStage→ : (i : ℕ) → (x : Permutation n n ) → deriving i x → Any (perm→FL x ≡_) ( CommFListN i )