# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1688957548 -32400
# Node ID 78e094559ceb1827048a5f7e34497ccef733a612
# Parent  1bf4163de3117fae30d944e38b4e48213fbbc770
...

diff -r 1bf4163de311 -r 78e094559ceb automaton-in-agda/src/bijection.agda
--- a/automaton-in-agda/src/bijection.agda	Sun Jul 09 16:03:43 2023 +0900
+++ b/automaton-in-agda/src/bijection.agda	Mon Jul 10 11:52:28 2023 +0900
@@ -1,5 +1,8 @@
+{-# OPTIONS --allow-unsolved-metas #-}
+
 module bijection where
 
+
 open import Level renaming ( zero to Zero ; suc to Suc )
 open import Data.Nat
 open import Data.Maybe
@@ -7,7 +10,7 @@
 open import Data.Nat.Properties
 open import Relation.Nullary
 open import Data.Empty
-open import Data.Unit hiding ( _≤_ )
+open import Data.Unit using ( tt ; ⊤ )
 open import  Relation.Binary.Core hiding (_⇔_)
 open import  Relation.Binary.Definitions
 open import Relation.Binary.PropositionalEquality
@@ -19,13 +22,13 @@
 --    field
 --        fun←  :  S → R
 --        fun→  :  R → S
---        fiso← : (x : R)  → fun← ( fun→ x )  ≡ x 
---        fiso→ : (x : S ) → fun→ ( fun← x )  ≡ x 
--- 
+--        fiso← : (x : R)  → fun← ( fun→ x )  ≡ x
+--        fiso→ : (x : S ) → fun→ ( fun← x )  ≡ x
+--
 -- injection :  {n m : Level} (R : Set n) (S : Set m) (f : R → S ) → Set (n Level.⊔ m)
 -- injection R S f = (x y : R) → f x ≡ f y → x ≡ y
 
-open Bijection 
+open Bijection
 
 bi-trans : {n m l : Level} (R : Set n) (S : Set m) (T : Set l)  → Bijection R S → Bijection S T → Bijection R T
 bi-trans R S T rs st = record { fun← = λ x → fun← rs ( fun← st x ) ; fun→ = λ x → fun→ st ( fun→ rs x )
@@ -33,27 +36,40 @@
     ; fiso→ = λ x →  trans (cong (λ k → fun→ st k) (fiso→ rs (fun← st x))) ( fiso→ st x) }
 
 bid : {n : Level} (R : Set n)  → Bijection R R
-bid {n} R = record {  fun← = λ x → x ; fun→  = λ x → x ; fiso← = λ _ → refl ;  fiso→ = λ _ → refl } 
+bid {n} R = record {  fun← = λ x → x ; fun→  = λ x → x ; fiso← = λ _ → refl ;  fiso→ = λ _ → refl }
 
 bi-sym : {n m : Level} (R : Set n) (S : Set m) → Bijection R S →  Bijection S R
-bi-sym R S eq = record {  fun← =  fun→ eq ; fun→  = fun← eq  ; fiso← =  fiso→ eq ;  fiso→ =  fiso← eq } 
+bi-sym R S eq = record {  fun← =  fun→ eq ; fun→  = fun← eq  ; fiso← =  fiso→ eq ;  fiso→ =  fiso← eq }
+
+bi-inject← : {n m : Level} {R : Set n} {S : Set m} → (rs : Bijection R S) → {x y : S} → fun← rs x ≡ fun← rs y → x ≡ y
+bi-inject← rs {x} {y} eq = subst₂ (λ j k → j ≡ k ) (fiso→  rs _) (fiso→ rs _) (cong (fun→ rs) eq)
+
+bi-inject→ : {n m : Level} {R : Set n} {S : Set m} → (rs : Bijection R S) → {x y : R} → fun→ rs x ≡ fun→ rs y → x ≡ y
+bi-inject→ rs {x} {y} eq = subst₂ (λ j k → j ≡ k ) (fiso←  rs _) (fiso← rs _) (cong (fun← rs) eq)
 
 open import Relation.Binary.Structures
 
 bijIsEquivalence : {n : Level } → IsEquivalence  (Bijection {n} {n})
 bijIsEquivalence = record { refl = λ {R} → bid R ; sym = λ {R} {S} → bi-sym R S ; trans = λ {R} {S} {T} → bi-trans R S T }
 
---  ¬ A = A → ⊥ 
+--  ¬ A = A → ⊥
 --
 -- famous diagnostic function
 --
 
+--   1 1 0 1 0 ...
+--   0 1 0 1 0 ...
+--   1 0 0 1 0 ...
+--   1 1 1 1 0 ...
+
+--   0 0 1 0 1 ...  diag
+
 diag : {S : Set }  (b : Bijection  ( S → Bool ) S) → S → Bool
 diag b n = not (fun← b n n)
 
 diagonal : { S : Set } → ¬ Bijection  ( S → Bool ) S
 diagonal {S} b = diagn1 (fun→ b (λ n → diag b n) ) refl where
-    diagn1 : (n : S ) → ¬ (fun→ b (λ n → diag b n) ≡ n ) 
+    diagn1 : (n : S ) → ¬ (fun→ b (λ n → diag b n) ≡ n )
     diagn1 n dn = ¬t=f (diag b n ) ( begin
            not (diag b n)
         ≡⟨⟩
@@ -63,17 +79,17 @@
         ≡⟨ cong (λ k → not (fun← b k n) ) dn ⟩
            not (fun← b n n)
         ≡⟨⟩
-           diag b n 
+           diag b n
         ∎ ) where open ≡-Reasoning
 
-b1 : (b : Bijection  ( ℕ → Bool ) ℕ) → ℕ 
+b1 : (b : Bijection  ( ℕ → Bool ) ℕ) → ℕ
 b1 b = fun→ b (diag b)
 
 b-iso : (b : Bijection  ( ℕ → Bool ) ℕ) → fun← b (b1 b) ≡ (diag b)
 b-iso b = fiso← b _
 
 --
--- ℕ <=> ℕ + 1
+-- ℕ <=> ℕ + 1    (infinite hotel)
 --
 to1 : {n : Level} {R : Set n} → Bijection ℕ R → Bijection ℕ (⊤ ∨ R )
 to1 {n} {R} b = record {
@@ -102,16 +118,23 @@
   field
      j k : ℕ
      k1 : nxn→n j k ≡ i
-     nn-unique : {j0 k0 : ℕ } →  nxn→n j0 k0 ≡ i  → ⟪ j , k ⟫ ≡ ⟪ j0 , k0 ⟫ 
+     nn-unique : {j0 k0 : ℕ } →  nxn→n j0 k0 ≡ i  → ⟪ j , k ⟫ ≡ ⟪ j0 , k0 ⟫
 
 i≤0→i≡0 : {i : ℕ } → i ≤ 0 → i ≡ 0
 i≤0→i≡0 {0} z≤n = refl
 
+----
+--    (0, 0) (0, 1)  (0, 2) ....
+--    (1, 0) (1, 1)  (1, 2) ....
+--    (2, 0) (2, 1)  (2, 2) ....
+--      :      :      :
+--      :      :      :
+--
 
 nxn : Bijection ℕ (ℕ ∧ ℕ)
 nxn = record {
      fun← = λ p → nxn→n (proj1 p) (proj2 p)
-   ; fun→ =  n→nxn 
+   ; fun→ =  n→nxn
    ; fiso← = λ i → NN.k1 (nn i)
    ; fiso→ = λ x → nn-id (proj1 x) (proj2 x)
   } where
@@ -120,10 +143,10 @@
      nxn→n zero (suc j) = j + suc (nxn→n zero j)
      nxn→n (suc i) zero = suc i + suc (nxn→n i zero)
      nxn→n (suc i) (suc j) = suc i + suc j + suc (nxn→n i (suc j))
-     nn : ( i  : ℕ) → NN i nxn→n 
+     nn : ( i  : ℕ) → NN i nxn→n
      n→nxn : ℕ → ℕ ∧ ℕ
      n→nxn n = ⟪ NN.j (nn n)  , NN.k (nn n) ⟫
-     k0 : {i : ℕ } → n→nxn i ≡ ⟪ NN.j (nn i) , NN.k (nn i) ⟫ 
+     k0 : {i : ℕ } → n→nxn i ≡ ⟪ NN.j (nn i) , NN.k (nn i) ⟫
      k0 {i} = refl
 
      nxn→n0 : { j k : ℕ } →  nxn→n j k ≡ 0 → ( j ≡ 0 ) ∧ ( k ≡ 0 )
@@ -153,7 +176,7 @@
      nid5 {suc i} {j} {k} = cong suc (nid5 {i} {j} {k} )
 
      -- increment in the same stage
-     nid2 : (i j : ℕ) → suc (nxn→n i (suc j)) ≡ nxn→n (suc i) j 
+     nid2 : (i j : ℕ) → suc (nxn→n i (suc j)) ≡ nxn→n (suc i) j
      nid2 zero zero = refl
      nid2 zero (suc j) = refl
      nid2 (suc i) zero = begin
@@ -178,7 +201,7 @@
              open ≡-Reasoning
 
      -- increment the stage
-     nid00 : (i : ℕ) → suc (nxn→n i 0) ≡ nxn→n 0 (suc i) 
+     nid00 : (i : ℕ) → suc (nxn→n i 0) ≡ nxn→n 0 (suc i)
      nid00 zero = refl
      nid00 (suc i) = begin
         suc (suc (i + suc (nxn→n i 0))) ≡⟨ cong (λ k → suc (suc (i + k ))) (nid00 i) ⟩
@@ -192,10 +215,10 @@
      --
      -- create the invariant NN for all n
      --
-     nn zero = record { j = 0 ; k = 0 ; k1 = refl 
+     nn zero = record { j = 0 ; k = 0 ; k1 = refl
         ;  nn-unique = λ {j0} {k0} eq → cong₂ (λ x y → ⟪ x , y ⟫) (sym (proj1 (nxn→n0 eq))) (sym (proj2 (nxn→n0 {j0} {k0} eq))) }
-     nn (suc i) with NN.k (nn i)  | inspect  NN.k (nn i) 
-     ... | zero | record { eq = eq } = record { k = suc (sum ) ; j = 0 
+     nn (suc i) with NN.k (nn i)  | inspect  NN.k (nn i)
+     ... | zero | record { eq = eq } = record { k = suc (sum ) ; j = 0
          ; k1 = nn02 ; nn-unique = nn04 } where
             ---
             --- increment the stage
@@ -216,28 +239,28 @@
                suc (nxn→n (NN.j (nn i)) (NN.k (nn i))) ≡⟨ cong suc (NN.k1 (nn i) ) ⟩
                suc i ∎  where open ≡-Reasoning
             nn04 : {j0 k0 : ℕ} → nxn→n j0 k0 ≡ suc i → ⟪ 0 , suc (sum ) ⟫ ≡ ⟪ j0 , k0 ⟫
-            nn04 {zero} {suc k0} eq1 = cong (λ k → ⟪ 0 , k ⟫ ) (cong suc (sym nn08)) where -- eq : nxn→n zero (suc k0) ≡ suc i -- 
+            nn04 {zero} {suc k0} eq1 = cong (λ k → ⟪ 0 , k ⟫ ) (cong suc (sym nn08)) where -- eq : nxn→n zero (suc k0) ≡ suc i --
                nn07 : nxn→n k0 0 ≡ i
                nn07 = cong pred ( begin
                   suc ( nxn→n k0 0 ) ≡⟨ nid00 k0 ⟩
                   nxn→n 0 (suc k0 )  ≡⟨ eq1 ⟩
-                  suc i  ∎ )  where open ≡-Reasoning 
-               nn08 : k0 ≡ sum 
+                  suc i  ∎ )  where open ≡-Reasoning
+               nn08 : k0 ≡ sum
                nn08 = begin
                   k0  ≡⟨ cong proj1 (sym (NN.nn-unique (nn i) nn07)) ⟩
                   NN.j (nn i)  ≡⟨ +-comm 0 _ ⟩
                   NN.j (nn i) + 0  ≡⟨ cong (λ k →  NN.j (nn i) + k) (sym eq) ⟩
                   NN.j (nn i) + NN.k (nn i)  ≡⟨ NNnn  ⟩
-                  sum   ∎   where open ≡-Reasoning 
+                  sum   ∎   where open ≡-Reasoning
             nn04 {suc j0} {k0} eq1 = ⊥-elim ( nat-≡< (cong proj2 (nn06 nn05)) (subst (λ k → k < suc k0) (sym eq) (s≤s z≤n))) where
                nn05 : nxn→n j0 (suc k0) ≡ i
                nn05 = begin
-                  nxn→n j0 (suc k0)  ≡⟨ cong pred ( begin 
+                  nxn→n j0 (suc k0)  ≡⟨ cong pred ( begin
                     suc (nxn→n j0 (suc k0))  ≡⟨ nid2 j0 k0 ⟩
                     nxn→n (suc j0) k0  ≡⟨ eq1 ⟩
                     suc i ∎ ) ⟩
-                  i ∎   where open ≡-Reasoning 
-               nn06 : nxn→n j0 (suc k0) ≡ i → ⟪ NN.j (nn i) , NN.k (nn i) ⟫ ≡ ⟪ j0 , suc k0 ⟫ 
+                  i ∎   where open ≡-Reasoning
+               nn06 : nxn→n j0 (suc k0) ≡ i → ⟪ NN.j (nn i) , NN.k (nn i) ⟫ ≡ ⟪ j0 , suc k0 ⟫
                nn06 = NN.nn-unique (nn i)
      ... | suc k  | record {eq = eq} = record { k = k ; j = suc (NN.j (nn i)) ; k1 = nn11 ;  nn-unique = nn13 } where
             ---
@@ -248,23 +271,23 @@
             j = NN.j (nn i)
             NNnn :  NN.j (nn i) + NN.k (nn i) ≡ sum
             NNnn = sym refl
-            nn10 : suc (NN.j (nn i)) + k ≡ sum 
+            nn10 : suc (NN.j (nn i)) + k ≡ sum
             nn10 = begin
                 suc (NN.j (nn i)) + k ≡⟨ cong (λ x → x + k) (+-comm 1 _)  ⟩
                 (NN.j (nn i) + 1) + k ≡⟨  +-assoc (NN.j (nn i)) 1 k ⟩
                 NN.j (nn i) + suc k  ≡⟨ cong (λ k → NN.j (nn i) + k) (sym eq) ⟩
                 NN.j (nn i) + NN.k (nn i) ≡⟨ NNnn  ⟩
-                sum   ∎   where open ≡-Reasoning 
+                sum   ∎   where open ≡-Reasoning
             nn11 :  nxn→n (suc (NN.j (nn i))) k ≡ suc i --  nxn→n ( NN.j (nn i)) (NN.k (nn i) ≡ i
             nn11 = begin
                 nxn→n (suc (NN.j (nn i))) k   ≡⟨ sym (nid2 (NN.j (nn i)) k) ⟩
                 suc (nxn→n (NN.j (nn i)) (suc k)) ≡⟨ cong (λ k →   suc (nxn→n (NN.j (nn i)) k)) (sym eq) ⟩
                 suc (nxn→n ( NN.j (nn i)) (NN.k (nn i)))  ≡⟨ cong suc (NN.k1 (nn i)) ⟩
-                suc i  ∎   where open ≡-Reasoning 
+                suc i  ∎   where open ≡-Reasoning
             nn18 :  zero < NN.k (nn i)
             nn18 = subst (λ k → 0 < k ) ( begin
                     suc k ≡⟨ sym eq ⟩
-                    NN.k (nn i)  ∎  ) (s≤s z≤n )  where open ≡-Reasoning  
+                    NN.k (nn i)  ∎  ) (s≤s z≤n )  where open ≡-Reasoning
             nn13 :  {j0 k0 : ℕ} → nxn→n j0 k0 ≡ suc i → ⟪ suc (NN.j (nn i)) , k ⟫ ≡ ⟪ j0 , k0 ⟫
             nn13 {zero} {suc k0} eq1 = ⊥-elim ( nat-≡< (sym (cong proj2 nn17)) nn18 ) where  -- (nxn→n zero (suc k0)) ≡ suc i
                 nn16 : nxn→n k0 zero ≡ i
@@ -273,7 +296,7 @@
                 nn17 = NN.nn-unique (nn i) nn16
             nn13 {suc j0} {k0} eq1 = begin
                ⟪ suc (NN.j (nn i)) , pred (suc k) ⟫ ≡⟨ cong (λ k →  ⟪ suc (NN.j (nn i)) , pred k ⟫ ) (sym eq) ⟩
-               ⟪ suc (NN.j (nn i)) , pred (NN.k (nn i)) ⟫ ≡⟨ cong (λ k → ⟪ suc (proj1 k) , pred (proj2 k) ⟫) ( begin 
+               ⟪ suc (NN.j (nn i)) , pred (NN.k (nn i)) ⟫ ≡⟨ cong (λ k → ⟪ suc (proj1 k) , pred (proj2 k) ⟫) ( begin
                  ⟪ NN.j (nn i) , NN.k (nn i) ⟫  ≡⟨ nn15 ⟩
                  ⟪ j0 , suc k0 ⟫ ∎ ) ⟩
                ⟪ suc j0 , k0 ⟫ ∎  where -- nxn→n (suc j0) k0 ≡ suc i
@@ -304,24 +327,24 @@
   field
      nlist : List Bool
      isBin : lton nlist ≡ n
-     isUnique :  (x : List Bool) → lton x ≡ n → nlist  ≡ x 
+     isUnique :  (x : List Bool) → lton x ≡ n → nlist  ≡ x
 
 lb+1 : List Bool → List Bool
-lb+1 [] =  false ∷ [] 
-lb+1 (false ∷ t) = true ∷ t 
+lb+1 [] =  false ∷ []
+lb+1 (false ∷ t) = true ∷ t
 lb+1 (true ∷ t) =  false ∷ lb+1 t
 
 lb-1 : List Bool → List Bool
 lb-1 [] =  []
-lb-1 (true ∷ t) = false ∷ t 
+lb-1 (true ∷ t) = false ∷ t
 lb-1 (false ∷ t) with lb-1 t
 ... | [] = true ∷ []
 ... | x ∷ t1 = true ∷ x ∷ t1
 
-LBℕ : Bijection ℕ ( List Bool ) 
+LBℕ : Bijection ℕ ( List Bool )
 LBℕ = record {
-       fun←  = λ x → lton x 
-     ; fun→  = λ n → LB.nlist (lb n) 
+       fun←  = λ x → lton x
+     ; fun→  = λ n → LB.nlist (lb n)
      ; fiso← = λ n → LB.isBin (lb n)
      ; fiso→ = λ x → LB.isUnique (lb (lton x)) x refl
    } where
@@ -332,7 +355,7 @@
      lton : List Bool → ℕ
      lton x  = pred (lton1 x)
 
-     lton1>0 : (x : List Bool ) → 0 < lton1 x 
+     lton1>0 : (x : List Bool ) → 0 < lton1 x
      lton1>0 [] = a<sa
      lton1>0 (true ∷ x₁) = 0<s
      lton1>0 (false ∷ t) = ≤-trans (lton1>0 t) x≤x+y
@@ -361,7 +384,7 @@
      lb=2 : {x y : ℕ } → pred x  < pred y → suc (x + x ) < suc (y + y )
      lb=2 {zero} {suc y} lt = s≤s 0<s
      lb=2 {suc x} {suc y} lt = s≤s (lb=0 {suc x} {suc y} lt)
-     lb=1 : {x y : List Bool} {z : Bool} → lton (z ∷ x) ≡ lton (z ∷ y) → lton x ≡ lton y 
+     lb=1 : {x y : List Bool} {z : Bool} → lton (z ∷ x) ≡ lton (z ∷ y) → lton x ≡ lton y
      lb=1 {x} {y} {true} eq with <-cmp (lton x) (lton y)
      ... | tri< a ¬b ¬c = ⊥-elim (nat-≡< (cong suc eq) (lb=2 {lton1 x} {lton1 y} a))
      ... | tri≈ ¬a b ¬c = b
@@ -388,7 +411,7 @@
             (y + y) ∸ 1  ∎  where open ≤-Reasoning
      ... | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (sym eq) (lb=02 c) ) where
         lb=02 : {x y : ℕ } → x  < y → x + x ∸ 1 < y + y
-        lb=02 {0} {y} lt = ≤-trans lt x≤x+y 
+        lb=02 {0} {y} lt = ≤-trans lt x≤x+y
         lb=02 {suc x} {y} lt = begin
             suc ( suc x + suc x ∸ 1 ) ≡⟨ refl ⟩
             suc x + suc x  ≤⟨ ≤-plus {suc x} (<to≤ lt) ⟩
@@ -408,60 +431,60 @@
      lb=b (x ∷ y) [] eq = ⊥-elim ( nat-≡< (sym eq) (lton-cons>0 {x} {y} ))
      lb=b (true ∷ x) (false ∷ y) eq = ⊥-elim ( lb-tf {x} {y} eq )
      lb=b (false ∷ x) (true ∷ y) eq = ⊥-elim ( lb-tf {y} {x} (sym eq) )
-     lb=b (true ∷ x)  (true ∷ y)  eq = cong (λ k → true ∷ k  ) (lb=b x y (lb=1 {x} {y} {true}  eq)) 
-     lb=b (false ∷ x) (false ∷ y) eq = cong (λ k → false ∷ k ) (lb=b x y (lb=1 {x} {y} {false} eq)) 
+     lb=b (true ∷ x)  (true ∷ y)  eq = cong (λ k → true ∷ k  ) (lb=b x y (lb=1 {x} {y} {true}  eq))
+     lb=b (false ∷ x) (false ∷ y) eq = cong (λ k → false ∷ k ) (lb=b x y (lb=1 {x} {y} {false} eq))
 
      lb : (n : ℕ) → LB n lton
      lb zero = record { nlist = [] ; isBin = refl ; isUnique = lb05 } where
          lb05 : (x : List Bool) → lton x ≡ zero → [] ≡ x
          lb05 x eq = lb=b [] x (sym eq)
-     lb (suc n) with LB.nlist (lb n) | inspect LB.nlist (lb n) 
+     lb (suc n) with LB.nlist (lb n) | inspect LB.nlist (lb n)
      ... | [] | record { eq = eq } = record { nlist = false ∷ [] ; isUnique = lb06 ; isBin = lb10 } where
          open ≡-Reasoning
          lb10 : lton1 (false ∷ []) ∸ 1 ≡ suc n
          lb10 = begin
-           lton (false ∷ []) ≡⟨ refl ⟩ 
-           suc 0  ≡⟨ refl ⟩ 
-           suc (lton [])   ≡⟨ cong (λ k → suc (lton k)) (sym eq) ⟩ 
-           suc (lton (LB.nlist (lb n)))  ≡⟨ cong suc (LB.isBin (lb n) ) ⟩ 
-           suc n ∎    
+           lton (false ∷ []) ≡⟨ refl ⟩
+           suc 0  ≡⟨ refl ⟩
+           suc (lton [])   ≡⟨ cong (λ k → suc (lton k)) (sym eq) ⟩
+           suc (lton (LB.nlist (lb n)))  ≡⟨ cong suc (LB.isBin (lb n) ) ⟩
+           suc n ∎
          lb06 :  (x : List Bool) → pred (lton1 x ) ≡ suc n → false ∷ [] ≡ x
          lb06 x eq1 = lb=b (false ∷ []) x (trans lb10 (sym eq1)) -- lton (false ∷ []) ≡ lton x
      ... | false ∷ t | record { eq = eq } =  record { nlist = true ∷ t ; isBin = lb01 ; isUnique = lb09 } where
         lb01 : lton (true ∷ t) ≡ suc n
         lb01 = begin
-           lton (true ∷ t)  ≡⟨ refl ⟩ 
-           lton1 t + lton1 t   ≡⟨ sym ( sucprd (2lton1>0 t) ) ⟩ 
-           suc (pred (lton1 t + lton1 t ))  ≡⟨ refl ⟩ 
-           suc (lton (false ∷ t))   ≡⟨ cong (λ k → suc (lton k )) (sym eq) ⟩ 
-           suc (lton (LB.nlist (lb n))) ≡⟨  cong suc (LB.isBin (lb n)) ⟩ 
+           lton (true ∷ t)  ≡⟨ refl ⟩
+           lton1 t + lton1 t   ≡⟨ sym ( sucprd (2lton1>0 t) ) ⟩
+           suc (pred (lton1 t + lton1 t ))  ≡⟨ refl ⟩
+           suc (lton (false ∷ t))   ≡⟨ cong (λ k → suc (lton k )) (sym eq) ⟩
+           suc (lton (LB.nlist (lb n))) ≡⟨  cong suc (LB.isBin (lb n)) ⟩
            suc n ∎  where open ≡-Reasoning
         lb09 :  (x : List Bool) → lton1 x ∸ 1 ≡ suc n → true ∷ t ≡ x
         lb09 x eq1 = lb=b (true ∷ t) x (trans lb01 (sym eq1) ) --  lton (true ∷ t) ≡ lton x
      ... | true ∷ t | record { eq = eq } = record { nlist =  lb+1 (true ∷ t) ; isBin = lb02 (true ∷ t) lb03 ; isUnique = lb07 } where
         lb03 : lton (true ∷ t) ≡ n
         lb03 = begin
-           lton (true ∷ t)   ≡⟨ cong (λ k → lton k ) (sym eq ) ⟩ 
-           lton (LB.nlist (lb n)) ≡⟨ LB.isBin (lb n) ⟩ 
+           lton (true ∷ t)   ≡⟨ cong (λ k → lton k ) (sym eq ) ⟩
+           lton (LB.nlist (lb n)) ≡⟨ LB.isBin (lb n) ⟩
            n ∎  where open ≡-Reasoning
 
         add11 : (x1 : ℕ ) → suc x1 + suc x1 ≡ suc (suc  (x1 + x1))
         add11 zero = refl
         add11 (suc x) = cong (λ k → suc (suc k)) (trans (+-comm x _) (cong suc (+-comm _ x)))
 
-        lb04 : (t : List Bool) →  suc (lton1 t) ≡ lton1 (lb+1 t) 
+        lb04 : (t : List Bool) →  suc (lton1 t) ≡ lton1 (lb+1 t)
         lb04 [] = refl
         lb04 (false ∷ t) = refl
         lb04 (true ∷ []) = refl
-        lb04 (true ∷ t0 )  = begin
-           suc (suc (lton1 t0 + lton1 t0)) ≡⟨ sym (add11 (lton1 t0)) ⟩ 
-           suc (lton1 t0) + suc (lton1 t0) ≡⟨ cong (λ k → k + k ) (lb04 t0  ) ⟩ 
+        lb04 (true ∷ t0 @ (_ ∷ _))  = begin
+           suc (suc (lton1 t0 + lton1 t0)) ≡⟨ sym (add11 (lton1 t0)) ⟩
+           suc (lton1 t0) + suc (lton1 t0) ≡⟨ cong (λ k → k + k ) (lb04 t0  ) ⟩
            lton1 (lb+1 t0) + lton1 (lb+1 t0) ∎  where
               open ≡-Reasoning
 
         lb02 : (t : List Bool) → lton t ≡ n → lton (lb+1 t) ≡ suc n
         lb02 [] refl = refl
-        lb02 t eq1 = begin
+        lb02 (t @ (_ ∷ _)) eq1 = begin
             lton (lb+1 t) ≡⟨ refl ⟩
             pred (lton1 (lb+1 t)) ≡⟨ cong pred (sym (lb04 t)) ⟩
             pred (suc (lton1 t))  ≡⟨ sym (sucprd (lton1>0 t)) ⟩
@@ -470,4 +493,525 @@
             suc n ∎  where open ≡-Reasoning
 
         lb07 : (x : List Bool) → pred (lton1 x ) ≡ suc n → lb+1 (true ∷ t) ≡ x
-        lb07 x eq1 = lb=b (lb+1 (true ∷ t)) x (trans ( lb02 (true ∷ t) lb03 ) (sym eq1)) 
+        lb07 x eq1 = lb=b (lb+1 (true ∷ t)) x (trans ( lb02 (true ∷ t) lb03 ) (sym eq1))
+
+-- Bernstein is non constructive, so we cannot use this without some assumption
+--   but in case of ℕ, we can construct it directly.
+
+open import Data.List hiding ([_])
+open import Data.List.Relation.Unary.Any
+
+record InjectiveF (A B : Set) : Set where
+   field
+      f : A → B
+      inject : {x y : A} → f x ≡ f y → x ≡ y
+
+record Is (A C : Set) (f : A → C) (c : C) : Set where
+   field
+      a : A
+      fa=c : f a ≡ c
+
+Countable-Bernstein : (A B C : Set) → Bijection A ℕ → Bijection C ℕ
+     → (fi : InjectiveF A  B ) → (gi : InjectiveF  B C )
+     → (is-A : (c : C ) → Dec (Is A C (λ x → (InjectiveF.f gi (InjectiveF.f fi x))) c )) 
+     → (is-B : (c : C ) → Dec (Is B C (InjectiveF.f gi) c)  )
+     → Bijection B ℕ
+Countable-Bernstein A B C an cn fi gi is-A is-B = record {
+       fun→  = λ x → bton x
+     ; fun←  = λ n → ntob n
+     ; fiso→ = biso
+     ; fiso← = biso1 
+   } where
+    --
+    --     an     f     g     cn
+    --   ℕ ↔   A  →  B  →  C  ↔   ℕ
+    --            B = Image A f ∪ (B \ Image A f )
+    -- 
+    open Bijection
+    f = InjectiveF.f fi
+    g = InjectiveF.f gi
+
+    --
+    -- count number of valid A and B in C
+    --     the count of B is the numner of B in Bijection B ℕ
+    --     if we have a , number a of A is larger than the numner of B C, so we have the inverse
+    --
+
+    count-B : ℕ → ℕ
+    count-B zero with is-B (fun← cn zero)
+    ... | yes isb = 1
+    ... | no nisb = 0
+    count-B (suc n) with is-B (fun← cn (suc n))
+    ... | yes isb = suc (count-B n)
+    ... | no nisb = count-B n
+
+    count-A : ℕ → ℕ
+    count-A zero with is-A (fun← cn zero)
+    ... | yes isb = 1
+    ... | no nisb = 0
+    count-A (suc n) with is-A (fun← cn (suc n))
+    ... | yes isb = suc (count-A n)
+    ... | no nisb = count-A n
+
+    ¬isA∧isB : (y : C ) →  Is A C (λ x → g ( f x)) y → ¬ Is B C g y → ⊥
+    ¬isA∧isB y isa nisb = ⊥-elim ( nisb record { a = f (Is.a isa) ; fa=c = lem } ) where
+         lem : g (f (Is.a isa)) ≡ y
+         lem = begin
+           g (f (Is.a isa))  ≡⟨ Is.fa=c isa  ⟩
+           y ∎ where
+             open ≡-Reasoning
+
+    ca≤cb0 : (n : ℕ) → count-A n ≤ count-B n
+    ca≤cb0 zero with is-A (fun← cn zero) | is-B (fun← cn zero)
+    ... | yes isA | yes isB = ≤-refl
+    ... | yes isA | no nisB = ⊥-elim ( ¬isA∧isB _ isA nisB )
+    ... | no nisA | yes isB = px≤x
+    ... | no nisA | no nisB = ≤-refl
+    ca≤cb0 (suc n) with is-A (fun← cn (suc n)) | is-B (fun← cn (suc n))
+    ... | yes isA | yes isB = s≤s (ca≤cb0 n)
+    ... | yes isA | no nisB = ⊥-elim ( ¬isA∧isB _ isA nisB )
+    ... | no nisA | yes isB = ≤-trans (ca≤cb0 n) px≤x
+    ... | no nisA | no nisB = ca≤cb0 n
+
+    --  (c n)  is
+    --     fun→ c, where c contains all "a" less than n
+    --     (i n : ℕ) → i < suc n → fun→ cn (g (f (fun← an i))) < suc (c n)
+    c : (n : ℕ) → ℕ
+    c zero = fun→ cn (g (f (fun← an zero)))
+    c (suc n) = max (fun→ cn (g (f (fun← an (suc n))))) (c n)
+
+    c< : (i : ℕ) → fun→ cn (g (f (fun← an i))) ≤ c i
+    c< zero = ≤-refl
+    c< (suc i) = x≤max _ _
+
+    c-mono1 : (i : ℕ) → c i ≤ c (suc i)
+    c-mono1 i = y≤max _ _
+    c-mono : (i j : ℕ ) → i ≤ j → c i ≤ c j
+    c-mono i j i≤j with ≤-∨ i≤j
+    ... | case1 refl = ≤-refl
+    c-mono zero (suc j) z≤n | case2 lt = ≤-trans (c-mono zero j z≤n ) (c-mono1 j) 
+    c-mono (suc i) (suc j) (s≤s i≤j) | case2 (s≤s lt) = ≤-trans (c-mono (suc i) j lt ) (c-mono1 j)
+
+    inject-cgf : {i j : ℕ} → fun→ cn (g (f (fun← an i))) ≡ fun→ cn (g (f (fun← an j))) → i ≡ j
+    inject-cgf {i} {j} eq = bi-inject← an (InjectiveF.inject fi (InjectiveF.inject gi ( bi-inject→ cn eq )))
+
+    ani : (i : ℕ) → ℕ
+    ani i = fun→ cn (g (f (fun← an i)))
+
+    ncfi = λ n → (fun→ cn (g (f (fun← an n) )))
+    cfi = λ n → (g (f (fun← an n) ))
+
+    clist : (n : ℕ) → List C
+    clist 0 = fun← cn 0 ∷ []
+    clist (suc n) = fun← cn (suc n) ∷ clist n
+
+    clist-more : {i j : ℕ} → i ≤ j → {c : C} →  Any (_≡_ c) (clist i) →  Any (_≡_ c) (clist j)
+    clist-more {zero} {zero} z≤n a = a
+    clist-more {zero} {suc n} i≤n a = there (clist-more {zero} {n} z≤n a)
+    clist-more {suc i} {suc n} (s≤s le) {c} (there a) = there (clist-more {i} {n} le a)
+    clist-more {suc i} {suc n} (s≤s le) {c} (here px) with ≤-∨ le
+    ... | case1 refl = here px
+    ... | case2 lt = there (clist-more {suc i} {n} lt {c} (here px) )
+
+    clist-any : (n i : ℕ) → i ≤ n → Any (_≡_ (g (f (fun← an i)))) (clist (c n))
+    clist-any n i i≤n = clist-more (c-mono _ _ i≤n) (lem00 (c i) (c< i))   where
+        lem00 : (j : ℕ ) → fun→ cn (g (f (fun← an i))) ≤ j → Any (_≡_ (g (f (fun← an i)))) (clist j)
+        lem00 0 f≤j with  ≤-∨ f≤j
+        ... | case1 eq = here ( trans (sym (fiso← cn _)) ( cong (fun← cn) eq ))
+        ... | case2 le = ⊥-elim (nat-≤> z≤n le )
+        lem00 (suc j) f≤j with  ≤-∨ f≤j
+        ... | case1 eq = here ( trans (sym (fiso← cn _)) ( cong (fun← cn) eq ))
+        ... | case2 (s≤s le) = there (lem00 j le)
+
+    ca-list : List C → ℕ
+    ca-list [] = 0
+    ca-list (h ∷ t) with is-A h
+    ... | yes _ = suc (ca-list t)
+    ... | no _ = ca-list t
+
+    ca-list=count-A : (n : ℕ) → ca-list (clist n) ≡ count-A n
+    ca-list=count-A n = lem02 n (clist n) refl  where
+        lem02 : (n : ℕ) → (cl : List C) → cl ≡ clist n → ca-list cl ≡ count-A n
+        lem02 zero [] ()
+        lem02 zero (h ∷ t) refl with is-A (fun← cn zero)
+        ... | yes _ = refl
+        ... | no _ = refl
+        lem02 (suc n) (h ∷ t) refl with is-A (fun← cn (suc n)) 
+        ... | yes _ = cong suc (lem02 n t refl)
+        ... | no _ = lem02 n t refl
+
+    --  remove (ani i) from clist (c n)
+    --
+    a-list : (i : ℕ) → (cl : List C) → Any (_≡_ (g (f (fun← an i)))) cl → List C
+    a-list i (_ ∷ t) (here px) = t
+    a-list i (h ∷ t) (there a) = h ∷ ( a-list i t a )
+
+    --  count of a in a-list is one step reduced
+    --
+    a-list-ca : (i : ℕ) → (cl : List C) → (a : Any (_≡_ (g (f (fun← an i)))) cl ) 
+        → suc (ca-list (a-list i cl a)) ≡ ca-list cl
+    a-list-ca i cl a = lem03 i cl _ a refl where
+         lem03 : (i : ℕ) → (cl cal : List C) → (a : Any (_≡_ (g (f (fun← an i)))) cl )  → cal ≡  (a-list i cl a) → suc (ca-list cal)  ≡ ca-list cl
+         lem03 i (h ∷ t) (h1 ∷ t1) (here px) refl with is-A h
+         ... | yes _ = refl
+         ... | no nisa = ⊥-elim ( nisa record { a = _ ; fa=c = px } )
+         lem03 i (h ∷ t) (h ∷ t1) (there ah) refl with is-A h
+         ... | yes y = cong suc (lem03 i t t1 ah refl)
+         ... | no _ = lem03 i t t1 ah refl
+         lem03 i (x ∷ []) [] (here px) refl with is-A x
+         ... | yes y = refl
+         ... | no nisa = ⊥-elim ( nisa record { a = _ ; fa=c = px } )
+
+    --  reduced list still have all ani j < i
+    --
+    a-list-any : (i : ℕ) → (cl : List C) → (a : Any (_≡_ (g (f (fun← an i)))) cl ) 
+         → (j : ℕ) → j < i  → Any (_≡_ (g (f (fun← an j)))) cl  → Any (_≡_ (g (f (fun← an j)))) (a-list i cl a) 
+    a-list-any i cl a j j<i b = lem03 i cl _ a refl j j<i b where
+         lem03 : (i : ℕ) → (cl cal : List C) → (a : Any (_≡_ (g (f (fun← an i)))) cl )  
+             → cal ≡  (a-list i cl a) 
+             → (j : ℕ) → j < i  → Any (_≡_ (g (f (fun← an j)))) cl  → Any (_≡_ (g (f (fun← an j)))) cal
+         lem03 i (h ∷ t) cal (here px) eq j j<i (here px₁) = ⊥-elim ( nat-≡< 
+             (  bi-inject← an (InjectiveF.inject fi (InjectiveF.inject gi (trans px₁ (sym px))))) j<i )
+         lem03 i (h ∷ t) cal (here px) eq j j<i (there b) = subst (λ k → Any (_≡_ (g (f (fun← an j)))) k) (sym eq) b
+         lem03 i (h ∷ t) cal (there a) eq j j<i (here px) = subst (λ k → Any (_≡_ (g (f (fun← an j)))) k) (sym eq) (here px)
+         lem03 i (h ∷ t) (h1 ∷ cal) (there a) refl j j<i (there b) = there (lem03 i t cal a refl j j<i b)
+
+    any-cl : (i : ℕ) → (cl : List C) → Set
+    any-cl i cl = (j : ℕ) → j ≤ i → Any (_≡_ (g (f (fun← an j)))) cl
+
+    n<ca-list : (n : ℕ) → n < ca-list (clist (c n))
+    n<ca-list n = lem30 n (clist (c n)) ≤-refl (λ j le  → clist-any n j le ) where
+         --
+         --  we have ANY i on i ≤ n, so we can remove n element from clist (c n)
+         --  induction on n is no good, because (ani (suc n)) may happen in clist (c n)
+         --  so we cannot recurse on n<ca-list itself.
+         --
+
+         del : (i : ℕ) → (cl : List C) → any-cl i cl → List C   -- del 0 contains ani 0
+         del i cl a = a-list i cl (a i ≤-refl)  
+         del-any : (i : ℕ) → (cl : List C) → (a : any-cl (suc i) cl)  → any-cl i (del (suc i) cl a )
+         del-any i cl a j le = lem41 cl (del (suc i) cl a ) (a (suc i) ≤-refl ) (a j (≤-trans le a≤sa) ) refl where
+            lem41 : (cl dl : List C) 
+                 → (ai : Any (_≡_ (g (f (fun← an (suc i))))) cl)
+                 → (aj : Any (_≡_ (g (f (fun← an j)))) cl) 
+                 → dl ≡ a-list (suc i) cl ai →   Any (_≡_ (g (f (fun← an j)))) dl
+            lem41 (h ∷ t) y (here px) (here px₁) eq = ⊥-elim ( nat-≡< 
+                 (  bi-inject← an (InjectiveF.inject fi (InjectiveF.inject gi (trans px₁ (sym px))))) (x≤y→x<sy le) )
+            lem41 (h ∷ t) y (here px) (there b0) eq = subst (λ k →  Any (_≡_ (g (f (fun← an j)))) k) (sym eq) b0
+            lem41 (h ∷ t) y (there a0) (here px) refl = here px
+            lem41 (h ∷ t) (x ∷ y) (there a0) (there b0) refl = there (lem41 t (a-list (suc i) t a0) a0 b0 refl)
+
+         del-ca : (i : ℕ) → (cl : List C) → (a : any-cl i cl  )
+              → suc (ca-list (del i cl a)) ≡ ca-list cl
+         del-ca i cl a = a-list-ca i cl (a i ≤-refl) 
+
+         lem30 : (i : ℕ) → (cl : List C) → (i≤n : i ≤ n) → (a : any-cl i cl) → i < ca-list cl
+         lem30 0 cl i≤n a = begin
+             1 ≤⟨ s≤s z≤n ⟩ 
+             suc (ca-list (del 0 cl a) )  ≡⟨ del-ca 0 cl a ⟩
+             ca-list cl ∎ where
+                open ≤-Reasoning
+         lem30 (suc i) cl i≤n a = begin
+            suc (suc i)   ≤⟨ s≤s (lem30 i _ (≤-trans a≤sa i≤n) (del-any i cl a) ) ⟩ 
+            suc (ca-list (del (suc i) cl a))  ≡⟨ del-ca (suc i) cl a ⟩ 
+            ca-list cl ∎ where
+                open ≤-Reasoning
+
+    record maxAC (n : ℕ) : Set where
+       field
+           ac : ℕ
+           n<ca : n < count-A ac
+
+    lem02 : (n : ℕ) → maxAC n
+    lem02 n = record { ac = c n ; n<ca = subst (λ k → n < k) (ca-list=count-A (c n)) (n<ca-list n ) }
+
+    --
+    -- countB record create ℕ → B and its injection
+    --
+    record CountB (n : ℕ) : Set where
+       field
+          b : B
+          cb : ℕ
+          b=cn : fun← cn cb ≡ g b
+          cb=n : count-B cb ≡ suc n
+          cb-inject : (cb1 : ℕ) → Is B C g (fun← cn cb1) → count-B cb ≡ count-B cb1 → cb ≡ cb1
+
+    count-B-mono : {i j : ℕ} → i ≤ j → count-B i ≤ count-B j
+    count-B-mono {i} {j} i≤j with ≤-∨ i≤j
+    ... | case1 refl = ≤-refl
+    ... | case2 i<j = lem00 _ _ i<j where
+         lem00 : (i j : ℕ) → i < j → count-B i ≤ count-B j
+         lem00 i (suc j) (s≤s i<j) = ≤-trans (count-B-mono i<j) (lem01 j) where
+             lem01 : (j : ℕ) → count-B j ≤ count-B (suc j)
+             lem01 zero with is-B (fun← cn (suc zero))
+             ... | yes isb = refl-≤s
+             ... | no nisb = ≤-refl
+             lem01 (suc n) with is-B (fun← cn (suc (suc n)))
+             ... | yes isb = refl-≤s
+             ... | no nisb = ≤-refl
+
+    lem01 : (n i : ℕ) → suc n ≤ count-B i → CountB n
+    lem01 n i le = lem09 i (count-B i) le refl where
+        -- injection of count-B
+        ---
+        lem06 : (i j : ℕ ) → Is B C g (fun← cn i) → Is B C g (fun← cn j) → count-B i ≡ count-B j → i ≡ j
+        lem06 i j bi bj eq = lem08  where
+            lem20 : (i j : ℕ) → i < j →  Is B C g (fun← cn i) → Is B C g (fun← cn j) → count-B j ≡ count-B i → ⊥
+            lem20 zero (suc j) i<j bi bj le with  is-B (fun← cn 0) | inspect count-B 0 | is-B (fun← cn (suc j)) | inspect count-B (suc j)
+            ... | no nisc  | _ | _ | _ = ⊥-elim (nisc bi)
+            ... |  yes _ | _ | no nisc | _  = ⊥-elim (nisc bj)
+            ... | yes _ | record { eq = eq1 } | yes _ | record { eq = eq2 } = ⊥-elim ( nat-≤> lem25 a<sa) where
+                 lem22 : 1 ≡ count-B 0
+                 lem22 with is-B (fun← cn 0) | inspect count-B 0
+                 ... | yes _ | record { eq = eq1 } = refl
+                 ... | no nisa | _ = ⊥-elim ( nisa bi )
+                 lem24 : count-B j ≡ 0
+                 lem24 = cong pred le
+                 lem25 : 1 ≤ 0
+                 lem25 = begin
+                    1 ≡⟨ lem22 ⟩
+                    count-B 0 ≤⟨ count-B-mono {0} {j} z≤n ⟩
+                    count-B j ≡⟨ lem24 ⟩
+                    0 ∎ where open ≤-Reasoning
+            lem20 (suc i) zero () bi bj le
+            lem20 (suc i) (suc j) (s≤s i<j) bi bj le = ⊥-elim ( nat-≡< lem24 lem21 ) where
+                 --
+                 --                    i  <     suc i  ≤    j
+                 --    cb i <  suc (cb i) < cb (suc i) ≤ cb j
+                 --    suc (cb i) ≡ suc (cb j) → cb i ≡ cb j
+                 lem22 : suc (count-B i) ≡ count-B (suc i)
+                 lem22 with is-B (fun← cn (suc i)) | inspect count-B (suc i)
+                 ... | yes _ | record { eq = eq1 } = refl
+                 ... | no nisa | _ = ⊥-elim ( nisa bi )
+                 lem23 : suc (count-B j) ≡ count-B (suc j)
+                 lem23 with is-B (fun← cn (suc j)) | inspect count-B (suc j)
+                 ... | yes _ | record { eq = eq1 } = refl
+                 ... | no nisa | _ = ⊥-elim ( nisa bj )
+                 lem24 : count-B i ≡ count-B j
+                 lem24 with  is-B (fun← cn (suc i)) | inspect count-B (suc i) | is-B (fun← cn (suc j)) | inspect count-B (suc j)
+                 ... | no nisc  | _ | _ | _ = ⊥-elim (nisc bi)
+                 ... |  yes _ | _ | no nisc | _  = ⊥-elim (nisc bj)
+                 ... | yes _ | record { eq = eq1 } | yes _ | record { eq = eq2 } = sym (cong pred le)
+                 lem21 : suc (count-B i) ≤ count-B j
+                 lem21 = begin
+                     suc (count-B i) ≡⟨ lem22 ⟩
+                     count-B (suc i) ≤⟨ count-B-mono i<j ⟩
+                     count-B j ∎ where
+                        open ≤-Reasoning
+            lem08 : i ≡ j
+            lem08 with <-cmp i j
+            ... | tri< a ¬b ¬c = ⊥-elim ( lem20 i j a bi bj (sym eq) )
+            ... | tri≈ ¬a b ¬c = b
+            ... | tri> ¬a ¬b c₁ = ⊥-elim ( lem20 j i c₁ bj bi eq )
+
+        lem07 : (n i : ℕ) → count-B i ≡ suc n → CountB n
+        lem07 n 0 eq with is-B (fun← cn 0) | inspect count-B 0
+        ... | yes isb | record { eq = eq1 } = record { b = Is.a isb ; cb = 0 ; b=cn = sym (Is.fa=c isb) ; cb=n = trans eq1 eq 
+                ; cb-inject = λ cb1 iscb1 cb1eq → lem12 cb1 iscb1 (subst (λ k → k ≡ count-B cb1) eq1 cb1eq)   } where
+            lem12 : (cb1 : ℕ) →  Is B C g (fun← cn cb1)  → 1 ≡ count-B cb1 → 0 ≡ cb1
+            lem12 cb1 iscb1 cbeq = lem06 0 cb1 isb iscb1 (trans eq1 cbeq) 
+        ... | no nisb | record { eq = eq1 } = ⊥-elim ( nat-≡< eq (s≤s z≤n ) )
+        lem07 n (suc i) eq with is-B (fun← cn (suc i)) | inspect count-B (suc i)
+        ... | yes isb | record { eq = eq1 } = record { b = Is.a isb ; cb = suc i ; b=cn = sym (Is.fa=c isb) ; cb=n = trans eq1 eq
+                 ; cb-inject = λ cb1 iscb1 cb1eq → lem12 cb1 iscb1 (subst (λ k → k ≡ count-B cb1) eq1 cb1eq)   } where
+            lem12 : (cb1 : ℕ) → Is B C g (fun← cn cb1) → suc (count-B i)  ≡ count-B cb1 → suc i ≡ cb1
+            lem12 cb1 iscb1 cbeq = lem06 (suc i) cb1 isb iscb1 (trans eq1 cbeq)
+        ... | no nisb | record { eq = eq1 } = lem07 n i  eq
+
+        -- starting from 0, if count B i ≡ suc n, this is it
+
+        lem09 : (i j : ℕ) → suc n ≤ j → j ≡ count-B i →  CountB n
+        lem09 0 (suc j) (s≤s le) eq with ≤-∨ (s≤s le)
+        ... | case1 eq1 = lem07 n 0 (sym (trans eq1 eq ))
+        ... | case2 (s≤s lt) with is-B (fun← cn 0) | inspect count-B 0
+        ... | yes isb | record { eq = eq1 } = ⊥-elim ( nat-≤> (≤-trans (s≤s lt) (refl-≤≡ eq) ) (s≤s (s≤s z≤n)) )
+        ... | no nisb | record { eq = eq1 } = ⊥-elim (nat-≡< (sym eq) (s≤s z≤n))
+        lem09 (suc i) (suc j) (s≤s le) eq with ≤-∨ (s≤s le)
+        ... | case1 eq1 = lem07 n (suc i) (sym (trans eq1 eq ))
+        ... | case2 (s≤s lt) with is-B (fun← cn (suc i)) | inspect count-B (suc i)
+        ... | yes isb | record { eq = eq1 } = lem09 i j lt (cong pred eq)
+        ... | no nisb | record { eq = eq1 } = lem09 i (suc j) (≤-trans lt a≤sa) eq
+
+    bton : B → ℕ
+    bton b = pred (count-B (fun→ cn (g b)))
+
+    ntob : (n : ℕ) → B
+    ntob n = CountB.b (lem01 n (maxAC.ac (lem02 n)) (≤-trans (maxAC.n<ca (lem02 n)) (ca≤cb0 (maxAC.ac (lem02 n))) ))
+
+    biso : (n : ℕ) → bton (ntob n) ≡ n
+    biso n = begin  
+        bton (ntob n) ≡⟨ refl ⟩
+        pred (count-B (fun→ cn (g (CountB.b CB)))) ≡⟨ sym ( cong (λ k → pred (count-B (fun→ cn k))) ( CountB.b=cn CB)) ⟩
+        pred (count-B (fun→ cn (fun← cn (CountB.cb CB)))) ≡⟨ cong (λ k → pred (count-B k)) (fiso→ cn _) ⟩
+        pred (count-B (CountB.cb CB)) ≡⟨ cong pred (CountB.cb=n CB) ⟩
+        pred (suc n) ≡⟨ refl ⟩
+        n ∎ where
+           open ≡-Reasoning
+           CB  = lem01 n (maxAC.ac (lem02 n)) (≤-trans (maxAC.n<ca (lem02 n)) (ca≤cb0 (maxAC.ac (lem02 n))) )
+
+    --
+    -- uniqueness of ntob is proved by injection
+    --
+    biso1 : (b : B) → ntob (bton b) ≡ b
+    biso1 b with count-B (fun→ cn (g b)) | inspect count-B (fun→ cn (g b)) 
+    ... | zero  | record { eq = eq1 } = ⊥-elim ( nat-≡< (sym lem20) (lem21 _ refl) ) where
+        lem20 : count-B (fun→ cn (InjectiveF.f gi b)) ≡ zero
+        lem20 = eq1
+        lem21 : (i : ℕ) → i ≡ fun→ cn (InjectiveF.f gi b) → 0 < count-B  i
+        lem21 0 eq with is-B (fun← cn 0) | inspect count-B 0
+        ... | yes isb | record { eq = eq1 } = ≤-refl
+        ... | no nisb | record{ eq = eq1 } = ⊥-elim ( nisb record { a = b ; fa=c = trans (sym (fiso← cn _)) (cong (fun← cn) (sym eq)) } )
+        lem21 (suc i) eq with is-B (fun← cn (suc i)) | inspect count-B (suc i)
+        ... | yes isb | record{ eq = eq2 } = s≤s z≤n
+        ... | no nisb | record{ eq = eq2 } = ⊥-elim ( nisb record { a = b ; fa=c = trans (sym (fiso← cn _)) (cong (fun← cn) (sym eq)) } )
+    ... | suc n | record { eq = eq1 } = begin 
+           CountB.b CB  ≡⟨ InjectiveF.inject gi (bi-inject→ cn (begin
+              fun→ cn (g (CountB.b CB)) ≡⟨ cong (fun→ cn) (sym (CountB.b=cn CB)) ⟩
+              fun→ cn (fun← cn (CountB.cb CB)) ≡⟨ fiso→ cn _ ⟩
+              CountB.cb CB  ≡⟨ CountB.cb-inject CB _ record { a = b ; fa=c = sym (fiso← cn _) }  (trans (CountB.cb=n CB) (sym eq1)) ⟩
+              fun→ cn (InjectiveF.f gi b) ∎ ))  ⟩
+           b  ∎  where
+           open ≡-Reasoning
+           CB  = lem01 n (maxAC.ac (lem02 n)) (≤-trans (maxAC.n<ca (lem02 n)) (ca≤cb0 (maxAC.ac (lem02 n))) )
+
+bi-∧ : {A B C D : Set} → Bijection A B → Bijection C D → Bijection (A ∧ C) (B ∧ D)
+bi-∧ {A} {B} {C} {D} ab cd = record {
+       fun←  = λ x → ⟪ fun←  ab (proj1 x) , fun←  cd (proj2 x) ⟫
+     ; fun→  = λ n → ⟪ fun→  ab (proj1 n) , fun→  cd (proj2 n) ⟫
+     ; fiso← = lem0
+     ; fiso→ = lem1
+  } where
+      open Bijection
+      lem0 : (x : A ∧ C) → ⟪ fun← ab (fun→ ab (proj1 x)) , fun← cd (fun→ cd (proj2 x)) ⟫ ≡ x
+      lem0 ⟪ x , y ⟫ = cong₂ ⟪_,_⟫ (fiso← ab x) (fiso← cd y)
+      lem1 : (x : B ∧ D) → ⟪ fun→ ab (fun← ab (proj1 x)) , fun→ cd (fun← cd (proj2 x)) ⟫ ≡ x
+      lem1 ⟪ x , y ⟫ = cong₂ ⟪_,_⟫ (fiso→ ab x) (fiso→ cd y)
+
+
+LM1 : (A : Set ) → Bijection (List A ) ℕ → Bijection (List A ∧ List Bool) ℕ
+LM1 A Ln = bi-trans (List A ∧ List Bool) (ℕ ∧ ℕ)  ℕ (bi-∧ Ln (bi-sym _ _ LBℕ) ) (bi-sym _ _ nxn)
+
+open import Data.List.Properties
+open import Data.Maybe.Properties
+
+---   ℕ ⊆ List A ⊆ List (Maybe A) ⊆ List A ∧ List Bool ⊆ ℕ
+
+LMℕ : (A : Set ) → Bijection (List A) ℕ → Bijection (List (Maybe A)) ℕ
+LMℕ A Ln = Countable-Bernstein (List A) (List (Maybe A)) (List A ∧ List Bool) Ln (LM1 A Ln)  fi gi dec0 dec1 where
+   f : List A → List (Maybe A)
+   f [] = []
+   f (x ∷ t) = just x ∷ f t
+   f-inject : {x y : List A} → f x ≡ f y → x ≡ y
+   f-inject {[]} {[]} refl = refl
+   f-inject {x ∷ xt} {y ∷ yt} eq = cong₂ (λ j k → j ∷ k ) (just-injective (∷-injectiveˡ eq)) (f-inject (∷-injectiveʳ eq) )
+   g : List (Maybe A) → List A ∧ List Bool
+   g [] = ⟪ [] , [] ⟫
+   g (just h ∷ t)  = ⟪ h ∷ proj1 (g t) , true  ∷ proj2 (g t) ⟫
+   g (nothing ∷ t) = ⟪     proj1 (g t) , false ∷ proj2 (g t) ⟫
+   g⁻¹ :  List A ∧ List Bool → List (Maybe A)
+   g⁻¹ ⟪ [] , [] ⟫ = []
+   g⁻¹ ⟪ x ∷ xt , [] ⟫ = just x ∷  g⁻¹ ⟪ xt , [] ⟫
+   g⁻¹ ⟪ [] , true ∷ y ⟫ = []
+   g⁻¹ ⟪ x ∷ xt , true ∷ yt ⟫ = just x ∷ g⁻¹ ⟪ xt , yt ⟫
+   g⁻¹ ⟪ [] , false ∷ y ⟫ = nothing ∷ g⁻¹ ⟪ [] , y ⟫
+   g⁻¹ ⟪ x ∷ x₁ , false ∷ y ⟫ = nothing ∷ g⁻¹ ⟪ x ∷ x₁ , y ⟫
+   g-iso : {x : List (Maybe A)} → g⁻¹ (g x) ≡ x
+   g-iso {[]} = refl
+   g-iso {just x ∷ xt} = cong ( λ k → just x ∷ k) ( g-iso )
+   g-iso {nothing ∷ []} = refl
+   g-iso {nothing ∷ just x ∷ xt} = cong (λ k → nothing ∷ k ) ( g-iso {_} )
+   g-iso {nothing ∷ nothing ∷ xt} with g-iso {nothing ∷ xt}
+   ... | t = trans (lemma01 (proj1 (g xt)) (proj2 (g xt)) ) ( cong (λ k → nothing ∷ k ) t ) where
+         lemma01 : (x : List A) (y : List Bool ) →  g⁻¹ ⟪ x , false ∷ false ∷ y ⟫ ≡ nothing ∷ g⁻¹ ⟪ x , false ∷ y ⟫
+         lemma01 [] y = refl
+         lemma01 (x ∷ x₁) y = refl
+   g-inject : {x y : List (Maybe A)} → g x ≡ g y → x ≡ y
+   g-inject {x} {y} eq = subst₂ (λ j k → j ≡ k ) g-iso g-iso (cong g⁻¹ eq )
+   fi : InjectiveF (List A) (List (Maybe A))
+   fi = record { f = f ; inject = f-inject  }
+   gi : InjectiveF (List (Maybe A)) (List A ∧ List Bool )
+   gi = record { f = g ; inject = g-inject }
+   dec0 : (c : List A ∧ List Bool) → Dec (Is (List A) (List A ∧ List Bool) (λ x → g (f x)) c)
+   dec0 ⟪ [] , [] ⟫ = yes record { a = [] ; fa=c = refl }
+   dec0 ⟪ h ∷ t , [] ⟫ = no ( lem00 ) where
+        lem00 : Is (List A) (List A ∧ List Bool) (λ x → g (f x)) ⟪ h ∷ t , [] ⟫ → ⊥
+        lem00 record { a = [] ; fa=c = () }
+        lem00 record { a = (x ∷ a) ; fa=c = () }
+   dec0 ⟪ [] , true ∷ bt ⟫ = no lem00 where
+        lem00 : Is (List A) (List A ∧ List Bool) (λ x → g (f x)) ⟪ [] , true ∷ bt ⟫ → ⊥
+        lem00 record { a = [] ; fa=c = () }
+   dec0 ⟪ [] , false ∷ bt ⟫ = no lem00 where
+        lem00 : Is (List A) (List A ∧ List Bool) (λ x → g (f x)) ⟪ [] , false ∷ bt ⟫ → ⊥
+        lem00 record { a = [] ; fa=c = () }
+   dec0 ⟪ h ∷ t , (true ∷ bt) ⟫ with dec0 ⟪ t , bt ⟫
+   ... | yes y = yes record { a = h ∷ Is.a y ; fa=c = cong₂ (λ j k → ⟪ h ∷ j , true ∷ k ⟫ ) (cong proj1 (Is.fa=c y)) (cong proj2 (Is.fa=c y))  }
+   ... | no n = no lem00  where
+        lem00 : ¬ Is (List A) (List A ∧ List Bool) (λ x → g (f x)) ⟪ h ∷ t , true ∷ bt ⟫
+        lem00 record { a = (x ∷ a) ; fa=c = refl } = ⊥-elim ( n record { a = a ; fa=c = refl } )
+   dec0 ⟪ (h ∷ t) , (false ∷ bt) ⟫ = no lem00 where
+        lem00 :  ¬ Is (List A) (List A ∧ List Bool) (λ x → g (f x)) ⟪ h ∷ t , false ∷ bt ⟫
+        lem00 record { a = [] ; fa=c = () }
+        lem00 record { a = (x ∷ a) ; fa=c = () }
+   dec1 : (c : List A ∧ List Bool) → Dec (Is (List (Maybe A)) (List A ∧ List Bool) g c)
+   dec1 ⟪ [] , [] ⟫ = yes record { a = [] ; fa=c = refl }
+   dec1 ⟪ h ∷ t , [] ⟫ = no lem00 where
+        lem00 :  ¬ Is (List (Maybe A)) (List A ∧ List Bool) g ⟪ h ∷ t , [] ⟫
+        lem00 record { a = (just x ∷ a) ; fa=c = () }
+        lem00 record { a = (nothing ∷ a) ; fa=c = () }
+   dec1 ⟪ [] , true ∷ bt ⟫ = no lem00 where
+        lem00 : ¬ Is (List (Maybe A)) (List A ∧ List Bool) g ⟪ [] , true ∷ bt ⟫
+        lem00 record { a = (just x ∷ a) ; fa=c = () }
+        lem00 record { a = (nothing ∷ a) ; fa=c = () }
+   dec1 ⟪ [] , false ∷ bt ⟫ with dec1 ⟪ [] , bt ⟫
+   ... | yes record { a = a ; fa=c = fa=c } = yes record { a = nothing ∷ a ; fa=c = cong₂ (λ j k → ⟪ j , false ∷ k ⟫) (cong proj1 fa=c) (cong proj2 fa=c) }
+   ... | no n = no lem00 where
+        lem00 : ¬ Is (List (Maybe A)) (List A ∧ List Bool) g ⟪ [] , false ∷ bt ⟫
+        lem00 record { a = (nothing ∷ a) ; fa=c = eq } = n record { a = a ; fa=c = cong₂ (λ j k → ⟪ j , k ⟫) (cong proj1 eq) lem01 } where
+            lem01 : proj2 (g a) ≡ bt
+            lem01 with cong proj2 eq
+            ... | refl = refl
+   dec1 ⟪ h ∷ t , true ∷ bt ⟫ with dec1 ⟪ t , bt ⟫
+   ... | yes y = yes record { a = just h ∷ Is.a y ; fa=c = cong₂ (λ j k → ⟪ h ∷ j , true ∷ k ⟫ ) (cong proj1 (Is.fa=c y)) (cong proj2 (Is.fa=c y))   }
+   ... | no n = no lem00 where
+        lem00 : ¬ Is (List (Maybe A)) (List A ∧ List Bool) g ⟪ h ∷ t , true ∷ bt ⟫
+        lem00 record { a = (just x ∷ a) ; fa=c = refl } = n record { a = a ; fa=c = refl } 
+   dec1 ⟪ h ∷ t , false ∷ bt ⟫  with dec1 ⟪ h ∷ t , bt ⟫
+   ... | yes record { a = a ; fa=c = fa=c } = yes record { a = nothing ∷ a ; fa=c = cong₂ (λ j k → ⟪ j , false ∷ k ⟫) (cong proj1 fa=c) (cong proj2 fa=c) }
+   ... | no n = no lem00 where
+        lem00 : ¬ Is (List (Maybe A)) (List A ∧ List Bool) g ⟪ h ∷ t , false ∷ bt ⟫
+        lem00 record { a = (nothing ∷ a) ; fa=c = eq } = n record { a = a ; fa=c = cong₂ (λ j k → ⟪ j , k ⟫) (cong proj1 eq) lem01 } where
+            lem01 : proj2 (g a) ≡ bt
+            lem01 with cong proj2 eq
+            ... | refl = refl
+
+--
+--  (     Bool ∷      Bool ∷ [] )    (      Bool ∷      Bool ∷ []   )  (      Bool ∷ [] )
+--        true ∷      true ∷ false ∷        true ∷      true ∷ false ∷        true ∷ []
+
+-- LMℕ A Ln = Countable-Bernstein (List A) (List (Maybe A)) (List A ∧ List Bool) Ln (LM1 A Ln)  fi gi dec0 dec1 where
+--    someday ...
+
+LBBℕ : Bijection (List (List Bool)) ℕ
+LBBℕ = Countable-Bernstein (List Bool ∧ List Bool) (List (List Bool)) (List Bool ∧ List Bool ) (LM1 Bool (bi-sym _ _ LBℕ)) (LM1 Bool (bi-sym _ _ LBℕ))  
+        ? ? ? ? where
+
+    atob : List (List Bool) →  List Bool ∧ List Bool 
+    atob [] = ⟪ [] , [] ⟫
+    atob ( [] ∷  t ) = ⟪ false  ∷ proj1 ( atob t ) , false ∷ proj2 ( atob t ) ⟫
+    atob ( (h ∷ t1) ∷ t ) = ⟪ h ∷ proj1 ( atob t ) , true  ∷ proj2 ( atob t ) ⟫
+
+    btoa : List Bool ∧ List Bool → List (List Bool) 
+    btoa ⟪ [] , _ ⟫ = []
+    btoa ⟪ _ ∷ _  , [] ⟫ = []
+    btoa ⟪ _ ∷ t0 ,  false ∷ t1  ⟫ = [] ∷ btoa ⟪ t0 , t1 ⟫ 
+    btoa ⟪ h ∷ t0 ,  true  ∷ t1  ⟫ with btoa ⟪ t0 , t1 ⟫
+    ... | [] = ( h ∷ [] ) ∷ []
+    ... | x ∷ y = (h ∷ x ) ∷ y
+
+Lℕ=ℕ : Bijection (List ℕ) ℕ
+Lℕ=ℕ = record {
+       fun→  = λ x → ?
+     ; fun←  = λ n → ?
+     ; fiso→ = ?
+     ; fiso← = ?
+     }
diff -r 1bf4163de311 -r 78e094559ceb automaton-in-agda/src/derive.agda
--- a/automaton-in-agda/src/derive.agda	Sun Jul 09 16:03:43 2023 +0900
+++ b/automaton-in-agda/src/derive.agda	Mon Jul 10 11:52:28 2023 +0900
@@ -81,6 +81,7 @@
 --    term generate   x & y   for each * and & only once
 --      rank : Regex → ℕ 
 --   r₀ & r₁ ... r
+--   generated state is a subset of the term set
 
 open import Relation.Binary.Definitions
 
diff -r 1bf4163de311 -r 78e094559ceb automaton-in-agda/src/finiteSetUtil.agda
--- a/automaton-in-agda/src/finiteSetUtil.agda	Sun Jul 09 16:03:43 2023 +0900
+++ b/automaton-in-agda/src/finiteSetUtil.agda	Mon Jul 10 11:52:28 2023 +0900
@@ -13,7 +13,7 @@
 open import nat
 open import finiteSet
 open import fin
-open import Data.Nat.Properties as NatP  hiding ( _≟_ )
+open import Data.Nat.Properties as NP  hiding ( _≟_ )
 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
 
 record Found ( Q : Set ) (p : Q → Bool ) : Set where
@@ -55,14 +55,14 @@
      next-end : {m : ℕ } → ( p : Q → Bool ) → End (suc m) p
               → (m<n : m < finite ) → p (Q←F (fromℕ< m<n )) ≡ false
               → End m p
-     next-end {m} p prev m<n np i m<i with NatP.<-cmp m (toℕ i) 
+     next-end {m} p prev m<n np i m<i with NP.<-cmp m (toℕ i) 
      next-end p prev m<n np i m<i | tri< a ¬b ¬c = prev i a
      next-end p prev m<n np i m<i | tri> ¬a ¬b c = ⊥-elim ( nat-≤> m<i c )
      next-end {m} p prev m<n np i m<i | tri≈ ¬a b ¬c = subst ( λ k → p (Q←F k) ≡ false) (m<n=i i b m<n ) np where
               m<n=i : {n : ℕ } (i : Fin n) {m : ℕ } → m ≡ (toℕ i) → (m<n : m < n )  → fromℕ< m<n ≡ i
               m<n=i i refl m<n = fromℕ<-toℕ i m<n 
      found : { p : Q → Bool } → (q : Q ) → p q ≡ true → exists p ≡ true
-     found {p} q pt = found1 finite  (NatP.≤-refl ) ( first-end p ) where
+     found {p} q pt = found1 finite  (NP.≤-refl ) ( first-end p ) where
          found1 : (m : ℕ ) (m<n : m Data.Nat.≤ finite ) → ((i : Fin finite) → m ≤ toℕ i → p (Q←F i )  ≡ false ) →  exists1 m m<n p ≡ true
          found1 0 m<n end = ⊥-elim ( ¬-bool (subst (λ k → k ≡ false ) (cong (λ k → p k) (finiso→ q) ) (end (F←Q q) z≤n )) pt )
          found1 (suc m)  m<n end with bool-≡-? (p (Q←F (fromℕ< m<n))) true
@@ -75,7 +75,7 @@
                  true
               ∎  where open ≡-Reasoning
      not-found : { p : Q → Bool } → ( (q : Q ) → p q ≡ false ) → exists p ≡ false
-     not-found {p} pn = not-found2 finite NatP.≤-refl where
+     not-found {p} pn = not-found2 finite NP.≤-refl where
          not-found2 : (m : ℕ ) → (m<n : m Data.Nat.≤ finite ) → exists1 m m<n p ≡ false
          not-found2  zero  _ = refl
          not-found2 ( suc m ) m<n with pn (Q←F (fromℕ< {m} {finite} m<n))
@@ -87,7 +87,7 @@
                   false
               ∎  where open ≡-Reasoning
      found← : { p : Q → Bool } → exists p ≡ true → Found Q p
-     found← {p} exst = found2 finite NatP.≤-refl  (first-end p ) where
+     found← {p} exst = found2 finite NP.≤-refl  (first-end p ) where
          found2 : (m : ℕ ) (m<n : m Data.Nat.≤ finite ) → End m p →  Found Q p
          found2 0 m<n end = ⊥-elim ( ¬-bool (not-found (λ q → end (F←Q q)  z≤n ) ) (subst (λ k → exists k ≡ true) (sym lemma) exst ) ) where
              lemma : (λ z → p (Q←F (F←Q z))) ≡ p
@@ -316,17 +316,17 @@
 
 F2L : {Q : Set } {n : ℕ } → (fin : FiniteSet Q ) → n < suc (FiniteSet.finite fin) → ( (q : Q) → toℕ (FiniteSet.F←Q fin q ) < n  → Bool ) → Vec Bool n
 F2L  {Q} {zero} fin _ Q→B = []
-F2L  {Q} {suc n} fin (s≤s n<m) Q→B = Q→B (FiniteSet.Q←F fin (fromℕ< n<m)) lemma6 ∷ F2L {Q} fin (NatP.<-trans n<m a<sa ) qb1 where
+F2L  {Q} {suc n} fin (s≤s n<m) Q→B = Q→B (FiniteSet.Q←F fin (fromℕ< n<m)) lemma6 ∷ F2L {Q} fin (NP.<-trans n<m a<sa ) qb1 where
    lemma6 : toℕ (FiniteSet.F←Q fin (FiniteSet.Q←F fin (fromℕ< n<m))) < suc n
    lemma6 = subst (λ k → toℕ k < suc n ) (sym (FiniteSet.finiso← fin _ )) (subst (λ k → k < suc n) (sym (toℕ-fromℕ< n<m ))  a<sa )
    qb1 : (q : Q) → toℕ (FiniteSet.F←Q fin q) < n → Bool
-   qb1 q q<n = Q→B q (NatP.<-trans q<n a<sa)
+   qb1 q q<n = Q→B q (NP.<-trans q<n a<sa)
 
 List2Func : { Q : Set } → {n : ℕ } → (fin : FiniteSet Q ) → n < suc (FiniteSet.finite fin)  → Vec Bool n →  Q → Bool 
 List2Func {Q} {zero} fin (s≤s z≤n) [] q = false
 List2Func {Q} {suc n} fin (s≤s n<m) (h ∷ t) q with  FiniteSet.F←Q fin q ≟ fromℕ< n<m
 ... | yes _ = h
-... | no _ = List2Func {Q} fin (NatP.<-trans n<m a<sa ) t q
+... | no _ = List2Func {Q} fin (NP.<-trans n<m a<sa ) t q
 
 open import Level renaming ( suc to Suc ; zero to Zero) 
 open import Axiom.Extensionality.Propositional
@@ -344,21 +344,21 @@
     lemma2 with FiniteSet.F←Q fin (FiniteSet.Q←F fin (fromℕ< n<m))  ≟ fromℕ< n<m
     lemma2 | yes p = refl
     lemma2 | no ¬p = ⊥-elim ( ¬p (FiniteSet.finiso← fin _) )
-    lemma4 : (q : Q ) → toℕ (FiniteSet.F←Q fin q ) < n → List2Func fin (s≤s n<m) (h ∷ t) q ≡ List2Func fin (NatP.<-trans n<m a<sa) t q
+    lemma4 : (q : Q ) → toℕ (FiniteSet.F←Q fin q ) < n → List2Func fin (s≤s n<m) (h ∷ t) q ≡ List2Func fin (NP.<-trans n<m a<sa) t q
     lemma4 q _ with FiniteSet.F←Q fin q ≟ fromℕ< n<m 
     lemma4 q lt | yes p = ⊥-elim ( nat-≡< (toℕ-fromℕ< n<m) (lemma5 n lt (cong (λ k → toℕ k) p))) where 
         lemma5 : {j k : ℕ } → ( n : ℕ) → suc j ≤ n → j ≡ k → k < n
         lemma5 {zero} (suc n) (s≤s z≤n) refl = s≤s  z≤n
         lemma5 {suc j} (suc n) (s≤s lt) refl = s≤s (lemma5 {j} n lt refl)
     lemma4 q _ | no ¬p = refl
-    lemma3f :  F2L fin (NatP.<-trans n<m a<sa) (λ q q<n → List2Func fin (s≤s n<m) (h ∷ t) q  ) ≡ t
+    lemma3f :  F2L fin (NP.<-trans n<m a<sa) (λ q q<n → List2Func fin (s≤s n<m) (h ∷ t) q  ) ≡ t
     lemma3f = begin 
-         F2L fin (NatP.<-trans n<m a<sa) (λ q q<n → List2Func fin (s≤s n<m) (h ∷ t) q )
-       ≡⟨ cong (λ k → F2L fin (NatP.<-trans n<m a<sa) ( λ q q<n → k q q<n ))
+         F2L fin (NP.<-trans n<m a<sa) (λ q q<n → List2Func fin (s≤s n<m) (h ∷ t) q )
+       ≡⟨ cong (λ k → F2L fin (NP.<-trans n<m a<sa) ( λ q q<n → k q q<n ))
               (f-extensionality ( λ q →  
               (f-extensionality ( λ q<n →  lemma4 q q<n )))) ⟩
-         F2L fin (NatP.<-trans n<m a<sa) (λ q q<n → List2Func fin (NatP.<-trans n<m a<sa) t q )
-       ≡⟨ f2l n (NatP.<-trans n<m a<sa ) t ⟩
+         F2L fin (NP.<-trans n<m a<sa) (λ q q<n → List2Func fin (NP.<-trans n<m a<sa) t q )
+       ≡⟨ f2l n (NP.<-trans n<m a<sa ) t ⟩
          t
        ∎  where
          open ≡-Reasoning
@@ -375,7 +375,7 @@
      lemma13 : {n nq : ℕ } → (n<m : n < m )  → ¬ ( nq ≡ n ) → nq  ≤ n → nq < n
      lemma13 {0} {0} (s≤s z≤n) nt z≤n = ⊥-elim ( nt refl )
      lemma13 {suc _} {0} (s≤s (s≤s n<m)) nt z≤n = s≤s z≤n
-     lemma13 {suc n} {suc nq} n<m nt (s≤s nq≤n) = s≤s (lemma13 {n} {nq} (NatP.<-trans a<sa n<m ) (λ eq → nt ( cong ( λ k → suc k ) eq )) nq≤n)
+     lemma13 {suc n} {suc nq} n<m nt (s≤s nq≤n) = s≤s (lemma13 {n} {nq} (NP.<-trans a<sa n<m ) (λ eq → nt ( cong ( λ k → suc k ) eq )) nq≤n)
      lemma3f : {a b : ℕ } → (lt : a < b ) → fromℕ< (s≤s lt) ≡ suc (fromℕ< lt)
      lemma3f (s≤s lt) = refl
      lemma12f : {n m : ℕ } → (n<m : n < m ) → (f : Fin m )  → toℕ f ≡ n → f ≡ fromℕ< n<m 
@@ -392,7 +392,7 @@
         f q 
      ∎  where
        open ≡-Reasoning
-  l2f (suc n) (s≤s n<m) (s≤s n<q) | no ¬p = l2f n (NatP.<-trans n<m a<sa) (lemma11f n<m ¬p n<q)
+  l2f (suc n) (s≤s n<m) (s≤s n<q) | no ¬p = l2f n (NP.<-trans n<m a<sa) (lemma11f n<m ¬p n<q)
 
 fin→ : {A : Set} → FiniteSet A → FiniteSet (A → Bool ) 
 fin→ {A}  fin = iso-fin fin2List iso where
@@ -431,29 +431,29 @@
     lemma8f {suc i} {suc i} {suc n} refl {s≤s i<n} {s≤s j<n} = HE.cong (λ k → s≤s k ) ( lemma8f {i} {i}  refl  )
     lemma10f : {n i j  : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n }  → fromℕ< i<n ≡ fromℕ< j<n
     lemma10f  refl  = HE.≅-to-≡ (HE.cong (λ k → fromℕ< k ) (lemma8f refl  ))
-    lemma3f : {a b c : ℕ } → { a<b : a < b } { b<c : b < c } { a<c : a < c } → NatP.<-trans a<b b<c ≡ a<c
+    lemma3f : {a b c : ℕ } → { a<b : a < b } { b<c : b < c } { a<c : a < c } → NP.<-trans a<b b<c ≡ a<c
     lemma3f {a} {b} {c} {a<b} {b<c} {a<c} = HE.≅-to-≡ (lemma8f refl) 
-    lemma11f : {n : ℕ } {x : Fin n } → (n<m : n < m ) → toℕ (fromℕ< (NatP.<-trans (toℕ<n x) n<m)) ≡ toℕ x
+    lemma11f : {n : ℕ } {x : Fin n } → (n<m : n < m ) → toℕ (fromℕ< (NP.<-trans (toℕ<n x) n<m)) ≡ toℕ x
     lemma11f {n} {x} n<m  = begin
-         toℕ (fromℕ< (NatP.<-trans (toℕ<n x) n<m))
+         toℕ (fromℕ< (NP.<-trans (toℕ<n x) n<m))
       ≡⟨ toℕ-fromℕ< _ ⟩
          toℕ x
       ∎  where
           open ≡-Reasoning
     fun← iso (elm1 elm x) = fromℕ< x
-    fun→ iso x = elm1 (FiniteSet.Q←F fa (fromℕ< (NatP.<-trans x<n n<m ))) to<n where
+    fun→ iso x = elm1 (FiniteSet.Q←F fa (fromℕ< (NP.<-trans x<n n<m ))) to<n where
       x<n : toℕ x < n
       x<n = toℕ<n x
-      to<n : toℕ (FiniteSet.F←Q fa (FiniteSet.Q←F fa (fromℕ< (NatP.<-trans x<n n<m)))) < n
-      to<n = subst (λ k → toℕ k < n ) (sym (FiniteSet.finiso← fa _ )) (subst (λ k → k < n ) (sym ( toℕ-fromℕ< (NatP.<-trans x<n n<m) )) x<n )
+      to<n : toℕ (FiniteSet.F←Q fa (FiniteSet.Q←F fa (fromℕ< (NP.<-trans x<n n<m)))) < n
+      to<n = subst (λ k → toℕ k < n ) (sym (FiniteSet.finiso← fa _ )) (subst (λ k → k < n ) (sym ( toℕ-fromℕ< (NP.<-trans x<n n<m) )) x<n )
     fiso← iso x  = lemma2 where
       lemma2 : fromℕ< (subst (λ k → toℕ k < n) (sym
-       (FiniteSet.finiso← fa (fromℕ< (NatP.<-trans (toℕ<n x) n<m)))) (subst (λ k → k < n)
-       (sym (toℕ-fromℕ< (NatP.<-trans (toℕ<n x) n<m))) (toℕ<n x))) ≡ x
+       (FiniteSet.finiso← fa (fromℕ< (NP.<-trans (toℕ<n x) n<m)))) (subst (λ k → k < n)
+       (sym (toℕ-fromℕ< (NP.<-trans (toℕ<n x) n<m))) (toℕ<n x))) ≡ x
       lemma2 = begin
         fromℕ< (subst (λ k → toℕ k < n) (sym
-          (FiniteSet.finiso← fa (fromℕ< (NatP.<-trans (toℕ<n x) n<m)))) (subst (λ k → k < n)
-               (sym (toℕ-fromℕ< (NatP.<-trans (toℕ<n x) n<m))) (toℕ<n x))) 
+          (FiniteSet.finiso← fa (fromℕ< (NP.<-trans (toℕ<n x) n<m)))) (subst (λ k → k < n)
+               (sym (toℕ-fromℕ< (NP.<-trans (toℕ<n x) n<m))) (toℕ<n x))) 
         ≡⟨⟩
            fromℕ< ( subst (λ k → toℕ ( k ) < n ) (sym (FiniteSet.finiso← fa _ )) lemma6 )
         ≡⟨ lemma10 (cong (λ k → toℕ k) (FiniteSet.finiso← fa _ ) ) ⟩
