# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1640576714 -32400
# Node ID 80276659bb181eaa491356e248e94f5b41b1cd2f
# Parent  8b437dd616dd614aecacef6a68cb730c5e731419
...

diff -r 8b437dd616dd -r 80276659bb18 automaton-in-agda/src/finiteSetUtil.agda
--- a/automaton-in-agda/src/finiteSetUtil.agda	Mon Dec 27 10:29:59 2021 +0900
+++ b/automaton-in-agda/src/finiteSetUtil.agda	Mon Dec 27 12:45:14 2021 +0900
@@ -566,38 +566,40 @@
        field
           ls : List (Fin n)
           ls>n : length ls > n
-    dup-02 : (n : ℕ) → (ls : NList n ) → Dup-in-list (Fin2Finite n) (NList.ls ls) 
-    dup-02 zero ls = {!!}
-    dup-02 (suc n) ls = dup-03 where
+    dup-02 : (n : ℕ) → (ls : NList n ) → length (NList.ls ls) > n → Dup-in-list (Fin2Finite n) (NList.ls ls) 
+    dup-02 zero ls lt = {!!}
+    dup-02 (suc n) ls lt = dup-03 lt where
        n1 : Fin (suc n)
        n1 =  fromℕ< refl-≤
-       d-phase2 : (qs : List (Fin (suc n)) ) → NList n ∨ ( phase2 (Fin2Finite (suc n)) n1 qs ≡ true )
-       d-phase2 [] = {!!}
-       d-phase2 (x ∷ qs) with equal? (Fin2Finite (suc n)) n1 x
+       n<n1 : (i : Fin (suc n)) → equal? (Fin2Finite (suc n)) n1 i ≡ false → n1 f> i
+       n<n1 = {!!}
+       d-phase2 : (qs : List (Fin (suc n)) ) → length qs > suc n  → NList n ∨ ( phase2 (Fin2Finite (suc n)) n1 qs ≡ true )
+       d-phase2 [] lt = case1 record { ls = [] ; ls>n = {!!} }
+       d-phase2 (x ∷ qs) lt with equal? (Fin2Finite (suc n)) n1 x
        ... | true = case2 refl
-       ... | false with d-phase2 qs
+       ... | false with d-phase2 qs {!!} 
        ... | case1 p = case1 record { ls = {!!} ∷ NList.ls p ; ls>n = {!!} }
        ... | case2 eq = case2 eq 
-       d-phase1 : (qs : List (Fin (suc n)) ) → NList n ∨ ( phase1 (Fin2Finite (suc n)) n1 qs ≡ true )
-       d-phase1 [] = {!!}
-       d-phase1 (x ∷ qs) with equal? (Fin2Finite (suc n)) n1 x
-       ... | true with d-phase2 qs
+       d-phase1 : (qs : List (Fin (suc n)) ) → length qs > (suc n)  → NList n ∨ ( phase1 (Fin2Finite (suc n)) n1 qs ≡ true )
+       d-phase1 [] lt = {!!}
+       d-phase1 (x ∷ qs) lt with equal? (Fin2Finite (suc n)) n1 x
+       ... | true with d-phase2 qs {!!}
        ... | case1 p = case1 record { ls = {!!} ∷ NList.ls p ; ls>n = {!!} }
        ... | case2 eq = case2 eq
-       d-phase1 (x ∷ qs)  | false with d-phase1 qs
+       d-phase1 (x ∷ qs) lt | false with d-phase1 qs {!!}
        ... | case1 p = case1 record { ls = {!!} ∷ NList.ls p ; ls>n = {!!} }
        ... | case2 eq = case2 eq
-       dup-03 : Dup-in-list (Fin2Finite (suc n)) (NList.ls ls) 
-       dup-03 with d-phase1 (NList.ls ls) 
+       dup-03 : length (NList.ls ls) > suc n → Dup-in-list (Fin2Finite (suc n)) (NList.ls ls) 
+       dup-03 lt with d-phase1 (NList.ls ls) {!!}
        ... | case1 ls1 = record { dup = fin+1 (Dup-in-list.dup dup-04) ; is-dup = dup-07 } where
            dup-04 : Dup-in-list (Fin2Finite n) (NList.ls ls1) 
-           dup-04 = dup-02 n ls1
+           dup-04 = dup-02 n ls1 {!!}
            dup-07 : dup-in-list (Fin2Finite (suc n)) (fin+1 (Dup-in-list.dup dup-04)) (NList.ls ls) ≡ true
            dup-07 = dup-in-list+iso finq  {!!} {!!} (dup-in-list+1 {!!} {!!} qs {!!})
        ... | case2 dup = record { dup = n1 ; is-dup = dup }
     dup-05 : Q
-    dup-05 = Q←F finq (Dup-in-list.dup (dup-02 (finite finq) record { ls = map (F←Q finq) qs ; ls>n = {!!} } ))
+    dup-05 = Q←F finq (Dup-in-list.dup (dup-02 (finite finq) record { ls = map (F←Q finq) qs ; ls>n = {!!} } {!!} )  )
     dup-06 :  dup-in-list (Fin2Finite (finite finq)) (F←Q finq dup-05) (map (F←Q finq) qs) ≡ true
     dup-06 = subst (λ k → dup-in-list (Fin2Finite (finite finq)) k (map (F←Q finq) qs) ≡ true )
-        {!!} (Dup-in-list.is-dup (dup-02 (finite finq) record { ls = map (F←Q finq) qs ; ls>n = {!!} } ) )
+        {!!} (Dup-in-list.is-dup (dup-02 (finite finq) record { ls = map (F←Q finq) qs ; ls>n = {!!} } {!!} ) )