--- a/automaton-in-agda/src/fin.agda	Sat Jul 15 18:44:23 2023 +0900
+++ b/automaton-in-agda/src/fin.agda	Sat Jul 15 18:44:51 2023 +0900
@@ -137,56 +137,6 @@
 -- find duplicate element in a List (Fin n)
 --
 --    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
--- 
--- 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 = ?
-
-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