--- a/automaton-in-agda/src/fin.agda	Sat Jul 15 10:36:40 2023 +0900
+++ b/automaton-in-agda/src/fin.agda	Sat Jul 15 18:44:23 2023 +0900
@@ -139,50 +139,54 @@
 --    if the length is longer than n, we can find duplicate element as FDup-in-list 
 --
 
-record fDUP {n m : ℕ} (n<m :  n < m) ( f : Fin m → Fin n )  : Set where
-    field 
-      i j   : Fin m
-      i<j   : toℕ i < toℕ j
-      dup : f i ≡ f j
-
-LEMdup : (n m : ℕ) → (n<m : n < m ) → ( f : Fin m → Fin n ) → fDUP n<m f ∨ (¬ ( fDUP n<m f ))
-LEMdup n (suc m) n<m f = ?
-
-f-1 : (n m : ℕ) → (n<m : n < suc m ) → ( f : Fin (suc m) → Fin n ) → Fin m → Fin n 
-f-1 = ?
+-- record fDUP {n m : ℕ} (n<m :  n < m) ( f : Fin m → Fin n )  : Set where
+--     field 
+--       i j   : Fin m
+--       i<j   : toℕ i < toℕ j
+--       dup : f i ≡ f j
+-- 
+-- n<m→fDUP : (n m : ℕ) → (n<m : n < m ) → ( f : Fin m → Fin n ) → fDUP n<m f
+-- n<m→fDUP n (suc m) n<sm f = ? where
+--       f-1 : Fin m → Fin n
+--       f-1 zero = f zero
+--       f-1 (suc x) = f (fromℕ< (<-trans (fin<n {_} {suc x}) a<sa))
+--       nf00 : fDUP n<sm f ∨ ( (n<m :  n < m ) → fDUP n<m f-1 )
+--       nf00 = ?
 
