--- a/automaton-in-agda/src/fin.agda	Mon Dec 27 12:45:14 2021 +0900
+++ b/automaton-in-agda/src/fin.agda	Mon Dec 27 19:48:00 2021 +0900
@@ -2,8 +2,8 @@
 
 module fin where
 
-open import Data.Fin hiding (_<_ ; _≤_ ; _>_ )
-open import Data.Fin.Properties hiding ( <-trans )
+open import Data.Fin hiding (_<_ ; _≤_ ; _>_ ; _+_ )
+open import Data.Fin.Properties hiding ( <-trans ;  ≤-refl  ) renaming ( <-cmp to <-fcmp )
 open import Data.Nat
 open import logic
 open import nat
@@ -87,7 +87,6 @@
 lemma12 {suc n} {suc m} (s≤s n<m) (suc f) refl =  cong suc ( lemma12 {n} {m} n<m f refl  ) 
 
 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
-open import Data.Fin.Properties
 
 -- <-irrelevant
 <-nat=irr : {i j n : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → i<n ≅ j<n  
@@ -114,3 +113,85 @@
            ∎  where
                open ≡-Reasoning
 
+open import Data.List
+open import Relation.Binary.Definitions
+
+fin-phase2 : { n : ℕ }  (q : Fin n) (qs : List (Fin n) ) → Bool
+fin-phase2 q [] = false
+fin-phase2 q (x ∷ qs) with <-fcmp q x
+... | tri< a ¬b ¬c = fin-phase2 q qs
+... | tri≈ ¬a b ¬c = true
+... | tri> ¬a ¬b c = fin-phase2 q qs
+fin-phase1 : { n : ℕ }  (q : Fin n) (qs : List (Fin n) ) → Bool
+fin-phase1 q [] = false
+fin-phase1 q (x ∷ qs) with <-fcmp q x
+... | tri< a ¬b ¬c = fin-phase1 q qs
+... | tri≈ ¬a b ¬c = fin-phase2 q qs
+... | tri> ¬a ¬b c = fin-phase1 q qs
+
+fin-dup-in-list : { n : ℕ}  (q : Fin n) (qs : List (Fin n) ) → Bool
+fin-dup-in-list {n} q qs = fin-phase1 q qs
+
+record FDup-in-list (n : ℕ ) (qs : List (Fin n))  : Set where
+   field
+      dup : Fin n
+      is-dup : fin-dup-in-list dup qs ≡ true
+
+list-less : {n : ℕ } → List (Fin (suc n)) → List (Fin n)
+list-less [] = []
+list-less {n} (i ∷ ls) with NatP.<-cmp (toℕ i) n
+... | tri< a ¬b ¬c = fromℕ< a ∷ list-less ls
+... | tri≈ ¬a b ¬c = list-less ls
+... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> (fin≤n i) c )
+
+record NList (n m : ℕ) (qs : List (Fin (suc n))) : Set where
+  field
+     ls : List (Fin n)
+     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
+     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 = 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 
+          f1-phase1 [] ()
+          f1-phase1 (x ∷ qs) p with <-fcmp (fin+1 i) x
+          ... | tri< a ¬b ¬c = f1-phase1 qs {!!}
+          ... | tri≈ ¬a b ¬c = f1-phase2 qs {!!}
+          ... | tri> ¬a ¬b c = f1-phase1 qs {!!}
+     fdup-phase2 : (qs : List (Fin (suc n)) ) → {m : ℕ} → m + length qs > n
+         → ( 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 = {!!}
+     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} {!!}
+     ... | case1 p = case1 p
+     ... | case2 nlist = case2 record { ls = {!!} ∷ 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} {!!}
+     ... | case1 p = case1 p
+     ... | case2 nlist = case2 record { ls = {!!} ∷ NList.ls nlist ; lseq = {!!} ; ls>n = {!!} }
+     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 = {!!} }
+     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 }
+     ... | case2 nlist = record { dup = fin+1 (FDup-in-list.dup fdup)
+              ; is-dup = fdup+1 qs (FDup-in-list.dup fdup) (FDup-in-list.is-dup fdup) } where
+           flt :  length (list-less qs) > n
+           flt = subst ( λ k → length k > n ) (sym (NList.lseq nlist)) ( NList.ls>n nlist )
+           fdup : FDup-in-list n (list-less qs)
+           fdup = fin-dup-in-list>n (list-less qs) flt