--- a/automaton-in-agda/src/finiteSetUtil.agda	Mon Jul 17 23:59:32 2023 +0900
+++ b/automaton-in-agda/src/finiteSetUtil.agda	Tue Jul 18 08:24:31 2023 +0900
@@ -98,6 +98,10 @@
                found2 m (<to≤ m<n) (next-end p end m<n (¬-bool-t np )) 
      not-found← : { p : Q → Bool } → exists p ≡ false → (q : Q ) → p q ≡ false 
      not-found← {p} np q = ¬-bool-t ( contra-position {_} {_} {_} {exists p ≡ true} (found q) (λ ep → ¬-bool np ep ) )
+     Q←F-inject : {x y : Fin finite} → Q←F x ≡ Q←F y → x ≡ y
+     Q←F-inject eq = subst₂ (λ j k → j ≡ k ) (finiso←  _) (finiso← _) (cong F←Q eq)
+     F←Q-inject : {x y : Q } → F←Q x ≡ F←Q y → x ≡ y
+     F←Q-inject eq = subst₂ (λ j k → j ≡ k ) (finiso→  _) (finiso→ _) (cong Q←F eq)
 
 
 
@@ -584,8 +588,8 @@
        finite = maxb
        ; Q←F = λ fb → CountB.b (cb00 _ (fin<n {_} {fb}))
        ; F←Q = λ b → fromℕ< (cb<mb b)
-       ; finiso→ = ?
-       ; finiso← = ?
+       ; finiso→ = iso1
+       ; finiso← = iso0
        } where
     f = InjectiveF.f fi
     pfa<fa : pfa < finite fa
@@ -650,4 +654,41 @@
                 toℕ (F←Q fa (f (Is.a isb))) ∎ where open ≡-Reasoning
         ... | case2 (s≤s lt) = lem09 i j lt (cong pred eq)
 
+    iso0 : (x : Fin maxb) → fromℕ< (cb<mb (CountB.b (cb00 (toℕ x) fin<n))) ≡ x 
+    iso0 x = begin
+         fromℕ< (cb<mb (CountB.b (cb00 (toℕ x) fin<n))) ≡⟨ fromℕ<-cong _ _ ( begin 
+            pred (count-B (toℕ (F←Q fa (f (CountB.b (cb00 (toℕ x) fin<n))))))  ≡⟨ sym (cong (λ k → pred (count-B k)) (CountB.b=cn CB)) ⟩
+            pred (count-B (CountB.cb CB))   ≡⟨ cong pred (CountB.cb=n CB) ⟩
+            pred (suc (toℕ x))  ≡⟨ refl ⟩
+            toℕ x ∎ ) (cb<mb (CountB.b CB)) fin<n ⟩ 
+         fromℕ< (fin<n {_} {x}) ≡⟨ fromℕ<-toℕ _ (fin<n {_} {x}) ⟩ 
+         x ∎ where
+             open ≡-Reasoning
+             CB = cb00 (toℕ x) fin<n
+
+    iso1 : (b : B) → CountB.b (cb00 (toℕ (fromℕ< (cb<mb b))) fin<n) ≡ b
+    iso1 b with count-B (toℕ (fromℕ< (cb<mb b))) | inspect count-B (toℕ (fromℕ< (cb<mb b))) 
+    ... | zero | record { eq = eq1 } = ?
+    ... | suc n | record { eq = eq1 } =  begin
+         CountB.b CB ≡⟨ InjectiveF.inject fi (F←Q-inject fa (toℕ-injective (begin
+            toℕ (F←Q fa (f (CountB.b CB))) ≡⟨ sym (CountB.b=cn CB) ⟩
+            CountB.cb CB ≡⟨ CountB.cb-inject CB _ fin<n isb lem30 ⟩
+            toℕ (F←Q fa (f b)) ∎ ) ))  ⟩
+         b ∎ where
+             open ≡-Reasoning
+             CB = cb00 (toℕ (fromℕ< (cb<mb b))) fin<n
+             isb : Is B A f (Q←F fa (fromℕ< fin<n))
+             isb = ?
+             lem31 : 0 < count-B (toℕ (F←Q fa (f b)))
+             lem31 = ?
+             lem30 : count-B (CountB.cb CB) ≡ count-B (toℕ (F←Q fa (InjectiveF.f fi b)))
+             lem30 = begin
+                 count-B (CountB.cb CB) ≡⟨ CountB.cb=n CB ⟩
+                 suc (toℕ (fromℕ< (cb<mb b)))  ≡⟨ cong suc (toℕ-fromℕ< (cb<mb b)) ⟩
+                 suc (pred (count-B (toℕ (F←Q fa (f b))))) ≡⟨ sucprd lem31 ⟩
+                 count-B (toℕ (F←Q fa (f b))) ∎ 
+
+
+
+
 -- end