Mercurial > hg > Members > kono > Proof > galois

changeset 192:a670644d5624

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 29 Nov 2020 09:24:30 +0900
parents 03d40f6e98b1
children f9aa8bb5fb1d
files FLComm.agda
diffstat 1 files changed, 10 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/FLComm.agda	Sun Nov 29 02:57:57 2020 +0900
+++ b/FLComm.agda	Sun Nov 29 09:24:30 2020 +0900
@@ -48,6 +48,7 @@
 open import Algebra 
 open Group (Symmetric n) hiding (refl)
 
+{-# 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)
 CommStage→ (suc i) .( [ g , h ] ) (comm {g} {h} p q) = comm2 (CommFListN i) (CommFListN i) (CommStage→ i g p) (CommStage→ i h q) [] where
@@ -58,7 +59,15 @@
    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 (cons a L1 x) x₁) (here refl) 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 where
+       comma :  (L1 : FList n)  →  Any (_≡_ (perm→FL [ g , h ])) (tl3 G L1 (FLinsert (perm→FL [ FL→perm G , FL→perm H ]) L3))
+       comma [] = 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 x) = {!!} where -- Any (_≡_ (perm→FL [ g , h ])) (tl3 G (cons a L2 x) (FLinsert (perm→FL [ FL→perm G , FL→perm H ]) L3))
+          commb :  Any (_≡_ (perm→FL [ g , h ]))
+               (tl3 (perm→FL g) L1 (FLinsert (perm→FL [ FL→perm G , FL→perm a ]) (FLinsert (perm→FL [ FL→perm G , FL→perm a ]) L1 )))
+          commb with x∈FLins  (perm→FL [ FL→perm G , FL→perm a ]) (FLinsert (perm→FL [ FL→perm G , FL→perm a ]) (FLinsert (perm→FL [ FL→perm G , FL→perm a ]) L1 ))
+          ... | t = {!!}
    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