Mercurial > hg > Members > kono > Proof > galois

changeset 218:b9b39cfb3b74

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:39:26 +0900
parents 479820ca372e
children e6d7671d80a4
files FLComm.agda
diffstat 1 files changed, 7 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
--- a/FLComm.agda	Sun Dec 06 11:18:58 2020 +0900
+++ b/FLComm.agda	Sun Dec 06 11:39:26 2020 +0900
@@ -111,15 +111,15 @@
 anyComm [] [] = record { commList = [] ; commAny = λ _ _ () }
 anyComm [] (cons q Q qr) = record { commList = [] ; commAny = λ _ _ () }
 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
-  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 →
+anyComm (cons p P pr) (cons q₀ Q qr₀) = anyc0n Q where
+  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 = {!!}
-  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 [] = 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
   anyc0n (cons q Q1 qr ) = record { commList = FLinsert (perm→FL [ FL→perm p , FL→perm q ]) (commList (anyc0n Q1)) 
                                  ; commAny = anyc01 Q1 q qr }