@@ -464,8 +464,8 @@
            x 
         ∎  where
           open ≡-Reasoning
-          lemma6 : toℕ (fromℕ< (NatP.<-trans (toℕ<n x) n<m)) < n
-          lemma6 = subst ( λ k → k < n ) (sym (toℕ-fromℕ< (NatP.<-trans (toℕ<n x) n<m))) (toℕ<n x )
+          lemma6 : toℕ (fromℕ< (NP.<-trans (toℕ<n x) n<m)) < n
+          lemma6 = subst ( λ k → k < n ) (sym (toℕ-fromℕ< (NP.<-trans (toℕ<n x) n<m))) (toℕ<n x )
     fiso→ iso (elm1 elm x) = fin-less-cong fa n<m _ _ lemma (lemma8 (cong (λ k → toℕ (FiniteSet.F←Q fa k) ) lemma ) ) where
       lemma13 : toℕ (fromℕ< x) ≡ toℕ (FiniteSet.F←Q fa elm)
       lemma13 = begin
@@ -473,13 +473,13 @@
          ≡⟨ toℕ-fromℕ< _ ⟩
             toℕ (FiniteSet.F←Q fa elm)
          ∎  where open ≡-Reasoning
-      lemma : FiniteSet.Q←F fa (fromℕ< (NatP.<-trans (toℕ<n (Bijection.fun← iso (elm1 elm x))) n<m)) ≡ elm 
+      lemma : FiniteSet.Q←F fa (fromℕ< (NP.<-trans (toℕ<n (Bijection.fun← iso (elm1 elm x))) n<m)) ≡ elm 
       lemma = begin
