Mercurial > hg > Members > kono > Proof > galois

changeset 202:d9f610c9a4f1

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 Tue, 01 Dec 2020 16:01:02 +0900
parents a626ab1dbbcd
children 0462c99f32cb
files FLComm.agda
diffstat 1 files changed, 5 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
--- a/FLComm.agda	Mon Nov 30 18:02:06 2020 +0900
+++ b/FLComm.agda	Tue Dec 01 16:01:02 2020 +0900
@@ -68,18 +68,16 @@
    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
-       comm8 : (L5 L4 L3 : FList n) → (a : FL n)
-            → Any (_≡_ (perm→FL [ g , h ])) (tl2 L4 L1           (tl3 G L1 L3))
-            → Any (_≡_ (perm→FL [ g , h ])) (tl2 L4 L1 (tl3 a L5 (tl3 G L1 L3)))
-       comm8 L5 [] L3 a any = {!!}
-       comm8 L5 (cons a₁ L4 x) L3 a any with comm8 L5 L4 L3 a₁ {!!}
-       ... | t = {!!}
+       comm8 : (L4 L2 : FList n) → (a : FL n) → (xr :  fresh (FL n) ⌊ _f<?_ ⌋ a L4)
+            → Any (_≡_ (perm→FL [ g , h ])) (tl2 L4             L1 L2)
+            → Any (_≡_ (perm→FL [ g , h ])) (tl2 (cons a L4 xr) L1 L2)
+       comm8 L4 L2 a xr any = {!!}
        -- found g, we have to walk thru till the end
        comm7 : (L L3 : FList n) → Any (_≡_ (perm→FL [ g , h ])) (tl2 L L1 (tl3 G L1 L3))
        -- at the end, find h
        comm7 [] L3 = comm3 L1 b L3  
        -- add n path
-       comm7 (cons a L4 x) L3 = comm8 L1 L4 L3 a (comm7 L4 L3)
+       comm7 (cons a L4 xr) L3 = comm8 L4 (tl3 G L1 L3) a xr (comm7 L4 L3) 
    -- accumerate tl3
    comm2 (cons x L xr) L1 (there a) b L3 = comm2 L L1 a b (tl3 x L1 L3)
 CommStage→ (suc i) x (ccong {f} {x} eq p) = subst (λ k → Any (k ≡_) (tl2 (CommFListN i) (CommFListN i) [])) (comm4 eq) (CommStage→ (suc i) f p ) where