Mercurial > hg > Members > kono > Proof > galois

changeset 205:0525f4dabdbc

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 Wed, 02 Dec 2020 11:35:54 +0900
parents 84795e6638ce
children 5ca41a11f8ae
files FLComm.agda
diffstat 1 files changed, 6 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/FLComm.agda	Wed Dec 02 10:16:24 2020 +0900
+++ b/FLComm.agda	Wed Dec 02 11:35:54 2020 +0900
@@ -85,9 +85,13 @@
            → 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 {!!})
+       comm9← (cons a₂ L4 x) L2 a a₁ not any = comm8← L1 L4 (tl3 a₂ L1 L2) a₁ {!!} {!!}
+       -- Any (_≡_ (perm→FL [ g , h ])) (tl2 L4 L1 (tl3 a₂ L1 (FLinsert (perm→FL [ FL→perm a , FL→perm a₁ ]) L2)))
+       -- Any (_≡_ (perm→FL [ g , h ])) (tl2 L4 L1 (tl3 a₁ L1 (tl3 a₂ L1 L2)))
        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 {!!})
+       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 (subst (λ k →  Any (_≡_ (perm→FL [ g , h ])) (tl2 L4 L1  k )) {!!} any ))
+       -- Any (_≡_ (perm→FL [ g , h ])) (tl2 L4 L1 (tl3 a L (FLinsert (perm→FL [ FL→perm a , FL→perm a₁ ]) L2))) →
+       -- Any (_≡_ (perm→FL [ g , h ])) (tl2 L4 L1 (FLinsert (perm→FL [ FL→perm a , FL→perm a₁ ]) (tl3 a L L2)))
        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