# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1607640365 -32400
# Node ID 38e56ea7d09f9b19be79545f4e972778ffea743b
# Parent  80b9fb5f80ab020fba237d0321226aad4944fbd0
remove anyFL0

diff -r 80b9fb5f80ab -r 38e56ea7d09f FLComm.agda
--- a/FLComm.agda	Fri Dec 11 07:38:09 2020 +0900
+++ b/FLComm.agda	Fri Dec 11 07:46:05 2020 +0900
@@ -58,65 +58,6 @@
 anyFL2 : (x : FL 1) → (y : FList 1) → y ≡ ((zero :: f0) ∷# []) → Any (_≡_ x) y
 anyFL2 (zero :: f0) .(cons (zero :: f0) [] (Level.lift tt)) refl = here refl
 
-anyFL0 :  (n : ℕ) → AnyFL (suc n) 
-anyFL0 zero = record { allFL = (zero :: f0) ∷# [] ; anyP = λ x → anyFL2 x ((zero :: f0) ∷# []) refl } 
-anyFL0 (suc n)  = record { allFL = allListF a<sa []; anyP = λ x → anyFL3 a<sa x (fin≤n (FLpos x)) [] } where 
-    allListFL : (x : Fin (suc (suc n))) → FList (suc n) → FList (suc (suc n)) → FList (suc (suc n))
-    allListFL _ [] y = y
-    allListFL x (cons y L yr) z = FLinsert (x :: y) (allListFL x L z) 
-    allListF : {i : ℕ} → (i<n : i < suc (suc n)) → FList (suc (suc n)) → FList (suc (suc n))
-    allListF (s≤s z≤n) z = allListFL zero (allFL (anyFL0 n)) z
-    allListF (s≤s (s≤s i<n)) z = allListFL (suc (fromℕ< (s≤s i<n ))) (allFL (anyFL0 n)) (allListF (<-trans (s≤s i<n) a<sa) z)
-    anyFL3 :  {i : ℕ} → (i<n : i < suc (suc n)) (x : FL (suc (suc n))) → (toℕ (FLpos x ) ≤ i) → (z : FList (suc (suc n))) → Any (_≡_ x) (allListF i<n z)
-    anyFL3 {zero} (s≤s z≤n) (x :: y) x<i z = anyFL6 (allFL (anyFL0 n)) (anyP (anyFL0 n) y) (anyFL5 x<i) where
-        anyFL5 : toℕ x ≤ zero → x ≡ zero
-        anyFL5 lt with <-fcmp x zero
-        ... | tri≈ ¬a b ¬c = b
-        ... | tri> ¬a ¬b c = ⊥-elim (nat-≤> x<i c)
-        anyFL6 : (L : FList (suc n)) → Any (_≡_ y) L → x ≡ zero → Any (_≡_ (x :: y)) (allListFL zero L z)
-        anyFL6 (cons _ xs _) (here refl) refl = x∈FLins (x :: y)  (allListFL zero xs z)
-        anyFL6 (cons _ xs  _) (there any) refl = insAny _ (anyFL6 xs any refl )
-    anyFL3 {suc i} (s≤s (s≤s i<n)) (x :: y) x<i z with <-cmp (toℕ x) (suc i)
-    ... | tri< a ¬b ¬c = anyFL1 (s≤s i<n) a where
-        anyFL1  : {i : ℕ} → (i<n : i < suc n) → (x<i : suc (toℕ x) ≤ suc i )  →  Any (_≡_ (x :: y)) (allListF (s≤s i<n) z)
-        anyFL10 : {i : ℕ} → (i<n : i < suc n ) → (x<i : suc (toℕ x) ≤ suc i) → (L : FList (suc n))  
-            → Any (_≡_ (x :: y))  (allListFL (suc (fromℕ< i<n)) L (allListF (<-trans i<n a<sa) z) )
-        anyFL10 {i} (s≤s j<n) (s≤s x<i) [] = anyFL3 (<-trans (s≤s j<n) a<sa) (x :: y) x<i z  
-        anyFL10 {i} i<n x<i (cons _ xs _)  = insAny _ (anyFL10 {i} i<n x<i xs )
-        anyFL1 {i} (s≤s i<n) x<i = anyFL10 (s≤s i<n ) x<i (allFL (anyFL0 n)) 
-    ... | tri≈ ¬a b ¬c = anyFL7 (allFL (anyFL0 n)) (anyP (anyFL0 n) y) where
-        anyFL9 : toℕ x ≡ suc i → x ≡ suc (fromℕ< (s≤s i<n))
-        anyFL9 x=si = toℕ-injective ( begin
-             toℕ x ≡⟨ x=si ⟩
-             suc i  ≡⟨ cong suc (≡-sym (toℕ-fromℕ< _) ) ⟩
-             suc (toℕ (fromℕ< (s≤s i<n)))  ≡⟨⟩
-             toℕ (suc (fromℕ< (s≤s i<n)))
-          ∎ ) where open ≡-Reasoning
-        anyFL8 : (L : FList (suc n)) → Any (_≡_ y) L → Any (_≡_ (x :: y)) (allListFL x L (allListF (<-trans (s≤s i<n) a<sa) z))
-        anyFL8 (cons _ xs _) (here refl) = x∈FLins (x :: y) (allListFL x xs (allListF (<-trans (s≤s i<n) a<sa) z))
-        anyFL8 (cons _ xs _) (there any) = insAny _ (anyFL8 xs any)
-        anyFL7 : (L : FList (suc n)) → Any (_≡_ y) L → Any (_≡_ (x :: y)) (allListF (s≤s (s≤s i<n)) z)
-        anyFL7 (cons _ xs _) (there any) = anyFL7 xs any
-        anyFL7 (cons _ xs _) (here refl) = subst (λ k →  Any (_≡_ (x :: y))
-            (allListFL k (allFL (anyFL0 n)) (allListF (<-trans (s≤s i<n) a<sa) z)) ) (anyFL9 b) (anyFL8 (allFL (anyFL0 n)) (anyP (anyFL0 n) y) )
-    ... | tri> ¬a ¬b c = ⊥-elim (nat-≤> x<i c)
-
-anyFL :  (n : ℕ) → AnyFL n 
-anyFL zero = record { allFL = f0 ∷# [] ; anyP = anyFL4 } where
-    anyFL4 : (x : FL zero) → Any (_≡_ x) ( f0 ∷# [] )
-    anyFL4 f0 = here refl
-anyFL (suc n) = anyFL0 n
-
-at1 = proj₁ (toList (allFL (anyFL 1)))
-at2 = proj₁ (toList (allFL (anyFL 2)))
-at3 = proj₁ (toList (allFL (anyFL 3)))
-at4 = proj₁ (toList (allFL (anyFL 4)))
-
--- open import Data.List.Fresh.Relation.Unary.All
--- at6 : All (_# allFL (anyFL 2)) (allFL (anyFL 2))
--- at6 = {!!}
--- at5 = append (allFL (anyFL 2)) (allFL (anyFL 2)) at6
-
 -- all cobmbination in P and Q
 record AnyComm {n m l : ℕ}  (P : FList n) (Q : FList m) (fpq : (p : FL n) (q : FL m) → FL l) : Set where
    field
@@ -176,7 +117,8 @@
      anyc04 [] = anyc05 P 
      anyc04 (cons a Q1 x) = insAny _ (anyc04 Q1)
 
---   anyComm ( #0 :: FL0 ... # n : FL0 ) (all n) (λ p q → FLpos p :: q ) = all (suc n)
+--   anyComm ( #0 :: FL0 ... # n :: FL0 ) (all n) (λ p q → FLpos p :: q ) = all (suc n)
+
 record AnyFin (n : ℕ)  : Set where
    field
      allFin : FList (suc n)
@@ -189,15 +131,15 @@
 anyFL01 (suc n) = record { allFL = commList anyC ;  anyP =  anyFL02 } where
      anyFL04 :  (n : ℕ) → AnyFin n
      anyFL04 n = record { allFin = anyFL05 a<sa ; anyF = λ x → anyFL06 a<sa x fin<n } where 
+         anyFL05 : {i : ℕ} → (i < suc n) → FList (suc n)
+         anyFL05 {0} (s≤s z≤n) = zero :: FL0 ∷# []
+         anyFL05 {suc i} (s≤s i<n) = FLinsert (fromℕ< (s≤s i<n) :: FL0) (anyFL05 {i} (<-trans i<n a<sa))
          anyFL08 : {n i : ℕ} {x : Fin (suc n)} {i<n : suc i < suc n}  → toℕ x ≡ suc i → x ≡ suc (fromℕ< (≤-pred i<n))
          anyFL08 {n} {i} {x} {i<n} eq = toℕ-injective ( begin
                 toℕ x                               ≡⟨ eq ⟩
                 suc i                               ≡⟨ cong suc (≡-sym (toℕ-fromℕ< _ )) ⟩
                 suc (toℕ (fromℕ< (≤-pred i<n)) )
           ∎ ) where open ≡-Reasoning
-         anyFL05 : {i : ℕ} → (i < suc n) → FList (suc n)
-         anyFL05 {0} (s≤s z≤n) = zero :: FL0 ∷# []
-         anyFL05 {suc i} (s≤s i<n) = FLinsert (fromℕ< (s≤s i<n) :: FL0) (anyFL05 {i} (<-trans i<n a<sa))
          anyFL06 : {i : ℕ} → (i<n : i < suc n) → (x : Fin (suc n)) → toℕ x < suc i → Any (_≡_ (x :: FL0)) (anyFL05 i<n)
          anyFL06 (s≤s z≤n) zero (s≤s lt) = here refl
          anyFL06 {suc i} (s≤s (s≤s i<n)) x (s≤s lt) with <-cmp (toℕ x) (suc i)
@@ -212,6 +154,22 @@
          x≤n : suc (toℕ x)  ≤ suc (suc n)
          x≤n = toℕ<n x
 
+anyFL :  (n : ℕ) → AnyFL n 
+anyFL zero = record { allFL = f0 ∷# [] ; anyP = anyFL4 } where
+    anyFL4 : (x : FL zero) → Any (_≡_ x) ( f0 ∷# [] )
+    anyFL4 f0 = here refl
+anyFL (suc n) = anyFL01 n
+
+at1 = proj₁ (toList (allFL (anyFL 1)))
+at2 = proj₁ (toList (allFL (anyFL 2)))
+at3 = proj₁ (toList (allFL (anyFL 3)))
+at4 = proj₁ (toList (allFL (anyFL 4)))
+
+-- open import Data.List.Fresh.Relation.Unary.All
+-- at6 : All (_# allFL (anyFL 2)) (allFL (anyFL 2))
+-- at6 = {!!}
+-- at5 = append (allFL (anyFL 2)) (allFL (anyFL 2)) at6
+
 CommFListN  : ℕ →  FList n
 CommFListN  zero = allFL (anyFL n)
 CommFListN (suc i ) = commList (anyComm ( CommFListN i ) ( CommFListN i ) (λ p q →  perm→FL [ FL→perm p , FL→perm q ] ))
@@ -230,7 +188,6 @@
   comm2 : Any (_≡_ (perm→FL [ g , h ])) (CommFListN (suc i))
   comm2 = subst (λ k → Any (_≡_ k) (CommFListN (suc i)) ) comm3
      ( commAny ( anyComm (CommFListN i) (CommFListN i) (λ p q →  perm→FL [ FL→perm p , FL→perm q ] )) G H (CommStage→ i g p) (CommStage→ i h q) )
-
 CommStage→ (suc i) x (ccong {f} {x} eq p) =
       subst (λ k → Any (k ≡_) (commList (anyComm ( CommFListN i ) ( CommFListN i ) (λ p q →  perm→FL [ FL→perm p , FL→perm q ] ))))
           (comm4 eq) (CommStage→ (suc i) f p ) where