# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1607227885 -32400
# Node ID 14b518eecf82e6330470cf6993f785e5db13e76c
# Parent  3e9222eae43cfa1648add1cde743bec05fd04ff7
P Q

diff -r 3e9222eae43c -r 14b518eecf82 FLComm.agda
--- a/FLComm.agda	Sun Dec 06 12:34:24 2020 +0900
+++ b/FLComm.agda	Sun Dec 06 13:11:25 2020 +0900
@@ -115,23 +115,24 @@
   insAnyComm : {p₁ q₁ h : FL n } → (xs : FList n)  → Any ( perm→FL [ FL→perm p₁ , FL→perm q₁ ] ≡_ ) xs
         → Any (perm→FL [ FL→perm p₁ , FL→perm q₁ ] ≡_ ) (FLinsert h xs)
   insAnyComm xs any = insAny _ any
+  anyc04 : (x b : FL n) → (L : FList n) → Any (x ≡_ )  L → Any (x ≡_ )  (FLinsert b L)
+  anyc04 a b L any = insAny L any
+
   anyc0n : (Q1 : FList n) → AnyComm (cons p P pr) (cons q Q qr)
   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)) ) 
-  anyc04 : (x b : FL n) → (L : FList n) → Any (x ≡_ )  L → Any (x ≡_ )  (FLinsert b L)
-  anyc04 a b L any = insAny L any
   anyc01 [] q₁ qr₁ p₁ q₂ (here refl) (here refl) = {!!}
   anyc01 [] q₁ qr₁ p₁ q₂ (here refl) (there anyq) with anyc04 (perm→FL [ FL→perm p , FL→perm q₁ ]) (perm→FL [ FL→perm p , FL→perm q₁ ]) (commList (anyc0n [])) {!!}
   ... | t = {!!}
   anyc01 [] q₁ qr₁ p₁ q₂ (there anyp) (here refl) =  {!!} 
   anyc01 [] q₁ qr₁ p₁ q₂ (there anyp) (there anyq) = {!!} --  insAny (commList (anyc0n [])) {!!}  -- (commAny (anyc0n [])  p₁  q₂ (here refl) (there anyq) )
   anyc01 (cons q₃ Q1 qr₃) q₁ qr₁ p₁ q₂ anyp anyq = {!!}
-  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₁ (here refl) (here refl) = {!!}
-    anyc03 p₁ q₁ (here refl) (there anyq) = {!!} -- insAnyComm ? ?
-    anyc03 p₁ q₁ (there anyp) (here refl) = {!!}
-    anyc03 p₁ q₁ (there anyp) (there anyq) = {!!}
+  anyc0n [] = record { commList = FLinsert (perm→FL [ FL→perm p , FL→perm q ]) (commList (anyComm P (cons q Q qr))) ; commAny = anyc03 P Q } where
+    anyc03 :  (P Q : FList n) → (p₁ q₁ : FL n) → Any (_≡_ p₁) (cons p P {!!} ) → Any (_≡_ q₁) (cons q Q {!!}) → Any (_≡ perm→FL [ FL→perm p₁ , FL→perm q₁ ]) (FLinsert (perm→FL [ FL→perm p , FL→perm q ]) (commList (anyComm P (cons q Q {!!}))))
+    anyc03 P Q p₁ q₁ (here refl) (here refl) = {!!}
+    anyc03 P Q p₁ q₁ (here refl) (there anyq) = insAny _ (commAny (anyComm P (cons q Q qr)) p₁ q₁ (here refl) anyq ) 
+    anyc03 P Q p₁ q₁ (there anyp) (here refl) =  insAny _ (commAny (anyComm P (cons q Q qr)) p₁ q₁ anyp (here refl)) 
+    anyc03 P Q p₁ q₁ (there anyp) (there anyq) =  insAny _ (commAny (anyComm P (cons q Q qr)) p₁ q₁ anyp anyq ) 
   anyc0n (cons q₁ Q1 qr₁ ) = record { commList = FLinsert (perm→FL [ FL→perm p , FL→perm q₁ ]) (commList (anyc0n Q1)) 
                                  ; commAny = anyc01 Q1 q₁ qr₁ }