Mercurial > hg > Members > kono > Proof > galois

changeset 178:2b4eec28eb13

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
dead end
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 25 Nov 2020 23:28:51 +0900
parents c8345c4a4c4b
children abc6acbd4452
files FLutil.agda
diffstat 1 files changed, 7 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/FLutil.agda	Wed Nov 25 09:41:50 2020 +0900
+++ b/FLutil.agda	Wed Nov 25 23:28:51 2020 +0900
@@ -263,8 +263,13 @@
 AnyFList0 x L fr with FLcmp x FL0
 ... | tri< a ¬b ¬c = ⊥-elim (¬x<FL0 a)
 ... | tri≈ ¬a refl ¬c = here refl
-AnyFList0 x [] fr | tri> ¬a ¬b c = {!!}
-AnyFList0 x (cons a L ar) fr | tri> ¬a ¬b c = {!!}
+AnyFList0 {n} x L xr | tri> ¬a ¬b c = af0 x L c xr (here refl) where
+   af0 : (y : FL n) → (L : FList n) → (c : FL0 f< y) → (yr : fresh (FL n) ⌊ _f<?_ ⌋ y L ) →  Any (x ≡_ ) (cons y L yr)
+       → Any (x ≡_ ) (∀Flist (fpred y c) (cons y L yr) ( Level.lift (fromWitness (fpred< y c)) , ttf (fpred< y c) L yr)) 
+   af0 y L c yr any with FLcmp (fpred y c) FL0
+   ... | tri< a ¬b ¬c = ⊥-elim (¬x<FL0 a)
+   ... | tri≈ ¬a b ¬c = subst (λ k → Any (x ≡_ ) k) {!!} (there any)
+   ... | tri> ¬a ¬b c₁ = {!!}
 
 {-# TERMINATING #-}
 AnyFList : {n : ℕ }  → (x : FL (suc n) ) →  Any (x ≡_ ) (∀Flist fmax [] (Level.lift tt))