Mercurial > hg > Members > kono > Proof > galois
changeset 199:6c81c3d535d1
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 30 Nov 2020 10:13:22 +0900 |
| parents | c93a60686dce |
| children | b5b4ee29cbe4 |
| files | FLutil.agda |
| diffstat | 1 files changed, 10 insertions(+), 4 deletions(-) [+] |
line wrap: on
line diff
--- a/FLutil.agda Mon Nov 30 08:07:55 2020 +0900 +++ b/FLutil.agda Mon Nov 30 10:13:22 2020 +0900 @@ -322,10 +322,16 @@ AnyFList1 : (i x : ℕ) → (i<n : i < suc (suc n) ) → (L L1 : FList (suc n) ) → (x<n : x < suc (suc n) ) → x < suc i → Any (y ≡_ ) L → Any (((fromℕ< x<n) :: y) ≡_ ) (Flist i i<n L L1) AnyFList1 zero x i<n [] L1 (s≤s x<i) _ () - AnyFList1 zero zero i<n (cons a L xr) L1 x<n (s≤s z≤n) (here refl) = x∈FLins (zero :: a) (Flist 0 i<n L L1) - AnyFList1 zero zero i<n (cons a L xr) L1 x<n (s≤s z≤n) (there wh) with AnyFList1 zero zero i<n L L1 x<n (s≤s z≤n) wh - ... | t = {!!} - AnyFList1 (suc i) x i<n L L1 x<n x<i wh = {!!} + AnyFList1 zero zero i<n (cons y L xr) L1 x<n (s≤s z≤n) (here refl) = x∈FLins (zero :: y) (Flist 0 i<n L L1) + AnyFList1 zero zero i<n (cons a L xr) L1 x<n (s≤s z≤n) (there wh) = insAny _ (AnyFList1 zero zero i<n L L1 x<n (s≤s z≤n) wh) + AnyFList1 (suc i) x (s≤s i<n) (cons y L x₁) L1 x<n (s≤s x<i) (here refl) with <-fcmp (fromℕ< x<n) (fromℕ< (s≤s i<n)) + ... | tri< a ¬b ¬c = insAny _ af1 where + af1 : Any (_≡_ (fromℕ< x<n :: y)) (Flist (suc i) (s≤s i<n) L L1) + af1 = AnyFList1 (suc i) x (s≤s i<n) L L1 x<n (s≤s x<i) {!!} + ... | tri≈ ¬a b ¬c = subst (λ k → Any (_≡_ (fromℕ< x<n :: y)) (FLinsert k (Flist (suc i) (s≤s i<n) L L1) )) (cong (λ k → k :: y) b) + (x∈FLins (fromℕ< x<n :: y) (Flist (suc i) (s≤s i<n) L L1)) + ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> x<i (subst₂ (λ j k → suc (suc k) ≤ j ) (toℕ-fromℕ< _) (toℕ-fromℕ< _) c) ) + AnyFList1 (suc i) x i<n (cons a L x₁) L1 x<n (s≤s x<i) (there wh) = {!!} -- FLinsert membership