# HG changeset patch # User Shinji KONO # Date 1606706827 -32400 # Node ID b5b4ee29cbe479dcb054d6439b0a1c9da07a8cf1 # Parent 6c81c3d535d152a73897560e01d6bca9edae2782 TERMINATING AnyFList diff -r 6c81c3d535d1 -r b5b4ee29cbe4 FLComm.agda --- a/FLComm.agda Mon Nov 30 10:13:22 2020 +0900 +++ b/FLComm.agda Mon Nov 30 12:27:07 2020 +0900 @@ -48,7 +48,7 @@ open import Algebra open Group (Symmetric n) hiding (refl) -{-# TERMINATING #-} +-- {-# TERMINATING #-} CommStage→ : (i : ℕ) → (x : Permutation n n ) → deriving i x → Any (perm→FL x ≡_) ( CommFListN i ) CommStage→ zero x (Level.lift tt) = AnyFList (perm→FL x) CommStage→ (suc i) .( [ g , h ] ) (comm {g} {h} p q) = comm2 (CommFListN i) (CommFListN i) (CommStage→ i g p) (CommStage→ i h q) [] where @@ -71,10 +71,11 @@ comm7 : (L L3 : FList n) → Any (_≡_ (perm→FL [ g , h ])) (tl2 L L1 (tl3 G L1 L3)) comm8 : (L5 L4 L3 : FList n) → (a : FL n) → Any (_≡_ (perm→FL [ g , h ])) (tl2 L4 L1 (tl3 a L5 (tl3 (perm→FL g) L1 L3))) comm8 [] L4 L3 a = comm7 L4 L3 - comm8 (cons a₁ L5 x) L4 L3 a = {!!} + comm8 (cons a₁ L5 x) [] L3 a = {!!} + comm8 (cons a₁ L5 x) (cons a₂ L4 x₁) L3 a = subst (λ k → Any (_≡_ (perm→FL [ g , h ])) k) {!!} (comm8 L5 (cons a₂ L4 x₁) L3 a₂) comm7 [] L3 = comm3 L1 b L3 comm7 (cons a L4 x) L3 = comm8 L1 L4 L3 a - comm2 (cons x L xr) L1 (there a) b L3 = comm2 L L1 a b {!!} + comm2 (cons x L xr) L1 (there a) b L3 = comm2 L L1 a b (tl3 x L1 L3) CommStage→ (suc i) x (ccong {f} {x} eq p) = subst (λ k → Any (k ≡_) (tl2 (CommFListN i) (CommFListN i) [])) (comm4 eq) (CommStage→ (suc i) f p ) where comm4 : f =p= x → perm→FL f ≡ perm→FL x comm4 = pcong-pF diff -r 6c81c3d535d1 -r b5b4ee29cbe4 FLutil.agda --- a/FLutil.agda Mon Nov 30 10:13:22 2020 +0900 +++ b/FLutil.agda Mon Nov 30 12:27:07 2020 +0900 @@ -314,24 +314,29 @@ insAny {suc n} {x} {h} (cons a (cons a₁ L x₁) xr) (here refl) | tri> ¬a ¬b c = here refl insAny {suc n} {x} {h} (cons a (cons a₁ L x₁) xr) (there any) | tri> ¬a ¬b c = there (insAny (cons a₁ L x₁) any) +{-# TERMINATING #-} AnyFList : {n : ℕ } → (x : FL n ) → Any (x ≡_ ) (∀Flist fmax) AnyFList {zero} f0 = here refl AnyFList {suc zero} (zero :: f0) = here refl AnyFList {suc (suc n)} (x :: y) = subst (λ k → Any (_≡_ (k :: y)) (Flist (suc n) a ¬a ¬b c = ⊥-elim ( nat-≤> x