--- a/automaton-in-agda/src/fin.agda	Tue Dec 28 15:56:48 2021 +0900
+++ b/automaton-in-agda/src/fin.agda	Wed Dec 29 03:50:04 2021 +0900
@@ -171,6 +171,9 @@
            toℕ (fromℕ< (≤-trans c (fin≤n (fromℕ< a<sa))))  ≡⟨ toℕ-fromℕ< _ ⟩
            toℕ x  ∎   where open ≡-Reasoning
 
+---
+---  if List (Fin n) is longer than n, there is at most one duplication
+---
 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
@@ -222,7 +225,9 @@
           ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ x < suc k ) (sym fin<asa) (fin≤n _ )))
           f1-phase1 (x ∷ qs) p (case1 q1) | tri≈ ¬a b ¬c with <-fcmp (fin+1 i) x
           ... | tri< a ¬b ¬c₁ = f1-phase1 qs p (case2 q1)
-          ... | tri≈ ¬a₁ b₁ ¬c₁ = f1-phase2 qs {!!} (case2 q1) -- fin-phase1 i (list-less qs) ≡ true
+          ... | tri≈ ¬a₁ b₁ ¬c₁ = ⊥-elim (fdup-10 b b₁) where
+               fdup-10 : fromℕ< a<sa ≡ x → fin+1 i ≡ x → ⊥
+               fdup-10 eq eq1 = nat-≡< (cong toℕ (trans eq1 (sym eq))) (subst₂ (λ j k → j < k ) (sym fin+1-toℕ) (sym fin<asa) fin<n ) 
           ... | tri> ¬a₁ ¬b c = f1-phase1 qs p (case2 q1)
           f1-phase1 (x ∷ qs) p (case1 q1) | tri> ¬a ¬b c with <-fcmp i (fromℕ< (≤-trans c (fin≤n (fromℕ< a<sa)))) | <-fcmp (fin+1 i) x
           ... | tri< a ¬b₁ ¬c | tri< a₁ ¬b₂ ¬c₁ = f1-phase1 qs p (case1 q1)
@@ -255,25 +260,31 @@
      fdup-phase2 (x ∷ qs)  | tri≈ ¬a b ¬c = case1 refl
      fdup-phase2 (x ∷ qs)  | tri> ¬a ¬b c with fdup-phase2 qs 
      ... | case1 p = case1 p
-     ... | case2 nlist = case2 record { ls = x<y→fin-1 c ∷ NList.ls nlist ; lseq = fdup01 ; ls< = case1 {!!} } where
+     ... | case2 nlist = case2 record { ls = x<y→fin-1 c ∷ NList.ls nlist ; lseq = fdup01 ; ls< = fdup02 {x<y→fin-1 c} } where
            fdup01 : list-less (x ∷ qs) ≡ x<y→fin-1 c ∷ NList.ls nlist
-           fdup01 with <-fcmp (fromℕ< a<sa) x 
-           ... | tri< a ¬b ¬c = {!!} -- begin
-                -- fromℕ< a ∷ list-less qs ≡⟨ cong₂ (λ j k → j ∷ k ) (lemma10 refl) (NList.lseq nlist) ⟩
-                -- fromℕ< (≤-trans c (fin≤n (fromℕ< a<sa))) ∷ NList.ls nlist ∎  where open ≡-Reasoning
-           ... | tri≈ ¬a b ¬c = {!!} -- ⊥-elim ( nat-≡< b (subst (λ k → toℕ x < k ) fin<asa c ))
-           ... | tri> ¬a ¬b c = {!!} -- ⊥-elim ( nat-≤> (fin≤n x) c )
+           fdup01 with <-fcmp (fromℕ< a<sa) x  -- somehow env is lost
+           ... | tri< a ¬b ¬c = ⊥-elim ( ¬a a )
+           ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬b b )
+           ... | tri> ¬a ¬b c₁ = begin
+                x<y→fin-1 c₁ ∷ list-less qs  ≡⟨ cong₂ (λ j k → j ∷ k ) (lemma10 refl) (NList.lseq nlist ) ⟩
+                fromℕ< (≤-trans c (fin≤n (fromℕ< a<sa))) ∷ NList.ls nlist ∎  where open ≡-Reasoning
+           fdup02 : { h : Fin n } → (length (h ∷ NList.ls nlist) ≡ length (x ∷ qs)) ∨ (suc (length (h ∷ NList.ls nlist)) ≡ length (x ∷ qs))
+           fdup02 with NList.ls< nlist
+           ... | case1 x = case1 (cong suc x)
+           ... | case2 x = case2 (cong suc x)
      fdup-phase1 : (qs : List (Fin (suc n)) ) → (fin-phase1  (fromℕ< a<sa) qs ≡ true)  ∨ NList n qs
      fdup-phase1 [] = case2  record { ls = [] ; lseq = refl ; ls< = case1 refl  }
      fdup-phase1 (x ∷ qs) with  <-fcmp (fromℕ< a<sa) x
      fdup-phase1 (x ∷ qs) | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ x < suc k) (sym fin<asa) fin<n ))
      fdup-phase1 (x ∷ qs) | tri≈ ¬a b ¬c with fdup-phase2 qs 
      ... | case1 p = case1 p
-     ... | case2 nlist = case2 record { ls = NList.ls nlist ; lseq = {!!} ; ls< = case2 {!!} } where
+     ... | case2 nlist = case2 record { ls = NList.ls nlist ; lseq = {!!} ; ls< = {!!} } where
            fdup03 : list-less (x ∷ qs) ≡ NList.ls nlist
            fdup03 = {!!}
-           fdup06 : suc (length (NList.ls nlist)) ≡ length (x ∷ qs) 
-           fdup06 = {!!}
+           fdup06 : (length (NList.ls nlist) ≡ length (x ∷ qs)) ∨ (suc (length (NList.ls nlist)) ≡ length (x ∷ qs))
+           fdup06 with NList.ls< nlist
+           ... | case1 x = case1 {!!}
+           ... | case2 x = case2 {!!}
      fdup-phase1 (x ∷ qs) | tri> ¬a ¬b c with fdup-phase1 qs  
      ... | case1 p = case1 p
      ... | case2 nlist = case2 record { ls = x<y→fin-1 c ∷ NList.ls nlist ; lseq = {!!} ; ls< = case1 fdup5 } where