Mercurial > hg > Members > kono > Proof > galois

changeset 239:f45298e34491

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
anyFL done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 09 Dec 2020 17:33:55 +0900
parents c3a67bb7cbc0
children 2b7b343616af
files FLComm.agda
diffstat 1 files changed, 5 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
--- a/FLComm.agda	Wed Dec 09 17:18:05 2020 +0900
+++ b/FLComm.agda	Wed Dec 09 17:33:55 2020 +0900
@@ -86,15 +86,13 @@
         anyFL6 (cons _ xs _) (here refl) refl = x∈FLins (x :: y)  (allListFL zero xs z)
         anyFL6 (cons _ xs  _) (there any) refl = insAny _ (anyFL6 xs any refl )
     anyFL3 {suc i} (s≤s (s≤s i<n)) (x :: y) x<i z with <-cmp (toℕ x) (suc i)
-    ... | tri< a ¬b ¬c = anyFL1 (s≤s i<n) where
-        anyFL1  : {i : ℕ} → (i<n : i < suc n) →  Any (_≡_ (x :: y)) (allListF (s≤s i<n) z)
-        anyFL10 : {j : ℕ} → (i<n : j < suc n ) → (x<i : toℕ x ≤ suc i) → (L : FList (suc n))  
+    ... | tri< a ¬b ¬c = anyFL1 (s≤s i<n) a where
+        anyFL1  : {i : ℕ} → (i<n : i < suc n) → (x<i : suc (toℕ x) ≤ suc i )  →  Any (_≡_ (x :: y)) (allListF (s≤s i<n) z)
+        anyFL10 : {i : ℕ} → (i<n : i < suc n ) → (x<i : suc (toℕ x) ≤ suc i) → (L : FList (suc n))  
             → Any (_≡_ (x :: y))  (allListFL (suc (fromℕ< i<n)) L (allListF (<-trans i<n a<sa) z) )
-        anyFL10 {j} (s≤s j<n) x<i [] = anyFL3 (<-trans (s≤s j<n) a<sa) (x :: y) (anyFL11 x<i)  z   where
-             anyFL11 : toℕ x ≤ suc i → toℕ x ≤ j 
-             anyFL11 = {!!}
+        anyFL10 {i} (s≤s j<n) (s≤s x<i) [] = anyFL3 (<-trans (s≤s j<n) a<sa) (x :: y) x<i z  --  where suc (toℕ x) ≤ suc i → toℕ x ≤ i
         anyFL10 {i} i<n x<i (cons _ xs _)  = insAny _ (anyFL10 {i} i<n x<i xs )
-        anyFL1 (s≤s i<n) = anyFL10 (s≤s i<n ) x<i (allFL (anyFL0 n)) 
+        anyFL1 {i} (s≤s i<n) x<i = anyFL10 (s≤s i<n ) x<i (allFL (anyFL0 n)) 
     ... | tri≈ ¬a b ¬c = anyFL7 (allFL (anyFL0 n)) (anyP (anyFL0 n) y) where
         anyFL9 : toℕ x ≡ suc i → x ≡ suc (fromℕ< (s≤s i<n))
         anyFL9 x=si = toℕ-injective ( begin