Mercurial > hg > Members > kono > Proof > galois
changeset 155:88585eeb917c
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 15 Sep 2020 09:25:45 +0900 |
| parents | 61bfb2c5e03d |
| children | 05fdfd07cabc |
| files | FLutil.agda |
| diffstat | 1 files changed, 8 insertions(+), 2 deletions(-) [+] |
line wrap: on
line diff
--- a/FLutil.agda Tue Sep 15 09:00:23 2020 +0900 +++ b/FLutil.agda Tue Sep 15 09:25:45 2020 +0900 @@ -221,13 +221,19 @@ x∈FLins {suc n} x (cons a [] x₁) | tri> ¬a ¬b a<x = there ( here refl ) x∈FLins {suc n} x (cons a (cons a₁ xs x₂) x₁) | tri> ¬a ¬b a<x = there ( x∈FLins x (cons a₁ xs x₂) ) +open import fin + x∈∀Flist : {n : ℕ } → (x : FL n ) → Any (x ≡_ ) (∀Flist fmax) x∈∀Flist {n} x = AFlist1 n x where + AFList0 : (n : ℕ ) → Any (_≡_ (fromℕ< a<sa :: fmax)) (Flist1 n a<sa (∀Flist fmax) (∀Flist fmax)) + AFList0 = {!!} + AFList2 : (n : ℕ ) (x : FL (suc n)) → (x1 : Fin (suc n)) (y : FL n) → x f< ( x1 :: y) → Any (_≡_ x) (Flist1 n a<sa (∀Flist y) (∀Flist y)) + AFList2 = {!!} AFlist1 : (n : ℕ ) → (x : FL n) → Any (_≡_ x) (∀Flist fmax) AFlist1 zero f0 = here refl AFlist1 (suc n) x with FLcmp x fmax - ... | tri< a ¬b ¬c = {!!} - ... | tri≈ ¬a refl ¬c = {!!} + ... | tri< a ¬b ¬c = AFList2 n x (fromℕ< a<sa) (fmax {n}) (fmax¬ ¬b) + ... | tri≈ ¬a refl ¬c = AFList0 n ... | tri> ¬a ¬b c = ⊥-elim ( fmax< c )