# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1606871784 -32400
# Node ID 84795e6638cec4839f338727e46eb50b541d6657
# Parent  0462c99f32cb451444db48a3a5ec5a69d1f740f5
commutativity of  Any _ (tl2 L4 L1 L2) and Any _ (tl2 L4 L1 (tl3 a L L2))

diff -r 0462c99f32cb -r 84795e6638ce FLComm.agda
--- a/FLComm.agda	Tue Dec 01 23:37:29 2020 +0900
+++ b/FLComm.agda	Wed Dec 02 10:16:24 2020 +0900
@@ -56,32 +56,44 @@
 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
-   comm6 : perm→FL [ FL→perm G , FL→perm H ] ≡ perm→FL [ g , h ]
-   comm6 = pcong-pF (comm-resp (FL←iso _) (FL←iso _))  
+
+   -- tl3 case
    commc :  (L3 L1 : FList n) →  Any (_≡_ (perm→FL [  FL→perm G , FL→perm H ])) L3 
            →  Any (_≡_ (perm→FL [ FL→perm G , FL→perm H ])) (tl3 G L1 L3)
    commc L3 [] any = any
    commc L3 (cons a L1 _) any = commc (FLinsert (perm→FL [ FL→perm G , FL→perm a ]) L3) L1 (insAny _ any)
+   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 (cons H L1 x₁) (here refl) L3 = subst (λ k → Any (_≡_ k) (tl3 G L1 (FLinsert (perm→FL [ FL→perm G , FL→perm H ]) L3))) comm6
        (commc (FLinsert (perm→FL [ FL→perm G , FL→perm H ]) L3 ) L1 (x∈FLins ( perm→FL [ FL→perm G , FL→perm H ] ) L3))
    comm3 (cons a L  _) (there b) L3 = comm3 L b (FLinsert (perm→FL [ FL→perm G , FL→perm a ]) L3)
+
+   -- tl2 case
    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
-       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← : (L L4 L2 : FList n) → (a : FL n)  → ¬ ( a ≡ perm→FL g )
+           →  Any (_≡_ (perm→FL [ g , h ])) (tl2 L4 L1 (tl3 a L L2))
+           →  Any (_≡_ (perm→FL [ g , h ])) (tl2 L4 L1 L2)
+       comm9← : (L4 L2 : FList n) → (a a₁ : FL n) → ¬ ( a ≡ perm→FL g )
+           → Any (_≡_ (perm→FL [ g , h ])) (tl2 L4 L1 (FLinsert (perm→FL [ FL→perm a , FL→perm a₁ ]) L2))
+           → Any (_≡_ (perm→FL [ g , h ])) (tl2 L4 L1 L2) 
+       --  Any (_≡_ (perm→FL [ g , h ])) (FLinsert (perm→FL [ FL→perm a , FL→perm a₁ ]) L2) → Any (_≡_ (perm→FL [ g , h ])) L2
+       comm9← [] L2 a a₁ not any = {!!}
+       comm9← (cons a₂ L4 x) L2 a a₁ not any = comm8← L1 L4 {!!} a₂ {!!} (comm9← L4 {!!} a a₁ not {!!})
+       comm8← [] L4 L2 a _ any = any 
+       comm8← (cons a₁ L x) L4 L2 a not any  = comm8← L  L4 L2 a not (comm9← L4 (tl3 a L L2 ) a a₁ not {!!})
+       comm9 : (L4 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 [] 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) 
+       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 L2 a a₁ any)
+       comm9 [] L2 a a₁ any = insAny _ any
+       comm9 (cons a₂ L4 x) L2 a a₁ any = comm8 L1 L4 (FLinsert (perm→FL [ FL→perm a , FL→perm a₁ ]) L2) a₂ (comm9 L4 L2 a a₁ (comm8← L1 L4 L2 a₂ {!!} any))
        -- 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