-           FiniteSet.Q←F fa (fromℕ< (NatP.<-trans (toℕ<n (Bijection.fun← iso (elm1 elm x))) n<m))
+           FiniteSet.Q←F fa (fromℕ< (NP.<-trans (toℕ<n (Bijection.fun← iso (elm1 elm x))) n<m))
          ≡⟨⟩
-           FiniteSet.Q←F fa (fromℕ< ( NatP.<-trans (toℕ<n ( fromℕ< x ) ) n<m))
+           FiniteSet.Q←F fa (fromℕ< ( NP.<-trans (toℕ<n ( fromℕ< x ) ) n<m))
          ≡⟨ cong (λ k → FiniteSet.Q←F fa k) (lemma10 lemma13 ) ⟩ 
-            FiniteSet.Q←F fa (fromℕ< ( NatP.<-trans x n<m))
+            FiniteSet.Q←F fa (fromℕ< ( NP.<-trans x n<m))
          ≡⟨ cong (λ k → FiniteSet.Q←F fa (fromℕ< k )) (HE.≅-to-≡ (lemma8 refl)) ⟩
            FiniteSet.Q←F fa (fromℕ< ( toℕ<n (FiniteSet.F←Q fa elm)))
          ≡⟨ cong (λ k → FiniteSet.Q←F fa k ) ( fromℕ<-toℕ _ _ ) ⟩
