--- a/FLComm.agda	Tue Dec 08 09:29:37 2020 +0900
+++ b/FLComm.agda	Tue Dec 08 10:07:50 2020 +0900
@@ -101,12 +101,11 @@
 CommFListN  (suc i) = CommFList (CommFListN i)
 
 -- all comm cobmbination in P and Q
-record AnyComm (p0 q0 : FL n) (P Q : FList n) : Set where
+record AnyComm  (P Q : FList n) : Set where
    field
      commList : FList n
      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
 
 -------------
@@ -115,8 +114,19 @@
 --     :        AnyComm FL0 FL0 P  Q
 --    p0,q       
 
+p<anyL : {p p₁ : FL n} {P : FList n} → {pr : fresh (FL n) ⌊ _f<?_ ⌋ p P } → Any (_≡_ p₁) (cons p P pr) → p f≤ p₁
+p<anyL {p} {p₁} {P} {pr} (here refl) = case1 refl
+p<anyL {p} {p₁} {cons a P x} { Data.Product._,_ (Level.lift p<a) snd} (there any) with p<anyL any
+... | case1 refl = case2 (toWitness p<a)
+... | case2 a<p₁ = case2 (f<-trans (toWitness p<a) a<p₁)
+
+p<anyL1 : {p p₁ : FL n} {P : FList n} → {pr : fresh (FL n) ⌊ _f<?_ ⌋ p P } → Any (_≡_ p₁) (cons p P pr) → ¬ (p ≡ p₁)  → p f< p₁
+p<anyL1 {p} {p₁} {P} {pr} any neq with p<anyL any
+... | case1 eq = ⊥-elim ( neq eq )
+... | case2 x = x
+
 open AnyComm -- q₂
-anyComm : (P Q : FList n) → AnyComm FL0 FL0 P Q
+anyComm : (P Q : FList n) → AnyComm P Q
 anyComm [] [] = record { commList = [] ; commAny = λ _ _ () }
 anyComm [] (cons q Q qr) = record { commList = [] ; commAny = λ _ _ () }
 anyComm (cons p P pr) [] = record { commList = [] ; commAny = λ _ _ _ () }
@@ -129,15 +139,18 @@
   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
+  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 = {!!} --  p,qi case
-  ... | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c = {!!}   --- pi,q case
-  ... | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ = {!!} --  previous 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
 
 -- {-# TERMINATING #-}
 CommStage→ : (i : ℕ) → (x : Permutation n n ) → deriving i x → Any (perm→FL x ≡_) ( CommFListN i )