Mercurial > hg > Members > kono > Proof > galois
changeset 218:b9b39cfb3b74
...
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 }