@@ -569,3 +569,92 @@
      dl01 :  fin-dup-in-list (F←Q finq (Q←F finq (FDup-in-list.dup dl))) (map (F←Q finq) qs) ≡ true
      dl01 = subst (λ k →  fin-dup-in-list k (map (F←Q finq) qs) ≡ true )
          (sym (finiso← finq _)) ( FDup-in-list.is-dup dl )
+
+open import bijection using ( InjectiveF ; Is )
+
+inject-fin : {A B : Set}  (fa : FiniteSet A ) 
+   → (fi : InjectiveF B A) 
+   → (is-B : (a : A ) → Dec (Is B A (InjectiveF.f fi) a)  )
+   → FiniteSet B
+inject-fin {A} {B} fa fi is-B = B<n→B (inf00 (finite fa) NP.≤-refl ) where
+   f = InjectiveF.f fi
+   record B<n ( n : ℕ ) : Set where
+       field 
+           b : B  
+           b<n : toℕ (F←Q fa (f b)) < n
+   B<n→B : FiniteSet (B<n (finite fa)) → FiniteSet B
+   B<n→B b<n = record {
+       finite = finite b<n
+       ; Q←F = λ fb → B<n.b (Q←F b<n fb )
+       ; F←Q =  λ b → F←Q b<n record { b = b ; b<n = fin<n }
+       ; finiso→ = ?
+       ; finiso← = ?
+       } 
+   inf00 : (n : ℕ ) → n ≤ finite fa → FiniteSet (B<n n)
+   inf00 zero lt = record {
+       finite = 0
+       ; Q←F = inf03
+       ; F←Q =  inf01
+       ; finiso→ = inf02
+       ; finiso← = λ ()
+       } where
+          inf03 : Fin 0 → B<n zero
+          inf03 ()
+          inf01 : B<n zero → Fin 0
+          inf01 b with B<n.b<n b
+          ... | le = ⊥-elim ( nat-≤> le (s≤s z≤n )) 
+          inf02 : (b : B<n zero) → inf03 (inf01 b) ≡ b
+          inf02 b = ⊥-elim ( nat-≤> (B<n.b<n b) (s≤s z≤n ) )
+   inf00 (suc n) le with is-B ( Q←F fa ( fromℕ< {n} ?  ))
+   ... | yes isb = record {
+        finite = suc (finite bp)
+        ; Q←F =  info05
+        ; F←Q =  ?
+        ; finiso→ = ?
+        ; finiso← = ?
+        } where
+          n≤fa : suc n ≤ finite fa
+          n≤fa = le
+          bp : FiniteSet (B<n n)
+          bp = inf00 n (NP.≤-trans a≤sa le )
+          info05 : Fin (suc (finite bp)) → B<n (suc n)
+          info05 x with <-cmp (toℕ x) (finite bp)
+          ... | tri< a ¬b ¬c = record { b = B<n.b (Q←F bp ? ) ; b<n = ? }
+          ... | tri≈ ¬a b ¬c = ?
+          ... | tri> ¬a ¬b c = ?
+          -- zero = record { b = Is.a isb ; b<n = ? }
+          -- info05 (suc x) = record { b = B<n.b (Q←F bp x) ; b<n = ? }
+          info06 : B<n (suc n) → Fin (suc (finite bp))
+          info06 x with <-cmp (toℕ (F←Q fa (f (B<n.b x)))) n
+          ... | tri< a ¬b ¬c = fromℕ< {toℕ (F←Q fa (f (B<n.b x)))} ?
+          ... | tri≈ ¬a b ¬c = fromℕ< {n} ?
+          ... | tri> ¬a ¬b c = ?
+   ... | no nisb = record {
+        finite = finite bp
+        ; Q←F =  λ x → record { b = B<n.b ( Q←F ? x) ; b<n = ? }
+        ; F←Q =  ?
+        ; finiso→ = ?
+        ; finiso← = ?
+        } where
+          bp : FiniteSet (B<n n)
+          bp = inf00 n (NP.≤-trans a≤sa le )
+   
+-- record {
+-- finite = ? 
+-- ; Q←F = ?
+-- ; F←Q =  ?
+-- ; finiso→ = ?
+-- ; finiso← = ?
+-- } where
+--    f = InjectiveF.f fi
+--    f⁻¹ : (a : A ) → Is B A f a → B
+--    f⁻¹ a isa = Is.a isa
+-- 
+--    record CountB (b : B) : Set where
+--       cb : ℕ
+--       a : A
+--       fb=a : InjectiveF.f fi b ≡ a
+-- 
+
+
+
diff -r 1bf4163de311 -r 78e094559ceb automaton-in-agda/src/nat.agda
--- a/automaton-in-agda/src/nat.agda	Sun Jul 09 16:03:43 2023 +0900
+++ b/automaton-in-agda/src/nat.agda	Mon Jul 10 11:52:28 2023 +0900
@@ -45,12 +45,43 @@
 <-∨ {suc x} {suc y} (s≤s lt) | case1 eq = case1 (cong (λ k → suc k ) eq)
 <-∨ {suc x} {suc y} (s≤s lt) | case2 lt1 = case2 (s≤s lt1)
 
