Mercurial > hg > Members > kono > Proof > galois

changeset 220:3e9222eae43c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
section?
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 06 Dec 2020 12:34:24 +0900
parents e6d7671d80a4
children 14b518eecf82
files FLComm.agda
diffstat 1 files changed, 15 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/FLComm.agda	Sun Dec 06 11:44:20 2020 +0900
+++ b/FLComm.agda	Sun Dec 06 12:34:24 2020 +0900
@@ -112,14 +112,26 @@
 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) = anyc0n Q where
+  insAnyComm : {p₁ q₁ h : FL n } → (xs : FList n)  → Any ( perm→FL [ FL→perm p₁ , FL→perm q₁ ] ≡_ ) xs
+        → Any (perm→FL [ FL→perm p₁ , FL→perm q₁ ] ≡_ ) (FLinsert h xs)
+  insAnyComm xs any = insAny _ any
   anyc0n : (Q1 : FList n) → AnyComm (cons p P pr) (cons q Q qr)
   anyc01 :  (Q1 : FList n)  (q₁ : FL n) → (qr₁ : fresh (FL n) ⌊ _f<?_ ⌋ q₁ Q1 ) → (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₂ ]) (FLinsert (perm→FL [ FL→perm p , FL→perm q₁ ])  (commList (anyc0n Q1)) ) 
-  anyc01 = {!!}
+  anyc04 : (x b : FL n) → (L : FList n) → Any (x ≡_ )  L → Any (x ≡_ )  (FLinsert b L)
+  anyc04 a b L any = insAny L any
+  anyc01 [] q₁ qr₁ p₁ q₂ (here refl) (here refl) = {!!}
+  anyc01 [] q₁ qr₁ p₁ q₂ (here refl) (there anyq) with anyc04 (perm→FL [ FL→perm p , FL→perm q₁ ]) (perm→FL [ FL→perm p , FL→perm q₁ ]) (commList (anyc0n [])) {!!}
+  ... | t = {!!}
+  anyc01 [] q₁ qr₁ p₁ q₂ (there anyp) (here refl) =  {!!} 
+  anyc01 [] q₁ qr₁ p₁ q₂ (there anyp) (there anyq) = {!!} --  insAny (commList (anyc0n [])) {!!}  -- (commAny (anyc0n [])  p₁  q₂ (here refl) (there anyq) )
+  anyc01 (cons q₃ Q1 qr₃) q₁ qr₁ p₁ q₂ anyp anyq = {!!}
   anyc0n [] = record { commList = FLinsert (perm→FL [ FL→perm p , FL→perm q ]) (commList (anyComm P (cons q Q qr))) ; commAny = anyc03  } where
     anyc03 :  (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₁ ]) (FLinsert (perm→FL [ FL→perm p , FL→perm q ]) (commList (anyComm P (cons q Q qr))))
-    anyc03 p₁ q₁ (here refl) anyq = {!!}    -- anyq : Any (_≡_ q) (cons q Q qr)
-    anyc03 p₁ q₁ (there anyp) anyq = {!!} -- commAny (anyComm P (cons q Q qr)) p₁ q anyp anyq
+    anyc03 p₁ q₁ (here refl) (here refl) = {!!}
+    anyc03 p₁ q₁ (here refl) (there anyq) = {!!} -- insAnyComm ? ?
+    anyc03 p₁ q₁ (there anyp) (here refl) = {!!}
+    anyc03 p₁ q₁ (there anyp) (there anyq) = {!!}
   anyc0n (cons q₁ Q1 qr₁ ) = record { commList = FLinsert (perm→FL [ FL→perm p , FL→perm q₁ ]) (commList (anyc0n Q1)) 
                                  ; commAny = anyc01 Q1 q₁ qr₁ }