Mercurial > hg > Members > kono > Proof > galois
changeset 219:e6d7671d80a4
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 06 Dec 2020 11:44:20 +0900 |
parents | b9b39cfb3b74 |
children | 3e9222eae43c |
files | FLComm.agda |
diffstat | 1 files changed, 11 insertions(+), 11 deletions(-) [+] |
line wrap: on
line diff
--- a/FLComm.agda Sun Dec 06 11:39:26 2020 +0900 +++ b/FLComm.agda Sun Dec 06 11:44:20 2020 +0900 @@ -106,22 +106,22 @@ commList : FList n commAny : (p q : FL n) → Any (p ≡_) P → Any (q ≡_) Q → Any ( _≡ perm→FL [ FL→perm p , FL→perm q ] ) commList -open AnyComm +open AnyComm -- q₂ anyComm : (P Q : FList n) → AnyComm P Q 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) (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)) ) +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 = 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 } + 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₁ } -- {-# TERMINATING #-} CommStage→ : (i : ℕ) → (x : Permutation n n ) → deriving i x → Any (perm→FL x ≡_) ( CommFListN i )