+≤-∨ : { x y : ℕ } → x ≤ y → ( (x ≡ y ) ∨ (x < y) )
+≤-∨ {zero} {zero} z≤n = case1 refl
+≤-∨ {zero} {suc y} z≤n = case2 (s≤s z≤n)
+≤-∨ {suc x} {zero} ()
+≤-∨ {suc x} {suc y} (s≤s lt) with ≤-∨ {x} {y} lt
+≤-∨ {suc x} {suc y} (s≤s lt) | case1 eq = case1 (cong (λ k → suc k ) eq)
+≤-∨ {suc x} {suc y} (s≤s lt) | case2 lt1 = case2 (s≤s lt1)
+
 max : (x y : ℕ) → ℕ
 max zero zero = zero
 max zero (suc x) = (suc x)
 max (suc x) zero = (suc x)
 max (suc x) (suc y) = suc ( max x y )
 
+x≤max : (x y : ℕ) → x ≤ max x y
+x≤max zero zero = ≤-refl
+x≤max zero (suc x) = z≤n
+x≤max (suc x) zero = ≤-refl
+x≤max (suc x) (suc y) = s≤s( x≤max x y )
+
+y≤max : (x y : ℕ) → y ≤ max x y
+y≤max zero zero = ≤-refl
+y≤max zero (suc x) = ≤-refl
+y≤max (suc x) zero = z≤n
+y≤max (suc x) (suc y) = s≤s( y≤max x y )
+
+x≤y→max=y : (x y : ℕ) → x ≤ y → max x y ≡ y
+x≤y→max=y zero zero x≤y = refl
+x≤y→max=y zero (suc y) x≤y = refl
+x≤y→max=y (suc x) (suc y) (s≤s x≤y) = cong suc (x≤y→max=y x y x≤y )
+
+y≤x→max=x : (x y : ℕ) → y ≤ x → max x y ≡ x
+y≤x→max=x zero zero y≤x = refl
+y≤x→max=x zero (suc y) ()
+y≤x→max=x (suc x) zero lt = refl
+y≤x→max=x (suc x) (suc y) (s≤s y≤x) = cong suc (y≤x→max=x x y y≤x )
+
 -- _*_ : ℕ → ℕ → ℕ
 -- _*_ zero _ = zero
 -- _*_ (suc n) m = m + ( n * m )
