# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1606664161 -32400
# Node ID 57188c35ea1af0dba05d61ef0bfa47cafafd1038
# Parent  ca656da4d4841a660f49d849f12a6e8fc7d02958
...

diff -r ca656da4d484 -r 57188c35ea1a FLComm.agda
--- a/FLComm.agda	Sun Nov 29 22:24:50 2020 +0900
+++ b/FLComm.agda	Mon Nov 30 00:36:01 2020 +0900
@@ -56,18 +56,15 @@
    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 _))  
+   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 {!!} 
    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 )
-   -- Any (_≡_ (perm→FL [ g , h ])) (tl3 G (cons H (cons a L1 x) x₁) L3)
-   comm3 (cons H L1 x₁) (here refl) L3 = comma L1 L3 where
-       commb : (a : FL n) → (L1 L3 : FList n) → (xr : fresh (FL n) ⌊ _f<?_ ⌋ a L1 )
-           → Any (_≡_ (perm→FL [ g , h ])) (tl3 G L1 (FLinsert (perm→FL [ FL→perm G , FL→perm H ]) L3))
-           → Any (_≡_ (perm→FL [ g , h ])) (tl3 G (cons a L1 xr) (FLinsert (perm→FL [ FL→perm G , FL→perm H ]) L3))
-       commb a L1 L3 xr wh = {!!}
-       comma :  (L1 L3 : FList n)  →  Any (_≡_ (perm→FL [ g , h ])) (tl3 G L1 (FLinsert (perm→FL [ FL→perm G , FL→perm H ]) L3))
-       comma [] 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 )
-       comma (cons a L1 xr) L3 = commb a L1 L3 xr (comma L1 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)
    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
diff -r ca656da4d484 -r 57188c35ea1a FLutil.agda
--- a/FLutil.agda	Sun Nov 29 22:24:50 2020 +0900
+++ b/FLutil.agda	Mon Nov 30 00:36:01 2020 +0900
@@ -304,6 +304,17 @@
 nextAny (here x₁) = there (here x₁)
 nextAny (there any) = there (there any)
 
+insAny : {n : ℕ} → {x h : FL n } → (L : FList n)  → Any (_≡_ x) L → Any (_≡_ x) (FLinsert h L)
+insAny {zero} {f0} {f0} (cons a L xr) (here refl) = here refl
+insAny {zero} {f0} {f0} (cons a L xr) (there any) = insAny {zero} {f0} {f0} L any 
+insAny {suc n} {x} {h} (cons a L xr) any with FLcmp h x | FLinsert h (cons a L xr) | inspect (FLinsert h) (cons a L xr) 
+... | tri< a₁ ¬b ¬c | [] | record { eq = eq } = ?
+... | tri< a₁ ¬b ¬c | cons a₂ t x₁ | record { eq = eq } = subst (λ k → Any (_≡_ x) k ) {!!} (there {_} {_} {_} {{!!}} {{!!}} {{!!}} any)
+... | tri≈ ¬a b ¬c | t | record { eq = eq }= subst (λ k → Any (_≡_ x) k ) {!!}  (here refl)
+insAny {suc n} {x} {h} (cons a [] xr) any | tri> ¬a ¬b c | t | record { eq = eq } = {!!}
+insAny {suc n} {x} {h} (cons a (cons a₁ L x₁) xr) (here x₂) | tri> ¬a ¬b c | t | record { eq = eq } = subst (λ k → Any (_≡_ x) k) {!!} (here {!!})
+insAny {suc n} {x} {h} (cons a (cons a₁ L x₁) xr) (there any) | tri> ¬a ¬b c | t | record { eq = eq } = subst (λ k → Any (_≡_ x) k) {!!} (there  {!!})
+
 AnyFList : {n : ℕ }  → (x : FL n ) →  Any (x ≡_ ) (∀Flist fmax)
 AnyFList {zero} f0 = here refl
 AnyFList {suc zero} (zero :: f0) = here refl