# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1695529231 -32400
# Node ID dfaf230f7b9a4b93c4bae01d63257fd9aef08373
# Parent  c298981108c1da40ad843157d86a991648e6bee5
...

diff -r c298981108c1 -r dfaf230f7b9a automaton-in-agda/src/finiteSetUtil.agda
--- a/automaton-in-agda/src/finiteSetUtil.agda	Sun Sep 24 11:32:01 2023 +0900
+++ b/automaton-in-agda/src/finiteSetUtil.agda	Sun Sep 24 13:20:31 2023 +0900
@@ -337,35 +337,6 @@
 
 open import Level renaming ( suc to Suc ; zero to Zero) 
 
-F2L-iso : { Q : Set } → (fin : FiniteSet Q ) → (x : Vec Bool (FiniteSet.finite fin) ) → F2L fin a<sa (λ q _ → List2Func fin a<sa x q ) ≡ x
-F2L-iso {Q} fin x = f2l m a<sa x where
-  m = FiniteSet.finite fin
-  f2l : (n : ℕ ) → (n<m : n < suc m )→ (x : Vec Bool n ) → F2L fin n<m (λ q q<n → List2Func fin n<m x q )  ≡ x 
-  f2l zero (s≤s z≤n) [] = refl
-  f2l (suc n) (s≤s n<m) (h ∷ t ) = lemma1 lemma2 lemma3f where
-    lemma1 : {n : ℕ } → {h h1 : Bool } → {t t1 : Vec Bool n } → h ≡ h1 → t ≡ t1 →  h ∷ t ≡ h1 ∷ t1
-    lemma1 refl refl = refl
-    lemma2 : List2Func fin (s≤s n<m) (h ∷ t) (FiniteSet.Q←F fin (fromℕ< n<m)) ≡ h
-    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 (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 (NP.<-trans n<m a<sa) (λ q q<n → List2Func fin (s≤s n<m) (h ∷ t) q  ) ≡ t
-    lemma3f = begin 
-         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) ?) ? ⟩
-         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
-
 
 L2F : {Q : Set } {n : ℕ } → (fin : FiniteSet Q )  → n < suc (FiniteSet.finite fin) → Vec Bool n → (q :  Q ) → toℕ (FiniteSet.F←Q fin q ) < n  → Bool
 L2F fin n<m x q q<n = List2Func fin n<m x q 
@@ -397,18 +368,6 @@
        open ≡-Reasoning
   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
-    a = FiniteSet.finite fin
-    iso : Bijection (Vec Bool a ) (A → Bool)
-    fun← iso x = F2L fin a<sa ( λ q _ → x q )
-    fun→ iso x = List2Func fin a<sa x 
-    fiso← iso x  =  F2L-iso fin x 
-    fiso→ iso f = lemma where
-      lemma : List2Func fin a<sa (F2L fin a<sa (λ q _ → f q)) ≡ f
-      lemma = ?
-    
-
 Fin2Finite : ( n : ℕ ) → FiniteSet (Fin n) 
 Fin2Finite n = record { F←Q = λ x → x ; Q←F = λ x → x ; finiso← = λ q → refl ; finiso→ = λ q → refl }
 
@@ -472,7 +431,7 @@
            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ℕ< ( NP.<-trans x n<m))
-         ≡⟨ cong (λ k → FiniteSet.Q←F fa (fromℕ< k )) ? ⟩
+         ≡⟨ cong (λ k → FiniteSet.Q←F fa k) (lemma10 refl ) ⟩
            FiniteSet.Q←F fa (fromℕ< ( toℕ<n (FiniteSet.F←Q fa elm)))
          ≡⟨ cong (λ k → FiniteSet.Q←F fa k ) ( fromℕ<-toℕ _ _ ) ⟩
            FiniteSet.Q←F fa (FiniteSet.F←Q fa elm )
@@ -636,7 +595,12 @@
                   ... | no ne = ⊥-elim (ne isb0)
              ... | no nisb1 | no  nisb0 = z≤n
              lem01 (suc i) with <-cmp (finite fa) (suc i) | <-cmp (finite fa) (suc (suc i)) 
-             ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = refl-≤≡ (sym ? )
+             ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = refl-≤≡ (sym lem14) where
+                  lem14 : count-B (suc i) ≡ count-B i
+                  lem14 with <-cmp (finite fa) (suc i) 
+                  ... | tri< a ¬b ¬c = refl
+                  ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬a a )
+                  ... | tri> ¬a ¬b c = ⊥-elim ( ¬a a )
              ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = ⊥-elim (nat-≡< b (<-trans a a<sa))
              ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = ⊥-elim (nat-<> a (<-trans a<sa c) )
              ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = refl-≤≡ (sym ?)