--- a/FL.agda	Sat Sep 12 22:18:30 2020 +0900
+++ b/FL.agda	Sun Sep 13 03:38:17 2020 +0900
@@ -99,33 +99,9 @@
 ... | case2 x = case2 (subst (λ k →  (zero :: FL0) f< (k :: fmax)) b (f<t x)  )
 
 open import Relation.Binary as B hiding (Decidable; _⇔_)
-
--- f≤-isDecTotalOrder : ∀ {n} → IsDecTotalOrder _≡_ (_f≤_ {n})
--- f≤-isDecTotalOrder = record { isTotalOrder = record { isPartialOrder = record { isPreorder = {!!}
---         ; antisym = {!!}
---         }
---      ; total = {!!}
---      }
---   ; _≟_          = {!!}
---   ; _≤?_         = {!!}
---   }
-
 open import Data.Sum.Base as Sum --  inj₁
-
-total : {n : ℕ } → Total (_f≤_ {n})
-total f0 f0 = inj₁  (case1 refl) 
-total (x :: xt) (y :: yt) with <-fcmp x y
-... | tri< a ¬b ¬c = inj₁ (case2 (f<n a))
-... | tri> ¬a ¬b c = inj₂ (case2 (f<n c))
-... | tri≈ ¬a b ¬c with FLcmp xt yt
-... | tri< a ¬b ¬c₁ = inj₁ (case2 (subst (λ k → (x :: xt ) f< (k :: yt) ) b (f<t a)))
-... | tri≈ ¬a₁ b₁ ¬c₁ = inj₁ (case1 (subst₂ (λ j k → j :: k ≡ y :: yt ) (sym b)  (sym b₁ ) refl  ))
-... | tri> ¬a₁ ¬b c = inj₂ (case2 (subst (λ k → (y :: yt ) f< (k :: xt) ) (sym b) (f<t c)))
-
 open import Relation.Nary using (⌊_⌋)
 open import Data.List.Fresh
-open import Data.List.Fresh.Relation.Unary.All
-open import Data.List.Fresh.Relation.Unary.Any as Any using (Any; here; there)
 
 FList : {n : ℕ } → Set
 FList {n} = List# (FL n) ⌊ _f<?_ ⌋
@@ -140,17 +116,10 @@
    []
 
 open import Data.Product
--- open import Data.Maybe
--- open TotalOrder
-
 open import Relation.Nullary.Decidable hiding (⌊_⌋)
 open import Data.Bool -- hiding (T)
 open import Data.Unit.Base using (⊤ ; tt)
 
--- T : Data.Bool.Bool → Set
--- T true  = ⊤
--- T false = ⊥
-
 --  fresh a []        = ⊤
 --  fresh a (x ∷# xs) = R a x × fresh a xs
 
@@ -167,33 +136,26 @@
        ttf1 t x<a = f<-trans x<a (toWitness t)
 
 FLinsert : {n : ℕ } → FL n → FList {n}  → FList {n} 
+FLfresh : {n : ℕ } → (a x : FL (suc n) ) → (y : FList {suc n} ) → a f< x
+     → fresh (FL (suc n)) ⌊ _f<?_ ⌋ a y → fresh (FL (suc n)) ⌊ _f<?_ ⌋ a (FLinsert x y)
 FLinsert {zero} f0 y = f0 ∷# []
 FLinsert {suc n} x [] = x ∷# []
-FLinsert {suc n} x (cons a y x₁) with total x a
-... | inj₁ (case1 eq) = cons a y x₁
-FLinsert {suc n} x (cons a y x₁) | inj₁ (case2 lt) = cons x ( cons a y x₁) ( Level.lift (fromWitness lt ) , ttf lt y  x₁) 
-... | inj₂ (case1 eq) = cons a y x₁
-FLinsert {suc n} x (cons a [] x₁) | inj₂ (case2 lt) with FLinsert x [] | inspect ( FLinsert x ) []
+FLinsert {suc n} x (cons a y x₁) with FLcmp x a
+... | tri≈ ¬a b ¬c  = cons a y x₁
+... | tri< lt ¬b ¬c  = cons x ( cons a y x₁) ( Level.lift (fromWitness lt ) , ttf lt y  x₁) 
+FLinsert {suc n} x (cons a [] x₁) | tri> ¬a ¬b 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₂) (lift a<a₁ , fr-ay)) | inj₂ (case2 a<x) with total x a₁
-... | inj₁ (case1 refl) =  cons a (cons a₁ y x₂) (Level.lift a<a₁ , fr-ay)
-... | inj₂ (case1 refl) =  cons a (cons a₁ y x₂) (Level.lift a<a₁ , fr-ay)
-... | inj₁ (case2 x<a₁) =  cons a (cons x  (cons a₁ y x₂) ( Level.lift (fromWitness x<a₁) , ttf x<a₁ y x₂))
-                   (  Level.lift (fromWitness a<x) , ttf a<x (cons  a₁ y x₂) ( Level.lift (fromWitness x<a₁) , ttf x<a₁ y x₂))
-... | inj₂ (case2 a₁<x) with FLinsert x y
-... | [] = []
-... | cons a₂ t x₁ = cons a ( cons a₁ ( cons a₂ t x₁ ) ( Level.lift (fromWitness ttf0) , ttf ttf0 t x₁))
-               ( Level.lift a<a₁ ,  Level.lift (fromWitness ttf1) , ttf ttf1 t x₁ ) where
-    ttf0 : a₁ f< a₂
-    ttf0 = ?
-    ttf1 : a  f< a₂
-    ttf1 = f<-trans (toWitness a<a₁) ttf0 
+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 )
 
-
--- a₁<x  : a₁ f< x
--- a<x   : a f< x
--- a<a₁  : T (isYes (a f<? a₁ | FLcmp a a₁))
+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
 
 
 fr6 = FLinsert ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) fr1