# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1606575915 -32400
# Node ID d0b678eec506e6154e61cd3bbc4db791cdf1f601
# Parent  9e0d946d35b6c54aa2a761b91edf28511eaae20b
...

diff -r 9e0d946d35b6 -r d0b678eec506 FLComm.agda
--- a/FLComm.agda	Sat Nov 28 21:50:16 2020 +0900
+++ b/FLComm.agda	Sun Nov 29 00:05:15 2020 +0900
@@ -46,18 +46,29 @@
 CommFListN  (suc i) = CommFList (CommFListN i)
 
 open import Algebra 
-open Group (Symmetric n)
+open Group (Symmetric n) hiding (refl)
 
 CommStage→ : (i : ℕ) → (x : Permutation n n ) → deriving i x → Any (perm→FL x ≡_) ( CommFListN i )
 CommStage→ zero x (Level.lift tt) = AnyFList (perm→FL x)
 CommStage→ (suc i) .( [ g , h ] ) (comm {g} {h} p q) = comm2 (CommFListN i) (CommFListN i) (CommStage→ i g p) (CommStage→ i h q) [] where
    G = perm→FL g
    H = perm→FL h
-   comm3 : (L L1 : FList n) → (xr : fresh (FL n) ⌊ _f<?_ ⌋ G L ) → Any (H ≡_) L1 → (L3 : FList n) → Any (_≡_ (perm→FL [ g , h ])) (tl2 (cons G L xr) L1 L3)
-   comm3 [] L1 _ b L3 = {!!}
-   comm3 (cons a L x) L1 _ b L3 = {!!}
+   comm6 : perm→FL [ FL→perm G , FL→perm H ] ≡ perm→FL [ g , h ]
+   comm6 = pcong-pF (comm-resp (FL←iso _) (FL←iso _))  
+   comm3 : (L1 : FList n) → Any (H ≡_) L1 → (L3 : FList n) → Any (_≡_ (perm→FL [ g , h ])) (tl3 G L1 L3)
+   comm3 (H ∷# []) (here refl) L3 = subst (λ k → Any (_≡_  k) (FLinsert (perm→FL [ FL→perm G , FL→perm H ]) L3 ) )
+       comm6 (x∈FLins ( perm→FL [ FL→perm G , FL→perm H ] ) L3 )
+   comm3 (H ∷# cons a L1 x) (here refl) L3 = ?
+   comm3 (cons _ _ _) (there b) L3 = {!!}
    comm2 : (L L1 : FList n) → Any (G ≡_) L → Any (H ≡_) L1 → (L3 : FList n) → Any (perm→FL [ g , h ]  ≡_) (tl2 L L1 L3)
-   comm2 (cons G L xr) L1 (here refl) b L3 = comm3 L L1 xr b L3
+   comm2 (cons G L xr) L1 (here refl) b L3 = comm7 L L3 where
+       comm7 : (L L3 : FList n) → Any (_≡_ (perm→FL [ g , h ])) (tl2 L L1 (tl3 G L1 L3))
+       comm8 : (L5 L4 L3 : FList n) → (a : FL n) → Any (_≡_ (perm→FL [ g , h ])) (tl2 L4 L1 (tl3 a L5 (tl3 (perm→FL g) L1 L3)))
+       comm8 [] L4 L3 a = comm7 L4 L3
+       comm8 (cons a₁ L5 x) L4 L3 a = {!!}
+       -- subst (λ k → Any (_≡_ (perm→FL [ g , h ])) k) {!!} (comm8 L5 L4 (cons a L3 {!!}) a₁ ) 
+       comm7 [] L3 = comm3 L1 b L3  
+       comm7 (cons a L4 x) L3 = comm8 L1 L4 L3 a
    comm2 (cons x L xr) L1 (there a) b L3 = comm2 L L1 a b {!!}
 CommStage→ (suc i) x (ccong {f} {x} eq p) = subst (λ k → Any (k ≡_) (tl2 (CommFListN i) (CommFListN i) [])) (comm4 eq) (CommStage→ (suc i) f p ) where
    comm4 : f =p= x →  perm→FL f ≡ perm→FL x