@@ -201,14 +232,25 @@
 <to≤ {zero} {suc y} (s≤s z≤n) = z≤n
 <to≤ {suc x} {suc y} (s≤s lt) = s≤s (<to≤ {x} {y}  lt)
 
+<∨≤ : ( x y : ℕ ) →  (x < y ) ∨ (y ≤ x) 
+<∨≤ x y with <-cmp x y
+... | tri< a ¬b ¬c = case1 a
+... | tri≈ ¬a refl ¬c = case2 ≤-refl
+... | tri> ¬a ¬b c = case2 (<to≤ c)
+
 refl-≤s : {x : ℕ } → x ≤ suc x
 refl-≤s {zero} = z≤n
 refl-≤s {suc x} = s≤s (refl-≤s {x})
 
+a≤sa = refl-≤s
+
 refl-≤ : {x : ℕ } → x ≤ x
 refl-≤ {zero} = z≤n
 refl-≤ {suc x} = s≤s (refl-≤ {x})
 
+refl-≤≡ : {x y : ℕ } → x ≡ y → x ≤ y
+refl-≤≡ refl = refl-≤ 
+
 x<y→≤ : {x y : ℕ } → x < y →  x ≤ suc y
 x<y→≤ {zero} {.(suc _)} (s≤s z≤n) = z≤n
 x<y→≤ {suc x} {suc y} (s≤s lt) = s≤s (x<y→≤ {x} {y} lt)
