# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1607207322 -32400
# Node ID 658789e98091fa11dc35b78067a9a67de24a0f3a
# Parent  189ce31dc52a8bf00c556b2af9a1a9f0322d39a0
restart anyComm

diff -r 189ce31dc52a -r 658789e98091 FLComm.agda
--- a/FLComm.agda	Sun Dec 06 06:40:38 2020 +0900
+++ b/FLComm.agda	Sun Dec 06 07:28:42 2020 +0900
@@ -111,27 +111,22 @@
 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) Q = anyc0n Q Q where
-  anyc0n : (Q Q1 : FList n) → AnyComm (cons p P pr) Q
-  anyc00 : (Q1 : FList n) (q : FL n) → fresh (FL n) ⌊ _f<?_ ⌋ q Q1 → fresh (FL n) ⌊ _f<?_ ⌋ (perm→FL [ FL→perm p , FL→perm q ]) (commList (anyc0n Q Q1))
+anyComm (cons p P pr) Q = anyc0n Q where
+  anyc0n : (Q1 : FList n) → AnyComm (cons p P pr) Q
+  anyc00 : (Q1 : FList n) (q : FL n) → fresh (FL n) ⌊ _f<?_ ⌋ q Q1 → fresh (FL n) ⌊ _f<?_ ⌋ (perm→FL [ FL→perm p , FL→perm q ]) (commList (anyc0n Q1))
   anyc00 = {!!}
-  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 Q1 qr) →
-    Any (_≡ perm→FL [ FL→perm p₁ , FL→perm q₁ ]) (cons (perm→FL [ FL→perm p , FL→perm q ])  (commList (anyc0n Q Q1)) (anyc00 Q1 q qr)) 
-  anyc01 Q1 q qr p q   (here refl)  (here refl)  = here refl
-  anyc01 Q1 q qr p q₁  (here refl)  (there anyq) = there (commAny (anyc0n  Q Q1) p q₁ (here refl) ? ) 
-  anyc01 Q1 q qr p₁ q  (there anyp) (here refl)  with commAny (anyc0n Q []) p₁ q (there anyp) {!!} --  Any (_≡_ q) Q
-  ... | t = {!!}
-   where
-    -- anyc02 Q p₁ q qr anyp where
-    anyc02 :  {P : FList n} {p₂ : FL n} {pr₂ : fresh (FL n) ⌊ _f<?_ ⌋ p₂ P}
-           → (Q1 : FList n) (p₁ q : FL n) → (qr : fresh (FL n) ⌊ _f<?_ ⌋ q Q1 ) → Any (_≡_ p₁) (cons p₂ P pr₂)
-           → Any (_≡ perm→FL [ FL→perm p₁ , FL→perm q ]) (cons (perm→FL [ FL→perm p , FL→perm q ]) (commList (anyc0n Q Q1)) (anyc00 Q1 q qr)) 
-    anyc02 {P} Q1 p₁ q qr (here refl) = {!!}
-    anyc02 {P} Q1 p₁ q qr (there any) = {!!}
-  anyc01 Q1 q qr p₁ q₁ (there anyp) (there anyq) = there (commAny (anyc0n Q Q1) p₁ q₁ (there anyp) ? )
-  anyc0n Q [] = record { commList = (commList (anyComm P Q)) ; commAny = ? }
-  anyc0n Q (cons q Q1 qr ) = record { commList = cons (perm→FL [ FL→perm p , FL→perm q ]) (commList (anyc0n Q Q1)) ? 
-                                 ; commAny = ? }
+  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₁) Q →
+    Any (_≡ perm→FL [ FL→perm p₁ , FL→perm q₁ ]) (cons (perm→FL [ FL→perm p , FL→perm q ])  (commList (anyc0n Q1)) (anyc00 Q1 q qr)) 
+  anyc01 Q1 q qr p q₁   (here refl)  (here refl)  = here {!!}
+  anyc01 Q1 q qr p q₁  (here refl)  (there anyq) = there (commAny (anyc0n  Q1) p q₁ (here refl) {!!} ) 
+  anyc01 Q1 q qr p₁ q₁  (there anyp) (here refl)  = there  {!!} 
+  anyc01 Q1 q qr p₁ q₁ (there anyp) (there anyq) = there (commAny (anyc0n Q1) p₁ q₁ (there anyp) {!!} )
+  anyc0n [] = record { commList = (commList (anyComm P Q)) ; commAny = λ p₁ q anyp anyq → commAny (anyComm P Q) p₁ q (anyc03 anyp) anyq } where
+    anyc03 : {p₁ : FL n} → Any (_≡_ p₁) (cons p P pr) → Any (_≡_ p₁) P
+    anyc03 (here x) = {!!}
+    anyc03 (there any) = any
+  anyc0n (cons q Q1 qr ) = record { commList = cons (perm→FL [ FL→perm p , FL→perm q ]) (commList (anyc0n Q1)) (anyc00 Q1 q qr)
+                                 ; commAny = anyc01 Q1 q qr }
 
 -- {-# TERMINATING #-}
 CommStage→ : (i : ℕ) → (x : Permutation n n ) → deriving i x → Any (perm→FL x ≡_) ( CommFListN i )