--- a/automaton-in-agda/src/fin.agda	Mon Dec 27 19:48:00 2021 +0900
+++ b/automaton-in-agda/src/fin.agda	Mon Dec 27 21:45:00 2021 +0900
@@ -3,8 +3,9 @@
 module fin where
 
 open import Data.Fin hiding (_<_ ; _≤_ ; _>_ ; _+_ )
-open import Data.Fin.Properties hiding ( <-trans ;  ≤-refl  ) renaming ( <-cmp to <-fcmp )
+open import Data.Fin.Properties hiding (≤-trans ;  <-trans ;  ≤-refl  ) renaming ( <-cmp to <-fcmp )
 open import Data.Nat
+open import Data.Nat.Properties
 open import logic
 open import nat
 open import Relation.Binary.PropositionalEquality
@@ -113,6 +114,14 @@
            ∎  where
                open ≡-Reasoning
 
+x<y→fin-1 : {n : ℕ } → { x y : Fin (suc n)} →  toℕ x < toℕ y  → Fin n
+x<y→fin-1 {n} {x} {y} lt = fromℕ< (≤-trans lt (fin≤n _ ))
+
+x<y→fin-1-eq : {n : ℕ } → { x y : Fin (suc n)} → (lt : toℕ x < toℕ y ) → toℕ x ≡ toℕ (x<y→fin-1 lt )
+x<y→fin-1-eq {n} {x} {y} lt = sym ( begin
+           toℕ (fromℕ< (≤-trans lt (fin≤n y)) ) ≡⟨ toℕ-fromℕ< _ ⟩
+           toℕ x  ∎  ) where open ≡-Reasoning
+
 open import Data.List
 open import Relation.Binary.Definitions
 
@@ -150,15 +159,26 @@
      lseq : list-less qs ≡ ls
      ls>n : m + length ls > n
 
+
 fin-dup-in-list>n : {n : ℕ } → (qs : List (Fin n))  → (len> : length qs > n ) → FDup-in-list n qs
 fin-dup-in-list>n {zero} [] ()
 fin-dup-in-list>n {zero} (() ∷ qs) lt
 fin-dup-in-list>n {suc n} qs lt = fdup-phase0 where
+     open import Level using ( Level )
+     mapleneq : {n : Level} {a b : Set n} { x : List a } {f : a → b} → length (map f x) ≡ length x
+     mapleneq {_} {_} {_} {[]} {f} = refl
+     mapleneq {_} {_} {_} {x ∷ x₁} {f} = cong suc (mapleneq  {_} {_} {_} {x₁})
+     lt-conv : {l : Level} {a : Set l} {m n : ℕ } ( qs : List a ) → m + suc ( length qs ) > n → suc m + length qs > n
+     lt-conv {_} {_} {m} {n} qs lt = begin
+         suc n ≤⟨ lt ⟩
+         m + suc (length qs) ≡⟨ sym (+-assoc m 1 _)  ⟩
+         (m + 1) + length qs ≡⟨ cong (λ k → k + length qs) (+-comm m _ ) ⟩
+         suc m + length qs ∎  where open ≤-Reasoning
      fdup+1 : (qs : List (Fin (suc n))) (i : Fin n) → fin-dup-in-list i (list-less qs) ≡ true → fin-dup-in-list (fin+1 i) qs ≡ true 
      fdup+1 qs i p = f1-phase1 qs p where
           f1-phase2 : (qs : List (Fin (suc n)) ) → fin-phase2 i (list-less qs) ≡ true → fin-phase2 (fin+1 i) qs ≡ true 
           f1-phase2 (x ∷ qs) p with <-fcmp (fin+1 i) x
-          ... | tri< a ¬b ¬c = f1-phase2 qs {!!} -- fin-phase2 i (list-less (x ∷ qs)) ≡ true
+          ... | tri< a ¬b ¬c = f1-phase2 qs {!!} -- fin-phase2 i (list-less (x ∷ qs)) ≡ true → fin-phase2 i (list-less qs) ≡ true
           ... | tri≈ ¬a b ¬c = refl
           ... | tri> ¬a ¬b c = f1-phase2 qs {!!}
           f1-phase1 : (qs : List (Fin (suc n)) ) → fin-phase1 i (list-less qs) ≡ true → fin-phase1 (fin+1 i) qs ≡ true 
@@ -171,21 +191,21 @@
          → ( fin-phase2 (fromℕ< a<sa ) qs ≡ true )  ∨ NList n m qs
      fdup-phase2 [] {m} lt = case2  record { ls = [] ; lseq = refl ; ls>n = lt }
      fdup-phase2 (x ∷ qs) {m} lt with <-fcmp (fromℕ< a<sa) x
-     ... | tri< a ¬b ¬c = {!!}
+     ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ x < suc k) (sym fin<asa) fin<n ))
      fdup-phase2 (x ∷ qs) {m} lt | tri≈ ¬a b ¬c = case1 refl
-     fdup-phase2 (x ∷ qs) {m} lt | tri> ¬a ¬b c with fdup-phase2 qs {suc m} {!!}
+     fdup-phase2 (x ∷ qs) {m} lt | tri> ¬a ¬b c with fdup-phase2 qs {suc m} (lt-conv qs lt)
      ... | case1 p = case1 p
-     ... | case2 nlist = case2 record { ls = {!!} ∷ NList.ls nlist ; lseq = {!!} ; ls>n = {!!} }
+     ... | case2 nlist = case2 record { ls = x<y→fin-1 c ∷ NList.ls nlist ; lseq = {!!} ; ls>n = {!!} }
      fdup-phase1 : (qs : List (Fin (suc n)) ) → {m : ℕ} → m + length qs > n → (fin-phase1  (fromℕ< a<sa) qs ≡ true)  ∨ NList n m qs
      fdup-phase1 [] {m} lt = case2  record { ls = [] ; lseq = refl ; ls>n = lt }
      fdup-phase1 (x ∷ qs) {m} lt with  <-fcmp (fromℕ< a<sa) x
-     fdup-phase1 (x ∷ qs) {m} lt | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a {!!} )
-     fdup-phase1 (x ∷ qs) {m} lt | tri≈ ¬a b ¬c with fdup-phase2 qs {m} {!!}
+     fdup-phase1 (x ∷ qs) {m} lt | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ x < suc k) (sym fin<asa) fin<n ))
+     fdup-phase1 (x ∷ qs) {m} lt | tri≈ ¬a b ¬c with fdup-phase2 qs {m} ?
      ... | case1 p = case1 p
-     ... | case2 nlist = case2 record { ls = {!!} ∷ NList.ls nlist ; lseq = {!!} ; ls>n = {!!} }
+     ... | case2 nlist = case2 record { ls = NList.ls nlist ; lseq = {!!} ; ls>n = NList.ls>n nlist }
      fdup-phase1 (x ∷ qs) {m} lt | tri> ¬a ¬b c with fdup-phase1 qs {m} {!!}
      ... | case1 p = case1 p
-     ... | case2 nlist = case2 record { ls = {!!} ∷ NList.ls nlist ; lseq = {!!} ; ls>n = {!!} }
+     ... | case2 nlist = case2 record { ls = x<y→fin-1 c ∷ NList.ls nlist ; lseq = {!!} ; ls>n = {!!} }
      fdup-phase0 : FDup-in-list (suc n) qs 
      fdup-phase0 with fdup-phase1 qs {0} ( <-trans a<sa lt ) 
      ... | case1 dup   = record { dup =  fromℕ< a<sa ; is-dup = dup }