@@ -226,6 +268,26 @@
 px≤py {zero} {suc y} lt = z≤n
 px≤py {suc x} {suc y} (s≤s lt) = lt 
 
+sx≤py→x≤y : {x y : ℕ } → suc x ≤ suc y → x  ≤ y 
+sx≤py→x≤y (s≤s lt) = lt
+
+sx<py→x<y : {x y : ℕ } → suc x < suc y → x  < y 
+sx<py→x<y (s≤s lt) = lt
+
+sx≤y→x≤y : {x y : ℕ } → suc x ≤ y → x  ≤ y 
+sx≤y→x≤y {zero} {suc y} (s≤s le) = z≤n
+sx≤y→x≤y {suc x} {suc y} (s≤s le) = s≤s (sx≤y→x≤y {x} {y} le)
+
+x<sy→x≤y : {x y : ℕ } → x < suc y → x  ≤ y 
+x<sy→x≤y {zero} {suc y} (s≤s le) = z≤n
+x<sy→x≤y {suc x} {suc y} (s≤s le) = s≤s (x<sy→x≤y {x} {y} le)
+x<sy→x≤y {zero} {zero} (s≤s z≤n) = ≤-refl
+
+x≤y→x<sy : {x y : ℕ } → x ≤ y → x < suc y 
+x≤y→x<sy {.zero} {y} z≤n = ≤-trans a<sa (s≤s z≤n)
+x≤y→x<sy {.(suc _)} {.(suc _)} (s≤s le) = s≤s ( x≤y→x<sy le) 
+
+
 open import Data.Product
 
 i-j=0→i=j : {i j  : ℕ } → j ≤ i  → i - j ≡ 0 → i ≡ j
