Mercurial > hg > Members > kono > Proof > galois

changeset 140:6006d2beaf24

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 18:45:51 +0900
parents 065d8410d346
children 35c0b6878863
files FL.agda
diffstat 1 files changed, 6 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
--- a/FL.agda	Wed Sep 09 11:14:36 2020 +0900
+++ b/FL.agda	Wed Sep 09 18:45:51 2020 +0900
@@ -172,12 +172,11 @@
        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 ( 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) = {!!}
+FLinsert {suc n} x (cons a [] x₁) | inj₂ (case2 lt) with FLinsert x [] | inspect ( FLinsert x ) []
+... | [] | ()
+... | cons a₁ t x₂ | e = cons a ( x  ∷# []  ) ( Level.lift (fromWitness lt) , Level.lift tt )
+FLinsert {suc n} x (cons a (cons a₁ y x₂) x₁) | inj₂ (case2 lt) with FLinsert x [] | inspect ( FLinsert x ) []
+... | [] | ()
+... | cons a₂ t x₃ | record { eq = eq1 }  = cons a ( cons a₂ t x₃) ( Level.lift (fromWitness {!!}), {!!} )
 
 fr6 = FLinsert ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) fr1