Mercurial > hg > Members > kono > Proof > galois

changeset 149:c5ed0175ecb9

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 Sun, 13 Sep 2020 04:27:17 +0900
parents 1db02863ec58
children 5e5e6cd7da2e
files FL.agda
diffstat 1 files changed, 8 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/FL.agda	Sun Sep 13 03:38:17 2020 +0900
+++ b/FL.agda	Sun Sep 13 04:27:17 2020 +0900
@@ -150,12 +150,14 @@
         cons a (FLinsert x y) (FLfresh a x y a<x yr )
 
 FLfresh {n} a x [] a<x (Level.lift tt) = Level.lift (fromWitness a<x) , Level.lift tt
-FLfresh {n} a x (cons b y br) a<x (lift a<b , a<y) with FLinsert x (cons b y br)
-... | [] = Level.lift tt
-... | cons i t ir with FLcmp i x
-... | tri< i<x ¬b ¬c = {!!} , {!!}
-... | tri≈ ¬a refl ¬c =  Level.lift (fromWitness a<x) , ttf a<x t ir 
-... | tri> ¬a ¬b x<i =  Level.lift (fromWitness  (f<-trans a<x x<i)) , ttf (f<-trans a<x x<i) t ir
+FLfresh {n} a x (cons b [] (Level.lift tt)) a<x (Level.lift a<b , a<y) with FLcmp x b
+... | tri< x<b ¬b ¬c = Level.lift (fromWitness a<x)  , Level.lift a<b , Level.lift tt
+... | tri≈ ¬a refl ¬c = Level.lift (fromWitness a<x) , Level.lift tt
+... | tri> ¬a ¬b b<x = Level.lift a<b  ,  Level.lift (fromWitness  (f<-trans (toWitness a<b) b<x))  , Level.lift tt
+FLfresh {n} a x (cons b (cons a₁ y x₁) br) a<x (Level.lift a<b , a<y) with FLcmp x b
+... | tri< x<b ¬b ¬c = Level.lift (fromWitness a<x) , {!!} , {!!} , ttf {!!} y x₁ 
+... | tri≈ ¬a refl ¬c =  Level.lift (fromWitness a<x)  , {!!} , ttf {!!}  y x₁
+... | tri> ¬a ¬b b<x = {!!} , {!!} 
 
 
 fr6 = FLinsert ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) fr1