# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1606833449 -32400
# Node ID 0462c99f32cb451444db48a3a5ec5a69d1f740f5
# Parent  d9f610c9a4f1878311eef4ffd5e46d903abf9447
...

diff -r d9f610c9a4f1 -r 0462c99f32cb FLComm.agda
--- a/FLComm.agda	Tue Dec 01 16:01:02 2020 +0900
+++ b/FLComm.agda	Tue Dec 01 23:37:29 2020 +0900
@@ -48,6 +48,8 @@
 open import Algebra 
 open Group (Symmetric n) hiding (refl)
 
+open _∧_
+
 -- {-# TERMINATING #-}
 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)
@@ -68,16 +70,24 @@
    comm3 (cons a L  _) (there b) L3 = comm3 L b (FLinsert (perm→FL [ FL→perm G , FL→perm a ]) 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 = comm7 L L3 where
-       comm8 : (L4 L2 : FList n) → (a : FL n) → (xr :  fresh (FL n) ⌊ _f<?_ ⌋ a L4)
-            → Any (_≡_ (perm→FL [ g , h ])) (tl2 L4             L1 L2)
-            → Any (_≡_ (perm→FL [ g , h ])) (tl2 (cons a L4 xr) L1 L2)
-       comm8 L4 L2 a xr any = {!!}
+       comm9 : (L4 L1 L2 : FList n) → (a a₁ : FL n) → Any (_≡_ (perm→FL [ g , h ])) (tl2 L4 L1 L2) →
+           Any (_≡_ (perm→FL [ g , h ])) (tl2 L4 L1 (FLinsert (perm→FL [ FL→perm a , FL→perm a₁ ]) L2))
+       comm8 : (L L4 L2 : FList n) → (a : FL n) 
+            → Any (_≡_ (perm→FL [ g , h ])) (tl2 L4 L1 L2)
+            → Any (_≡_ (perm→FL [ g , h ])) (tl2 L4 L1 (tl3 a L L2))
+       comm8 [] L4 L2 a any = any
+       comm8 (cons a₁ L x) L4 L2 a any = comm8 L L4 (FLinsert (perm→FL [ FL→perm a , FL→perm a₁ ]) L2) a (comm9 L4 L1 L2 a a₁ any)
+       comm9 [] L1 L2 a a₁ any = insAny _ any
+       comm9 (cons a₂ L4 x) L1 L2 a a₁ any = comm8 L1 ? (FLinsert (perm→FL [ FL→perm a , FL→perm a₁ ]) L2) a {!!}
+       ---   Any (_≡_ (perm→FL [ g , h ])) (tl2 L4 L1 (tl3 a₂ L1 L2))  
+       --- → Any (_≡_ (perm→FL [ g , h ])) (tl2 (cons a₂ L4 x) L1 (FLinsert (perm→FL [ FL→perm a , FL→perm a₁ ]) L2))
+       ---                                  tl2 L4 L1 (tl3 a₂ L1 (FLinsert (perm→FL [ FL→perm a , FL→perm a₁ ] L2) 
        -- found g, we have to walk thru till the end
        comm7 : (L L3 : FList n) → Any (_≡_ (perm→FL [ g , h ])) (tl2 L L1 (tl3 G L1 L3))
        -- at the end, find h
        comm7 [] L3 = comm3 L1 b L3  
        -- add n path
-       comm7 (cons a L4 xr) L3 = comm8 L4 (tl3 G L1 L3) a xr (comm7 L4 L3) 
+       comm7 (cons a L4 xr) L3 = comm8 L1 L4 (tl3 G L1 L3) a (comm7 L4 L3)
    -- accumerate tl3
    comm2 (cons x L xr) L1 (there a) b L3 = comm2 L L1 a b (tl3 x L1 L3)
 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