---  we have natural injection g : Fin n  → Fin m
---  if f is injection, we have a bijection which is a contradiction
---
---  (x : Fin m ) → ∃ f⁻¹ x ∨ ¬ (∃ f⁻¹ x )
---
-n<m→fDUP : (n m : ℕ) → (n<m : n < m ) → ( f : Fin m → Fin n ) → fDUP n<m f
-n<m→fDUP n m n<m f = ? where
-     -- find dup in first n part
-     -- if no dup, we have f⁻¹ , but ¬ (f⁻¹ (f (suc n)) ≡ suc n since n < suc n )
-     record g (y : ℕ ) (y<m : y < m) : Set where
-        field
-          x : Fin n
-          fx=y : f (fromℕ< y<m) ≡ x
-          gi : (i j : Fin m)  →  toℕ i < y → toℕ j < y → f i ≡ f j → i ≡ j 
-     nf00 : (i : ℕ ) (i<n : i < n) → fDUP n<m f ∨ g i (<-trans i<n n<m)
-     nf00 zero i<n = case2 record { x = f (fromℕ< (<-trans i<n n<m)) ; fx=y = refl ; gi = λ i j () }
-     nf00 (suc y) y<n with nf00 y (<-trans a<sa y<n)
-     ... | case1 dup  = case1 dup
-     ... | case2 gi  = ? where
-         fn01 : fDUP n<m f ∨ ( (i : Fin m)  →  toℕ i < y → f i ≡ f (fromℕ< (<-trans y<n n<m))  → i ≡ fromℕ< (<-trans y<n n<m) )
-         fn01 = ? where
-            fn02 : (i : Fin m)  →  toℕ i < y → f i ≡ f (fromℕ< (<-trans y<n n<m))  → ( i ≡ fromℕ< (<-trans y<n n<m))  ∨ fDUP n<m f 
-            fn02 = ?
-
-
-n<m→¬dup : {n m : ℕ} → n < m → ( f : Fin m → Fin n ) 
-   → ¬ ( (i j : Fin m)  → f i ≡ f j → i ≡ j )
-n<m→¬dup {n} {m} n<m f inj = ? where
-     g : Fin n → Fin m 
-     g x = fromℕ< (<-trans (fin<n {n} {x}) n<m )
-     gi : (i j : Fin n)  → g i ≡ g j → i ≡ j 
-     gi = ?
+n<m→fDUP : (n m : ℕ) → (n<m : n < m ) → ( f : Fin m → Fin n ) → ¬ ((i j : Fin m) → f i ≡ f j → i ≡ j ) 
+n<m→fDUP n m n<m f fi = ? where
+     record IsImage (x : ℕ) : Set  where
+       field
+          x<n : x < n
+          y : Fin m
+          x=fy : fromℕ< x<n  ≡ f y
+     data gfImage : (x : ℕ) →  Set where
+          a-g : (x : Fin n) → (¬ib : ¬  IsImage (toℕ x) ) → gfImage (toℕ x)
+          next-gf : {x : Fin n} → (ix : IsImage (toℕ x)) → (gfiy : gfImage (toℕ (IsImage.y ix)) ) → gfImage (toℕ x)
+     nf00 : (x : Fin n) → Dec ( gfImage (toℕ x))
+     nf00 x = ? where
+         nf04 : (i : ℕ) → i < m → Dec ( gfImage (toℕ x))
+         nf04 zero i<m with <-cmp (toℕ (f (fromℕ< i<m))) (toℕ x)
+         ... | tri< a ¬b ¬c = yes (a-g ? ?)
+         ... | tri≈ ¬a b ¬c = no (λ lt → ? )
+         ... | tri> ¬a ¬b c = ?
+         nf04 (suc i) i<m = ?
+     nf01 : (x : Fin m) → Dec ( IsImage (toℕ x))
+     nf01 x = ? where
+         nf04 : (i : ℕ) → i < m → Dec ( IsImage (toℕ x))
+         nf04 zero i<m with <-cmp (toℕ (f (fromℕ< i<m))) (toℕ x)
+         ... | tri< a ¬b ¬c = yes (?)
+         ... | tri≈ ¬a b ¬c = yes record { x<n = ? ; y = ? ; x=fy = ? }
+         ... | tri> ¬a ¬b c = ?
+         nf04 (suc i) i<m = ?
+     nf02 : (x : Fin  n) → ¬ ( gfImage (toℕ x)) → IsImage (toℕ x)
+     nf02 = ?
+     f⁻¹ :  Fin n → Fin m
+     f⁻¹ = ?
+     fiso : (x : Fin n) → f (f⁻¹ x) ≡ x
+     fiso = ?
+     nf03 : n < toℕ ( f ( fromℕ< ? )  )
+     nf03 = ?
 
 list2func : (n : ℕ) → (x : List (Fin n)) → n < length x → Fin (length x) → Fin n
 list2func n x n<l y = lf00 (toℕ y) x fin<n  where
@@ -190,19 +194,6 @@
      lf00 zero (x ∷ t) lt = x
      lf00 (suc i) (x ∷ t) (s≤s lt) = lf00 i t lt
 
--- fin-count : { n : ℕ }  (q : Fin n) (qs : List (Fin n) ) → ℕ
--- fin-count q p[ = 0
--- fin-count q (q0 ∷ qs ) with <-fcmp q q0 
--- ... | tri-e = suc (fin-count q qs)
--- ... | false = fin-count q qs
-
--- fin-not-dup-in-list : { n : ℕ}  (qs : List (Fin n) ) → Set
--- fin-not-dup-in-list {n} qs = (q : Fin n) → fin-count q ≤ 1
-
--- this is far easier
--- fin-not-dup-in-list→len<n : { n : ℕ}  (qs : List (Fin n) ) → ( (q : Fin n) → fin-not-dup-in-list qs q) → length qs ≤ n
--- fin-not-dup-in-list→len<n = ?
-
 fin-phase2 : { n : ℕ }  (q : Fin n) (qs : List (Fin n) ) → Bool  -- find the dup
 fin-phase2 q [] = false
 fin-phase2 q (x ∷ qs) with <-fcmp q x