# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1599554029 -32400
# Node ID 1722fd0f1fcf22c4d0267d991cd47da84f4d6921
# Parent  5689c06be30dbce9040621c6e95368fcaad40162
...

diff -r 5689c06be30d -r 1722fd0f1fcf FL.agda
--- a/FL.agda	Tue Sep 08 13:51:10 2020 +0900
+++ b/FL.agda	Tue Sep 08 17:33:49 2020 +0900
@@ -12,6 +12,8 @@
 open import Data.Empty
 open import  Relation.Binary.Core
 open import  Relation.Binary.Definitions
+open import logic
+open import nat
 
 infixr  100 _::_
 
@@ -26,13 +28,6 @@
 FLeq : {n : ℕ } {xn yn : Fin (suc n)} {x : FL n } {y : FL n}  → xn :: x ≡ yn :: y → ( xn ≡ yn )  × (x ≡ y )
 FLeq refl = refl , refl 
 
-nat-<> : { x y : ℕ } → x < y → y < x → ⊥
-nat-<>  (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x
-nat-<≡ : { x : ℕ } → x < x → ⊥
-nat-<≡  (s≤s lt) = nat-<≡ lt
-nat-≡< : { x y : ℕ } → x ≡ y → x < y → ⊥
-nat-≡< refl lt = nat-<≡ lt
-
 f-<> :  {n : ℕ } {x : FL n } {y : FL n}  → x f< y → y f< x → ⊥
 f-<> (f<n x) (f<n x₁) = nat-<> x x₁
 f-<> (f<n x) (f<t lt2) = nat-≡< refl x
@@ -61,8 +56,6 @@
 ... | tri≈ ¬a refl ¬c = no ( ¬a )
 ... | tri> ¬a ¬b c = no ( ¬a )
 
-open import logic
-
 _f≤_ : {n : ℕ } (x : FL n ) (y : FL n)  → Set
 _f≤_ x y = (x ≡ y ) ∨  (x f< y )
 
@@ -70,8 +63,6 @@
 FL0 {zero} = f0
 FL0 {suc n} = zero :: FL0
 
-open import logic
-open import nat
 
 fmax : { n : ℕ } →  FL n
 fmax {zero} = f0
@@ -154,16 +145,20 @@
 -- T true  = ⊤
 -- T false = ⊥
 
+ttf< :  {n : ℕ } → {x a : FL n } → x f< a  → T (isYes (x f<? a))
+ttf< {n} {x} {a} x<a with x f<? a
+... | yes y = subst (λ k → Data.Bool.T k ) refl tt
+... | no nn = ⊥-elim ( nn x<a )
 
 FLcons : {n : ℕ } → FL n → FList {n}  → FList {n} 
 FLcons {zero} f0 y = f0 ∷# []
 FLcons {suc n} x [] = x ∷# []
 FLcons {suc n} x (cons a y x₁) with total x a
 ... | inj₁ (case1 eq) = cons a y x₁
-FLcons {suc n} x (cons a y x₁) | inj₁ (case2 lt) = cons x ( cons a y x₁) ( {!!} , ttf a y  x₁) where
+FLcons {suc n} x (cons a y x₁) | inj₁ (case2 lt) = cons x ( cons a y x₁) ( Level.lift (ttf<  lt ) , ttf a y  x₁) where
    ttf : (a : FL (suc n)) → (y : FList {suc n}) →  fresh (FL (suc n)) ⌊ _f<?_ ⌋  a y  → fresh (FL (suc n)) ⌊ _f<?_ ⌋  x y
    ttf a [] fr = Level.lift tt
-   ttf a (cons a₁ y x) fr = {!!}  , ttf a₁ y x
+   ttf a (cons a₁ y x1) (lift lt1 , _ ) = (Level.lift (ttf< {!!} )) , ttf a₁ y x1
 ... | inj₂ (case1 eq) = cons a y x₁
 ... | inj₂ (case2 lt) = cons a (cons x y {!!}) {!!}