--- a/automaton-in-agda/src/fin.agda	Wed Dec 29 11:20:49 2021 +0900
+++ b/automaton-in-agda/src/fin.agda	Wed Dec 29 11:50:34 2021 +0900
@@ -251,19 +251,21 @@
      ... | false | record { eq = ne } = fdup+1 qs (FDup-in-list.dup fdup) ne (FDup-in-list.is-dup fdup)  where
            fless : (qs : List (Fin (suc n))) → length qs > suc n  → fin-dup-in-list (fromℕ< a<sa) qs ≡ false → n < length (list-less qs) 
            fless qs lt p = fl-phase1 n qs lt p where
-               fl-phase2 : (n1 : ℕ) (qs : List (Fin (suc n))) → length qs > n1  → fin-phase2 (fromℕ< a<sa) qs ≡ false → suc n1 < length (list-less qs) 
+               fl-phase2 : (n1 : ℕ) (qs : List (Fin (suc n))) → length qs > n1  → fin-phase2 (fromℕ< a<sa) qs ≡ false → n1 < length (list-less qs) 
                fl-phase2 zero (x ∷ qs) (s≤s lt) p with  <-fcmp (fromℕ< a<sa) x
-               ... | t = {!!}
+               ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ x < suc k ) (sym fin<asa) (fin≤n _ )))
+               ... | tri> ¬a ¬b c =  s≤s z≤n 
                fl-phase2 (suc n1) (x ∷ qs) (s≤s lt) p with  <-fcmp (fromℕ< a<sa) x
-               ... | t = {!!}
+               ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ x < suc k ) (sym fin<asa) (fin≤n _ )))
+               ... | tri> ¬a ¬b c = s≤s ( fl-phase2 n1 qs lt p )
                fl-phase1 : (n1 : ℕ) (qs : List (Fin (suc n))) → length qs > suc n1  → fin-phase1 (fromℕ< a<sa) qs ≡ false → n1 < length (list-less qs) 
                fl-phase1 zero (x ∷ qs) (s≤s lt) p  with <-fcmp (fromℕ< a<sa) x
                ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ x < suc k ) (sym fin<asa) (fin≤n _ )))
-               ... | tri≈ ¬a b ¬c = <-trans a<sa (fl-phase2 0 qs lt p) 
+               ... | tri≈ ¬a b ¬c = fl-phase2 0 qs lt p
                ... | tri> ¬a ¬b c = s≤s z≤n
                fl-phase1 (suc n1) (x ∷ qs) (s≤s lt) p with <-fcmp (fromℕ< a<sa) x
                ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ x < suc k ) (sym fin<asa) (fin≤n _ )))
-               ... | tri≈ ¬a b ¬c = fl-phase2 n1 qs (<-trans a<sa lt) p
+               ... | tri≈ ¬a b ¬c = fl-phase2 (suc n1) qs lt p 
                ... | tri> ¬a ¬b c = s≤s ( fl-phase1 n1 qs lt p )
            fdup : FDup-in-list n (list-less qs)
            fdup = fin-dup-in-list>n (list-less qs) (fless qs lt ne)