# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1607136552 -32400
# Node ID 08166685ed2c946695af4c87312854c70df2ef30
# Parent  2eb62a2a34f2b57bc71bdbafdda3334ac01db7a4
anyComm

diff -r 2eb62a2a34f2 -r 08166685ed2c FLComm.agda
--- a/FLComm.agda	Sat Dec 05 09:41:16 2020 +0900
+++ b/FLComm.agda	Sat Dec 05 11:49:12 2020 +0900
@@ -33,6 +33,8 @@
 open Group (Symmetric n) hiding (refl)
 open Solvable (Symmetric n) 
 open _∧_
+-- open import Relation.Nary using (⌊_⌋)
+open import Relation.Nullary.Decidable hiding (⌊_⌋)
 
 -- Flist :  {n : ℕ } (i : ℕ) → i < suc n → FList n → FList n → FList (suc n)
 -- Flist zero i<n [] _ = []
@@ -61,18 +63,22 @@
    -- loop on i 
    any02 : (i : ℕ ) → (i<n : i < suc n ) → (a : FL n) → AnyFL (suc n) (fromℕ< i<n  :: a) → AnyFL (suc n) (zero :: a)
    any02 zero (s≤s z≤n) a any = any
-   any02 (suc i) i<n a any = any02 i {!!} a {!!}
+   any02 (suc i) (s≤s i<n) a any = any02 i (<-trans i<n a<sa) a record { anyList = cons ((fromℕ< (s≤s i<n )) :: a) (anyList any) any07 ; anyP = any08 } where
+      any07 : fresh (FL (suc n)) ⌊ _f<?_ ⌋ (fromℕ< (s≤s i<n) :: a) (anyList any)
+      any07 = {!!}
+      any08 : (x : FL (suc n)) → (fromℕ< (<-trans i<n a<sa) :: a) f≤ x → Any (_≡ x) (cons (fromℕ< (s≤s i<n) :: a) (anyList any) any07 )
+      any08 = {!!}
    -- loop on a 
    any03 :  (L : FList n) → (a : FL n) →  fresh (FL n) ⌊ _f<?_ ⌋ a L  →  AnyFL (suc n) (fromℕ< a<sa :: a ) → AnyFL (suc n) FL0
    any03 [] a ar any = {!!} -- any02 n a<sa a any
-   any03 (cons b L br) a (a<b Data.Product., _) any = any03 L b br record { anyList = anyList any04 ; anyP = any05 } where
-      any06 : {n : ℕ} → zero Data.Fin.< fromℕ< {n} a<sa
-      any06 = {!!}
+   any03 (cons b L br) a ( Data.Product._,_ (Level.lift a<b)_) any = any03 L b br record { anyList = anyList any04 ; anyP = any05 } where
       any04 : AnyFL (suc n) (zero :: a)
       any04 = any02 n a<sa a any
       any05 : (x : FL (suc n)) → (fromℕ< a<sa :: b) f≤ x → Any (_≡ x) (anyList any04) -- 0<fmax : zero Data.Fin.< fromℕ< a<sa
-      any05 .(fromℕ< a<sa :: b) (case1 refl) = anyP any04 (fromℕ< a<sa :: b) (case2 (f<n any06 )) -- (fromℕ< a<sa :: b) f< x → (zero :: a) f≤ x
-      any05 x (case2 mb<x ) = anyP any04 x (case2 (f<-trans (f<n any06) mb<x ))
+      any05 x mb≤x  = anyP any04 x (any06 a b x (toWitness a<b) mb≤x) where
+         any06 : {n : ℕ } → (a b : FL n) → (x : FL (suc n)) → a f< b → (fromℕ< {n} a<sa :: b) f≤ x → (zero :: a) f≤ x 
+         any06 {suc n} a b x a<b (case1 refl) = case2 (f<n 0<fmax)
+         any06 {suc n} a b x a<b (case2 mb<x) = case2 (f<-trans (f<n 0<fmax) mb<x) 
    any01 : (i : ℕ ) → (L : FList n) → Any (_≡ FL0) L → AnyFL (suc n) fmax → AnyFL (suc n) FL0 
    any01 zero [] ()
    any01 (suc i) [] ()
@@ -80,12 +86,6 @@
    any01 (suc i) (cons .FL0 L x) (here refl) any = any01 i L {!!} {!!} -- can't happen
    any01 (suc i) (cons a L ar) (there b) any = any03 L a ar {!!}
 
--- all comm cobmbibation in P and Q
-record AnyComm (P Q : FList n) : Set where
-   field
-     commList : FList n  
-     commAny : (p q : FL n) → Any (p ≡_) P →  Any (q ≡_) Q → Any ( _≡ perm→FL [ FL→perm p , FL→perm q ] ) commList 
-
 tl3 : (FL n) → ( z : FList n) → FList n → FList n
 tl3 h [] w = w
 tl3 h (x ∷# z) w = tl3 h z (FLinsert ( perm→FL [ FL→perm h , FL→perm x ] ) w )
@@ -100,6 +100,31 @@
 CommFListN  0 = ∀Flist fmax
 CommFListN  (suc i) = CommFList (CommFListN i)
 
+-- all comm cobmbination in P and Q
+record AnyComm (P Q : FList n) : Set where
+   field
+     commList : FList n
+     commAny : (p q : FL n) → Any (p ≡_) P →  Any (q ≡_) Q → Any ( _≡ perm→FL [ FL→perm p , FL→perm q ] ) commList
+
+open AnyComm
+anyComm : (P Q : FList n) → AnyComm P Q
+anyComm [] [] = record { commList = [] ; commAny = λ _ _ () }
+anyComm [] (cons q Q qr) = record { commList = [] ; commAny = λ _ _ () }
+anyComm (cons p P pr) [] = record { commList = [] ; commAny = λ _ _ _ () }
+anyComm (cons p P pr) (cons q Q qr) = record {
+     commList = cons (perm→FL [ FL→perm p , FL→perm q ]) (commList (anyComm (cons p P pr) Q)) anyc00 ; commAny = anyc01 } where
+  anyc00 :  fresh (FL n) ⌊ _f<?_ ⌋ (perm→FL [ FL→perm p , FL→perm q ]) (commList (anyComm (cons p P pr) Q))
+  anyc00 = {!!}
+  anyc01 :  (p₁ q₁ : FL n) → Any (_≡_ p₁) (cons p P pr) → Any (_≡_ q₁) (cons q Q qr) →
+    Any (_≡ perm→FL [ FL→perm p₁ , FL→perm q₁ ]) (cons (perm→FL [ FL→perm p , FL→perm q ])  (commList (anyComm (cons p P pr) Q)) anyc00)
+  anyc01 p q   (here refl)  (here refl)  = here refl
+  anyc01 p q₁  (here refl)  (there anyq) = there (commAny (anyComm (cons p P pr) Q) p q₁ (here refl) anyq ) 
+  anyc01 p₁ q  (there anyp) (here refl) = anyc02 (commAny (anyComm P (cons q Q qr)) p₁ q anyp (here refl)) where
+    anyc02 : Any (_≡ perm→FL [ FL→perm p₁ , FL→perm q ]) (commList (anyComm P (cons q Q qr)))
+           → Any (_≡ perm→FL [ FL→perm p₁ , FL→perm q ]) (cons (perm→FL [ FL→perm p , FL→perm q ]) (commList (anyComm (cons p P pr) Q)) anyc00)
+    anyc02 t = ?
+  anyc01 p₁ q₁ (there anyp) (there anyq) = there (commAny (anyComm (cons p P pr) Q) p₁ q₁ (there anyp) anyq )
+
 -- {-# 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)