--- a/automaton-in-agda/src/fin.agda	Wed Dec 29 03:50:04 2021 +0900
+++ b/automaton-in-agda/src/fin.agda	Wed Dec 29 11:20:49 2021 +0900
@@ -160,12 +160,6 @@
 ... | tri≈ ¬a b ¬c = list-less ls
 ... | tri> ¬a ¬b c = x<y→fin-1 c ∷ list-less ls
 
-record NList (n : ℕ) (qs : List (Fin (suc n))) : Set where
-  field
-     ls : List (Fin n)
-     lseq : list-less qs ≡ ls
-     ls< : (length ls ≡ length qs) ∨ (suc (length ls) ≡ length qs) 
-
 fin010 : {n m : ℕ } {x : Fin n} (c : suc (toℕ x) ≤ toℕ (fromℕ< {m} a<sa) ) → toℕ (fromℕ< (≤-trans c (fin≤n (fromℕ< a<sa)))) ≡ toℕ x
 fin010 {_} {_} {x} c = begin 
            toℕ (fromℕ< (≤-trans c (fin≤n (fromℕ< a<sa))))  ≡⟨ toℕ-fromℕ< _ ⟩
@@ -179,10 +173,9 @@
 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 )
-     fdup+1 : (qs : List (Fin (suc n))) (i : Fin n) → fin-dup-in-list i (list-less qs) ≡ true → FDup-in-list (suc n) qs
-     fdup+1 qs i p with fin-dup-in-list (fromℕ< a<sa ) qs | inspect (fin-dup-in-list (fromℕ< a<sa )) qs 
-     ... | true  | record {eq = eq } = record { dup = fromℕ< a<sa ; is-dup = eq }
-     ... | false | record {eq = ne } = record { dup = fin+1 i ; is-dup = f1-phase1 qs p (case1 ne) } where
+     fdup+1 : (qs : List (Fin (suc n))) (i : Fin n) →  fin-dup-in-list  (fromℕ< a<sa ) qs ≡ false
+          → fin-dup-in-list i (list-less qs) ≡ true → FDup-in-list (suc n) qs
+     fdup+1 qs i ne p = record { dup = fin+1 i ; is-dup = f1-phase1 qs p (case1 ne) } where
           f1-phase2 : (qs : List (Fin (suc n)) ) → fin-phase2 i (list-less qs) ≡ true
               → (fin-phase1 (fromℕ< a<sa) qs ≡ false ) ∨ (fin-phase2 (fromℕ< a<sa) qs ≡ false)
               → fin-phase2 (fin+1 i) qs ≡ true
@@ -252,59 +245,25 @@
           ... | tri> ¬a₁ ¬b₁ c₁ | tri< a ¬b₂ ¬c = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) (sym fin+1-toℕ) (toℕ-fromℕ< _) c₁ ))
           ... | tri> ¬a₁ ¬b₁ c₁ | tri≈ ¬a₂ b ¬c = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) (sym fin+1-toℕ) (toℕ-fromℕ< _) c₁ ))
           ... | tri> ¬a₁ ¬b₁ c₁ | tri> ¬a₂ ¬b₂ c₂ = f1-phase1 qs p (case2 q1)
-     fdup-phase2 : (qs : List (Fin (suc n)) ) 
-         → ( fin-phase2 (fromℕ< a<sa ) qs ≡ true )  ∨ NList n qs
-     fdup-phase2 []  = case2  record { ls = [] ; lseq = refl ; ls< = case1 refl }
-     fdup-phase2 (x ∷ qs)  with <-fcmp (fromℕ< a<sa) x
-     ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ x < suc k) (sym fin<asa) fin<n ))
-     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< = 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  -- 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< = {!!} } where
-           fdup03 : list-less (x ∷ qs) ≡ NList.ls nlist
-           fdup03 = {!!}
-           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
-           fdup5 : length (x<y→fin-1 c ∷ NList.ls nlist) ≡ length (x ∷ qs)
-           fdup5 = {!!}
      fdup-phase0 : FDup-in-list (suc n) qs 
-     fdup-phase0 with fdup-phase1 qs 
-     ... | case1 dup   = record { dup =  fromℕ< a<sa ; is-dup = dup }
-     ... | case2 nlist = fdup+1 qs (FDup-in-list.dup fdup) (FDup-in-list.is-dup fdup)  where
-           fdup04 : (length (NList.ls nlist) ≡ length qs) ∨ (suc (length (NList.ls nlist)) ≡ length qs)  → length (list-less qs) > n
-           fdup04 (case1 eq)  =  px≤py ( begin 
-              suc (suc n)  ≤⟨ lt ⟩
-              length qs  ≡⟨ sym eq ⟩
-              length (NList.ls nlist)  ≡⟨ cong (λ k → length k) (sym (NList.lseq nlist )) ⟩
-              length (list-less qs) ≤⟨ refl-≤s ⟩
-              suc (length (list-less qs)) ∎  ) where open ≤-Reasoning
-           fdup04 (case2 eq) =  px≤py ( begin
-              suc (suc n)  ≤⟨ lt ⟩
-              length qs  ≡⟨ sym eq ⟩
-              suc (length (NList.ls nlist))  ≡⟨ cong (λ k → suc (length k)) (sym (NList.lseq nlist )) ⟩
-              suc (length (list-less qs)) ∎ )  where open ≤-Reasoning
+     fdup-phase0 with fin-dup-in-list (fromℕ< a<sa) qs | inspect (fin-dup-in-list (fromℕ< a<sa)) qs
+     ... | true  | record { eq = eq } = record { dup = fromℕ< a<sa ; is-dup = eq }
+     ... | 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 zero (x ∷ qs) (s≤s lt) p with  <-fcmp (fromℕ< a<sa) x
+               ... | t = {!!}
+               fl-phase2 (suc n1) (x ∷ qs) (s≤s lt) p with  <-fcmp (fromℕ< a<sa) x
+               ... | t = {!!}
+               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 = 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 = 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) ( fdup04 (NList.ls< nlist)  )
+           fdup = fin-dup-in-list>n (list-less qs) (fless qs lt ne)