Mercurial > hg > Members > kono > Proof > galois

changeset 139:065d8410d346

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 Wed, 09 Sep 2020 11:14:36 +0900
parents 6bb9b3f7b844
children 6006d2beaf24
files FL.agda
diffstat 1 files changed, 7 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/FL.agda	Wed Sep 09 10:53:20 2020 +0900
+++ b/FL.agda	Wed Sep 09 11:14:36 2020 +0900
@@ -172,8 +172,12 @@
        ttf1 : True (a f<? a₁) → x f< a  → x f< a₁
        ttf1 t x<a = f<-trans x<a (toWitness t)
 ... | inj₂ (case1 eq) = cons a y x₁
-... | inj₂ (case2 lt) = cons a (cons x y (ttf2 a lt y x₁)) (Level.lift (fromWitness lt ) , x₁) where
-   ttf2 :  (a : FL (suc n)) → a f< x → (y : FList {suc n}) →  fresh (FL (suc n)) ⌊ _f<?_ ⌋ a y → fresh (FL (suc n)) ⌊ _f<?_ ⌋ x y 
-   ttf2 = {!!}
+... | inj₂ (case2 lt) = cons a ( FLinsert x y ) (ttf2 y) where
+   ttf2 : (y : FList {suc n}) → fresh (FL (suc n)) ⌊ _f<?_ ⌋ a  (FLinsert x y)
+   ttf2 [] with FLinsert x []
+   ... | [] = Level.lift tt
+   ... | cons a t x = {!!} , {!!}
+   ttf2 (cons a [] x) = {!!}
+   ttf2 (cons a (cons a₁ y x₁) x) = {!!}
 
 fr6 = FLinsert ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) fr1