Mercurial > hg > Members > kono > Proof > galois

changeset 150:5e5e6cd7da2e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
FLinsert done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 13 Sep 2020 09:33:57 +0900
parents c5ed0175ecb9
children c00eac825964
files FL.agda
diffstat 1 files changed, 9 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
--- a/FL.agda	Sun Sep 13 04:27:17 2020 +0900
+++ b/FL.agda	Sun Sep 13 09:33:57 2020 +0900
@@ -149,15 +149,17 @@
 FLinsert {suc n} x (cons a y yr) |  tri> ¬a ¬b a<x =
         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 [] (Level.lift tt)) a<x (Level.lift a<b , a<y) with FLcmp x b
+FLfresh a x [] a<x (Level.lift tt) = Level.lift (fromWitness a<x) , Level.lift tt
+FLfresh 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 = {!!} , {!!} 
-
+FLfresh a x (cons b y br) 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 , ttf (toWitness a<b) y br
+... | tri≈ ¬a refl ¬c =  Level.lift (fromWitness a<x)  , ttf a<x y br
+FLfresh a x (cons b [] br) a<x (Level.lift a<b , a<y) | tri> ¬a ¬b b<x =
+    Level.lift a<b ,  Level.lift (fromWitness (f<-trans (toWitness a<b) b<x)) , Level.lift tt
+FLfresh a x (cons b (cons a₁ y x₁) br) a<x (Level.lift a<b , a<y) | tri> ¬a ¬b b<x =
+    Level.lift a<b , FLfresh a x  (cons a₁ y x₁) a<x a<y
 
 fr6 = FLinsert ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) fr1