# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1640626987 -32400
# Node ID f49c6d768e19feff458487ca8ccdae1205429c8c
# Parent  6e85b8b0d8db0c480fd96fb80dcf15e2e125e136
...

diff -r 6e85b8b0d8db -r f49c6d768e19 automaton-in-agda/src/fin.agda
--- a/automaton-in-agda/src/fin.agda	Tue Dec 28 00:28:29 2021 +0900
+++ b/automaton-in-agda/src/fin.agda	Tue Dec 28 02:43:07 2021 +0900
@@ -157,6 +157,7 @@
   field
      ls : List (Fin n)
      lseq : list-less qs ≡ ls
+     ls< : (length ls ≡ length qs) ∨ (suc (length ls) ≡ length qs) 
 
 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} [] ()
@@ -166,10 +167,13 @@
      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 → fin-phase2 i (list-less qs) ≡ true
-          ... | tri≈ ¬a b ¬c = refl
-          ... | tri> ¬a ¬b c = f1-phase2 qs {!!}
+          f1-phase2 (x ∷ qs) p with NatP.<-cmp (toℕ x) n
+          f1-phase2 (x ∷ qs) p | tri< a ¬b ¬c with <-fcmp (fin+1 i) x
+          ... | tri< a₁ ¬b₁ ¬c₁ = f1-phase2 qs {!!}
+          ... | tri≈ ¬a b ¬c₁ = refl
+          ... | tri> ¬a ¬b₁ c = f1-phase2 qs {!!}
+          f1-phase2 (x ∷ qs) p | tri≈ ¬a b ¬c = {!!}
+          f1-phase2 (x ∷ qs) p | tri> ¬a ¬b c = ⊥-elim ( nat-≤> (fin≤n x) c )
           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
@@ -178,13 +182,13 @@
           ... | tri> ¬a ¬b c = f1-phase1 qs {!!}
      fdup-phase2 : (qs : List (Fin (suc n)) ) 
          → ( fin-phase2 (fromℕ< a<sa ) qs ≡ true )  ∨ NList n qs
-     fdup-phase2 []  = case2  record { ls = [] ; lseq = refl }
+     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 } where
+     ... | case2 nlist = case2 record { ls = x<y→fin-1 c ∷ NList.ls nlist ; lseq = fdup01 ; ls< = case1 {!!} } where
            fdup01 : list-less (x ∷ qs) ≡ x<y→fin-1 c ∷ NList.ls nlist
            fdup01 with NatP.<-cmp (toℕ x) n
            ... | tri< a ¬b ¬c = begin
@@ -193,21 +197,37 @@
            ... | 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 )
      fdup-phase1 : (qs : List (Fin (suc n)) ) → (fin-phase1  (fromℕ< a<sa) qs ≡ true)  ∨ NList n qs
-     fdup-phase1 [] = case2  record { ls = [] ; lseq = refl }
+     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 = {!!} } where
+     ... | case2 nlist = case2 record { ls = NList.ls nlist ; lseq = {!!} ; ls< = case2 {!!} } where
            fdup03 : list-less (x ∷ qs) ≡ NList.ls nlist
            fdup03 = {!!}
+           fdup06 : suc (length (NList.ls nlist)) ≡ length (x ∷ qs) 
+           fdup06 = {!!}
      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 = {!!} }
+     ... | 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 = 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
+           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 : FDup-in-list n (list-less qs)
-           fdup = fin-dup-in-list>n (list-less qs) {!!}
+           fdup = fin-dup-in-list>n (list-less qs) ( fdup04 (NList.ls< nlist)  )