Mercurial > hg > Members > kono > Proof > galois

changeset 169:d69252685ed9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
... ?
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 23 Nov 2020 12:13:02 +0900
parents 17c19100ecfd
children 53d31ba08456
files FLutil.agda
diffstat 1 files changed, 11 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/FLutil.agda	Mon Nov 23 11:09:44 2020 +0900
+++ b/FLutil.agda	Mon Nov 23 12:13:02 2020 +0900
@@ -246,7 +246,17 @@
     af4  : (i : ℕ) → (i<n : i < suc n) 
         → (a : FL n) → (y : FList n) → fresh (FL n) ⌊ _f<?_ ⌋ a y  
         → (y1 : FList (suc n)) → fresh (FL (suc n)) ⌊ _f<?_ ⌋ (fromℕ< i<n :: a) y1  →  FList (suc n)
-    af4 i i<n y a fr y1 fr1 = {!!}
+    af4 zero i<n a [] fr y1 fr1 = cons (fromℕ< i<n :: a) y1 fr1
+    --  a < a₁
+    af4 zero i<n a (cons a₁ y x) (lift p , fr) y1 fr1 = af4 zero i<n a₁ y x (cons (fromℕ< i<n :: a) y1 fr1) {!!} where
+        af41 : fresh (FL (suc n)) ⌊ _f<?_ ⌋ (fromℕ< i<n :: a) (cons (fromℕ< i<n :: a₁) y1 {!!})
+        af41 = Level.lift (fromWitness (f<t {!!})) , ttf {!!} y1 fr1
+    af4 (suc i) (s≤s i<n) a' [] fr' y1 fr1 = af4 i (<-trans i<n a<sa) a y fr y1 af42 where
+        af42 : fresh (FL (suc n)) ⌊ _f<?_ ⌋ (fromℕ< (<-trans i<n a<sa) :: a) y1
+        af42 = {!!}
+    af4 (suc i) (s≤s i<n) a (cons a₁ y x) (lift p , fr) y1 fr1 = af4 (suc i) (s≤s i<n) a₁ y x (cons  (fromℕ< (s≤s i<n) :: a) y1 fr1) af43 where
+        af43 : fresh (FL (suc n)) ⌊ _f<?_ ⌋ (fromℕ< (s≤s i<n) :: a₁) (cons (fromℕ< (s≤s i<n) :: a) y1 fr1)
+        af43 = {!!}
 
 
 -- FLinsert membership