# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1640629049 -32400
# Node ID ce16779e72a57c60c7ed1a0df7ddaa30e7cfdd97
# Parent  f49c6d768e19feff458487ca8ccdae1205429c8c
fix decrement case

diff -r f49c6d768e19 -r ce16779e72a5 automaton-in-agda/src/fin.agda
--- a/automaton-in-agda/src/fin.agda	Tue Dec 28 02:43:07 2021 +0900
+++ b/automaton-in-agda/src/fin.agda	Tue Dec 28 03:17:29 2021 +0900
@@ -164,17 +164,19 @@
 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 → 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 NatP.<-cmp (toℕ x) n
-          f1-phase2 (x ∷ qs) p | tri< a ¬b ¬c with <-fcmp (fin+1 i) x
+     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 } = f1-phase1 qs p where
+          f1-phase2 : (qs : List (Fin (suc n)) ) → fin-phase2 i (list-less qs) ≡ true → {!!}
+          f1-phase2 (x ∷ qs) p with <-fcmp (fin+1 i) x
+          f1-phase2 (x ∷ qs) p | tri< a ¬b ¬c with NatP.<-cmp (toℕ x) n
           ... | 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 
+          ... | tri≈ ¬a b ¬c₁ = f1-phase2 qs {!!}
+          ... | tri> ¬a ¬b₁ c = {!!} -- ⊥-elim ( nat-<> fin<n c )
+          f1-phase2 (x ∷ qs) p | tri≈ ¬a b ¬c = refl
+          f1-phase2 (x ∷ qs) p | tri> ¬a ¬b c = f1-phase2 qs {!!}
+          f1-phase1 : (qs : List (Fin (suc n)) ) → fin-phase1 i (list-less qs) ≡ true → {!!}
           f1-phase1 [] ()
           f1-phase1 (x ∷ qs) p with <-fcmp (fin+1 i) x
           ... | tri< a ¬b ¬c = f1-phase1 qs {!!}
@@ -215,8 +217,7 @@
      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
+     ... | 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 ⟩