Mercurial > hg > Members > kono > Proof > galois

changeset 217:479820ca372e

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, 06 Dec 2020 11:18:58 +0900
parents 658789e98091
children b9b39cfb3b74
files FLComm.agda
diffstat 1 files changed, 7 insertions(+), 12 deletions(-) [+]
line wrap: on
line diff
--- a/FLComm.agda	Sun Dec 06 07:28:42 2020 +0900
+++ b/FLComm.agda	Sun Dec 06 11:18:58 2020 +0900
@@ -113,19 +113,14 @@
 anyComm (cons p P pr) [] = record { commList = [] ; commAny = λ _ _ _ () }
 anyComm (cons p P pr) Q = anyc0n Q where
   anyc0n : (Q1 : FList n) → AnyComm (cons p P pr) Q
-  anyc00 : (Q1 : FList n) (q : FL n) → fresh (FL n) ⌊ _f<?_ ⌋ q Q1 → fresh (FL n) ⌊ _f<?_ ⌋ (perm→FL [ FL→perm p , FL→perm q ]) (commList (anyc0n Q1))
-  anyc00 = {!!}
   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₁) Q →
-    Any (_≡ perm→FL [ FL→perm p₁ , FL→perm q₁ ]) (cons (perm→FL [ FL→perm p , FL→perm q ])  (commList (anyc0n Q1)) (anyc00 Q1 q qr)) 
-  anyc01 Q1 q qr p q₁   (here refl)  (here refl)  = here {!!}
-  anyc01 Q1 q qr p q₁  (here refl)  (there anyq) = there (commAny (anyc0n  Q1) p q₁ (here refl) {!!} ) 
-  anyc01 Q1 q qr p₁ q₁  (there anyp) (here refl)  = there  {!!} 
-  anyc01 Q1 q qr p₁ q₁ (there anyp) (there anyq) = there (commAny (anyc0n Q1) p₁ q₁ (there anyp) {!!} )
-  anyc0n [] = record { commList = (commList (anyComm P Q)) ; commAny = λ p₁ q anyp anyq → commAny (anyComm P Q) p₁ q (anyc03 anyp) anyq } where
-    anyc03 : {p₁ : FL n} → Any (_≡_ p₁) (cons p P pr) → Any (_≡_ p₁) P
-    anyc03 (here x) = {!!}
-    anyc03 (there any) = any
-  anyc0n (cons q Q1 qr ) = record { commList = cons (perm→FL [ FL→perm p , FL→perm q ]) (commList (anyc0n Q1)) (anyc00 Q1 q qr)
+    Any (_≡ perm→FL [ FL→perm p₁ , FL→perm q₁ ]) (FLinsert (perm→FL [ FL→perm p , FL→perm q ])  (commList (anyc0n Q1)) ) 
+  anyc01 = {!!}
+  anyc0n [] = record { commList = commList (anyComm P Q) ; commAny = anyc03  } where
+    anyc03 :  (p₁ q : FL n) → Any (_≡_ p₁) (cons p P pr) → Any (_≡_ q) Q → Any (_≡ perm→FL [ FL→perm p₁ , FL→perm q ]) (commList (anyComm P Q))
+    anyc03 p₁ q (here refl) anyq = {!!}
+    anyc03 p₁ q (there anyp) anyq = commAny (anyComm P Q) p₁ q anyp 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 }
 
 -- {-# TERMINATING #-}