# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1607222660 -32400
# Node ID e6d7671d80a41e4ecad705c60316b0454402d422
# Parent  b9b39cfb3b74776d469df55887b44d46a00e8514
...

diff -r b9b39cfb3b74 -r e6d7671d80a4 FLComm.agda
--- a/FLComm.agda	Sun Dec 06 11:39:26 2020 +0900
+++ b/FLComm.agda	Sun Dec 06 11:44:20 2020 +0900
@@ -106,22 +106,22 @@
      commList : FList n
      commAny : (p q : FL n) → Any (p ≡_) P →  Any (q ≡_) Q → Any ( _≡ perm→FL [ FL→perm p , FL→perm q ] ) commList
 
-open AnyComm
+open AnyComm -- 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 = λ _ _ _ () }
-anyComm (cons p P pr) (cons q₀ Q qr₀) = anyc0n Q where
-  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)) ) 
+anyComm (cons p P pr) (cons q Q qr) = anyc0n Q where
+  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)) ) 
   anyc01 = {!!}
-  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) anyq = {!!}    -- anyq : Any (_≡_ q) (cons q₀ Q qr₀)
-    anyc03 p₁ q (there anyp) anyq = {!!} -- 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 }
+  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) anyq = {!!}    -- anyq : Any (_≡_ q) (cons q Q qr)
+    anyc03 p₁ q₁ (there anyp) anyq = {!!} -- 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₁ }
 
 -- {-# TERMINATING #-}
 CommStage→ : (i : ℕ) → (x : Permutation n n ) → deriving i x → Any (perm→FL x ≡_) ( CommFListN i )