# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1607140664 -32400
# Node ID fa1e0944d1a02b28e284f858468458ea26452b12
# Parent  08166685ed2c946695af4c87312854c70df2ef30
...

diff -r 08166685ed2c -r fa1e0944d1a0 FLComm.agda
--- a/FLComm.agda	Sat Dec 05 11:49:12 2020 +0900
+++ b/FLComm.agda	Sat Dec 05 12:57:44 2020 +0900
@@ -111,19 +111,23 @@
 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) = record {
-     commList = cons (perm→FL [ FL→perm p , FL→perm q ]) (commList (anyComm (cons p P pr) Q)) anyc00 ; commAny = anyc01 } where
-  anyc00 :  fresh (FL n) ⌊ _f<?_ ⌋ (perm→FL [ FL→perm p , FL→perm q ]) (commList (anyComm (cons p P pr) Q))
+anyComm (cons p P pr) Q = anyc0n Q where
+  anyc00 : (Q : FList n) (q : FL n) → fresh (FL n) ⌊ _f<?_ ⌋ q Q → fresh (FL n) ⌊ _f<?_ ⌋ (perm→FL [ FL→perm p , FL→perm q ]) (commList (anyComm (cons p P pr) Q))
   anyc00 = {!!}
-  anyc01 :  (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₁ ]) (cons (perm→FL [ FL→perm p , FL→perm q ])  (commList (anyComm (cons p P pr) Q)) anyc00)
-  anyc01 p q   (here refl)  (here refl)  = here refl
-  anyc01 p q₁  (here refl)  (there anyq) = there (commAny (anyComm (cons p P pr) Q) p q₁ (here refl) anyq ) 
-  anyc01 p₁ q  (there anyp) (here refl) = anyc02 (commAny (anyComm P (cons q Q qr)) p₁ q anyp (here refl)) where
-    anyc02 : Any (_≡ perm→FL [ FL→perm p₁ , FL→perm q ]) (commList (anyComm P (cons q Q qr)))
-           → Any (_≡ perm→FL [ FL→perm p₁ , FL→perm q ]) (cons (perm→FL [ FL→perm p , FL→perm q ]) (commList (anyComm (cons p P pr) Q)) anyc00)
-    anyc02 t = ?
-  anyc01 p₁ q₁ (there anyp) (there anyq) = there (commAny (anyComm (cons p P pr) Q) p₁ q₁ (there anyp) anyq )
+  anyc01 :  (Q : FList n)  (q : FL n) → (qr : fresh (FL n) ⌊ _f<?_ ⌋ q Q ) → (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₁ ]) (cons (perm→FL [ FL→perm p , FL→perm q ])  (commList (anyComm (cons p P pr) Q)) (anyc00 Q q qr))
+  anyc01 Q q qr p q   (here refl)  (here refl)  = here refl
+  anyc01 Q q qr p q₁  (here refl)  (there anyq) = there (commAny (anyComm (cons p P pr) Q) p q₁ (here refl) anyq ) 
+  anyc01 Q q qr p₁ q  (there anyp) (here refl) = anyc02 Q q qr (commAny (anyComm P (cons q Q qr)) p₁ q anyp (here refl)) where
+    anyc02 :  (Q : FList n) (q : FL n) → (qr : fresh (FL n) ⌊ _f<?_ ⌋ q Q )
+           → Any (_≡ perm→FL [ FL→perm p₁ , FL→perm q ]) (commList (anyComm P (cons q Q qr)))
+           → Any (_≡ perm→FL [ FL→perm p₁ , FL→perm q ]) (cons (perm→FL [ FL→perm p , FL→perm q ]) (commList (anyComm (cons p P pr) Q)) (anyc00 Q q qr))
+    anyc02 Q q qr t = {!!}
+  anyc01 Q q qr p₁ q₁ (there anyp) (there anyq) = there (commAny (anyComm (cons p P pr) Q) p₁ q₁ (there anyp) anyq )
+  anyc0n : (Q : FList n) → AnyComm (cons p P pr) Q
+  anyc0n [] = record { commList = [] ; commAny = λ _ _ _ () }
+  anyc0n (cons q Q qr ) = record { commList = cons (perm→FL [ FL→perm p , FL→perm q ]) (commList (anyComm (cons p P pr) Q)) (anyc00 Q q qr)
+                                 ; commAny = anyc01 Q q qr }
 
 -- {-# TERMINATING #-}
 CommStage→ : (i : ℕ) → (x : Permutation n n ) → deriving i x → Any (perm→FL x ≡_) ( CommFListN i )