@@ -280,9 +342,16 @@
 minus+xy-zy : {x y z : ℕ } → (x + y) - (z + y)  ≡ x - z
 minus+xy-zy {x} {y} {z} = subst₂ (λ j k → j - k ≡ x - z  ) (+-comm y x) (+-comm y z) (minus+yx-yz {x} {y} {z})
 
++cancel<l : (x z : ℕ ) {y : ℕ} → y + x < y + z → x < z
++cancel<l x z {zero} lt = lt
++cancel<l x z {suc y} (s≤s lt) = +cancel<l x z {y} lt
+
++cancel<r : (x z : ℕ ) {y : ℕ} → x + y < z + y → x < z
++cancel<r x z {y} lt = +cancel<l x z (subst₂ (λ j k → j < k ) (+-comm x _) (+-comm z _) lt ) 
+
 y-x<y : {x y : ℕ } → 0 < x → 0 < y  → y - x  <  y
 y-x<y {x} {y} 0<x 0<y with <-cmp x (suc y)
-... | tri< a ¬b ¬c = +-cancelʳ-<  (y - x) _ ( begin
+... | tri< a ¬b ¬c = +cancel<r (y - x) _ ( begin
          suc ((y - x) + x) ≡⟨ cong suc (minus+n {y} {x} a ) ⟩
          suc y  ≡⟨ +-comm 1 _ ⟩
          y + suc 0  ≤⟨ +-mono-≤ ≤-refl 0<x ⟩
@@ -681,3 +750,4 @@
             ; ind = λ {p} prev → ind p prev
           } 
 
+