# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1689385000 -32400
# Node ID ab3b3a06d019d2c199e0a5d2048c82a76c7f0c7a
# Parent  9120a5872a5bed80db23d45a22ed85281435496f
...

diff -r 9120a5872a5b -r ab3b3a06d019 automaton-in-agda/src/fin.agda
--- a/automaton-in-agda/src/fin.agda	Tue Jul 11 11:04:00 2023 +0900
+++ b/automaton-in-agda/src/fin.agda	Sat Jul 15 10:36:40 2023 +0900
@@ -142,24 +142,53 @@
 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 = ?
 
+--  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 (suc m) (s≤s n≤m) f with ≤-∨ n≤m
-... | case1 eq = ?
-... | case2 n<m with n<m→fDUP n m ? (f-1 _ _ ? f )
-... | t = ?
+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→¬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 = ?
 
-list2func : (n : ℕ) → (x : List (Fin n)) → suc n < length x → Fin (length x) → Fin n
-list2func n (x ∷ t) n<x zero = x
-list2func n (x ∷ t) (s≤s n<x) (suc fx) = list2func n t ? fx
+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
+     lf00 : (i : ℕ) → (x : List (Fin n)) → i < length x → Fin n
+     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