Mercurial > hg > Members > kono > Proof > galois

changeset 146:173b0541c766

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 Sat, 12 Sep 2020 09:26:39 +0900
parents 0d59dcbbd0e1
children 91a858f0b78f
files FL.agda
diffstat 1 files changed, 3 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
--- a/FL.agda	Fri Sep 11 12:26:22 2020 +0900
+++ b/FL.agda	Sat Sep 12 09:26:39 2020 +0900
@@ -184,12 +184,8 @@
      a<a₂ : a f< a₂
      a<a₂ = f<-trans (toWitness a<a₁) lt2
 ... | inj₂ (case1 refl) = cons a (cons a₁ y x₂) (Level.lift a<a₁ , fr-ay)
-... | inj₂ (case2 lt2)  = cons a (cons x (cons a₁ y x₂) ttf2) ( Level.lift (fromWitness lt) , ttf3 ) where
-    x<a₂ : x f< a₂
-    x<a₂ = ?
-    ttf2 : fresh (FL (suc n)) ⌊ _f<?_ ⌋ x (cons a₁ y x₂) --  a f< x ,  a₂ f< a₁, a < a₁ → x < a₁ , x f< a₂
-    ttf2 = {!!} ,  ttf (f<-trans {!!} lt2 ) y x₂
-    ttf3 : fresh (FL (suc n)) ⌊ _f<?_ ⌋ a (cons a₁ y x₂)
-    ttf3 = Level.lift a<a₁ , fr-ay
+... | inj₂ (case2 lt2)  = cons a (cons a₂ t x₁)  ( Level.lift (fromWitness a<a₂) , ttf a<a₂ t  x₁) where
+     a<a₂ : a f< a₂   -- lt : a f< x
+     a<a₂  = {!!}
 
 fr6 = FLinsert ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) fr1