# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1695522721 -32400
# Node ID c298981108c1da40ad843157d86a991648e6bee5
# Parent  093e386c10a231382eea47d054ee8df633c0522e
fix for std-lib 2.0

diff -r 093e386c10a2 -r c298981108c1 automaton-in-agda/automaton-in-agda.agda-lib
--- a/automaton-in-agda/automaton-in-agda.agda-lib	Thu Aug 10 09:59:47 2023 +0900
+++ b/automaton-in-agda/automaton-in-agda.agda-lib	Sun Sep 24 11:32:01 2023 +0900
@@ -1,6 +1,8 @@
 -- File generated by Agda-Pkg
 name:    automaton-in-agda
-depend: standard-library
+depend: standard-library-2.0
 include: src
+flags:
+   --warning=noUnsupportedIndexedMatch
 
 -- End 
diff -r 093e386c10a2 -r c298981108c1 automaton-in-agda/src/automaton.agda
--- a/automaton-in-agda/src/automaton.agda	Thu Aug 10 09:59:47 2023 +0900
+++ b/automaton-in-agda/src/automaton.agda	Sun Sep 24 11:32:01 2023 +0900
@@ -1,3 +1,4 @@
+{-# OPTIONS --cubical-compatible --safe #-}
 module automaton where
 
 open import Data.Nat
diff -r 093e386c10a2 -r c298981108c1 automaton-in-agda/src/bijection.agda
--- a/automaton-in-agda/src/bijection.agda	Thu Aug 10 09:59:47 2023 +0900
+++ b/automaton-in-agda/src/bijection.agda	Sun Sep 24 11:32:01 2023 +0900
@@ -1,4 +1,4 @@
-{-# OPTIONS --allow-unsolved-metas #-}
+{-# OPTIONS --cubical-compatible --safe #-}
 
 module bijection where
 
@@ -217,8 +217,8 @@
      --
      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)  in eq 
+     ... | zero = record { k = suc (sum ) ; j = 0
          ; k1 = nn02 ; nn-unique = nn04 } where
             ---
             --- increment the stage
@@ -262,7 +262,7 @@
                   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
+     ... | suc k  = record { k = k ; j = suc (NN.j (nn i)) ; k1 = nn11 ;  nn-unique = nn13 } where
             ---
             --- increment in a stage
             ---
@@ -438,8 +438,8 @@
      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)
-     ... | [] | record { eq = eq } = record { nlist = false ∷ [] ; isUnique = lb06 ; isBin = lb10 } where
+     lb (suc n) with LB.nlist (lb n) in eq
+     ... | [] = record { nlist = false ∷ [] ; isUnique = lb06 ; isBin = lb10 } where
          open ≡-Reasoning
          lb10 : lton1 (false ∷ []) ∸ 1 ≡ suc n
          lb10 = begin
@@ -450,7 +450,7 @@
            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
+     ... | false ∷ t =  record { nlist = true ∷ t ; isBin = lb01 ; isUnique = lb09 } where
         lb01 : lton (true ∷ t) ≡ suc n
         lb01 = begin
            lton (true ∷ t)  ≡⟨ refl ⟩
@@ -461,7 +461,7 @@
            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
+     ... | true ∷ t = 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 ) ⟩
@@ -757,14 +757,14 @@
         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
+            lem20 zero (suc j) i<j bi bj le with  is-B (fun← cn 0) in eq1 | is-B (fun← cn (suc j)) in eq2
+            ... | no nisc  | _ = ⊥-elim (nisc bi)
+            ... |  yes _ | no nisc = ⊥-elim (nisc bj)
+            ... | yes _ | yes _ = ⊥-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 )
+                 lem22 with is-B (fun← cn 0) in eq1
+                 ... | yes _ = refl
+                 ... | no nisa = ⊥-elim ( nisa bi )
                  lem24 : count-B j ≡ 0
                  lem24 = cong pred le
                  lem25 : 1 ≤ 0
@@ -780,18 +780,18 @@
                  --    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 )
+                 lem22 with is-B (fun← cn (suc i)) in eq1
+                 ... | yes _ = 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 )
+                 lem23 with is-B (fun← cn (suc j)) in eq1 
+                 ... | yes _ = 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)
+                 lem24 with  is-B (fun← cn (suc i)) in eq1 | is-B (fun← cn (suc j)) in eq2
+                 ... | no nisc  | _ = ⊥-elim (nisc bi)
+                 ... | yes _ | no nisc = ⊥-elim (nisc bj)
+                 ... | yes _ |  yes _ = sym (cong pred le)
                  lem21 : suc (count-B i) ≤ count-B j
                  lem21 = begin
                      suc (count-B i) ≡⟨ lem22 ⟩
@@ -805,32 +805,44 @@
             ... | 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
+        lem07 n 0 eq with is-B (fun← cn 0) 
+        ... | yes isb = lem13 where
+            cb1 = count-B 0
+            lem14 : count-B 0 ≡ 1
+            lem14 with  is-B (fun← cn 0)
+            ... | yes _ = refl
+            ... | no ne = ⊥-elim (ne isb)
             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 iscb1 cbeq = lem06 0 cb1 isb iscb1 (trans lem14 cbeq) 
+            lem13 : CountB n
+            lem13 = record { b = Is.a isb ; cb = 0 ; b=cn = sym (Is.fa=c isb) ; cb=n = trans lem14 eq
+                ; cb-inject = λ cb1 iscb1 cb1eq → lem12 cb1 iscb1 (subst (λ k → k ≡ count-B cb1) lem14 cb1eq)   } 
+        ... | no nisb = ⊥-elim ( nat-≡< eq (s≤s z≤n ) )
+        lem07 n (suc i) eq with is-B (fun← cn (suc i)) 
+        ... | yes isb = record { b = Is.a isb ; cb = suc i ; b=cn = sym (Is.fa=c isb) ; cb=n = trans lem14 eq
+                 ; cb-inject = λ cb1 iscb1 cb1eq → lem12 cb1 iscb1 (subst (λ k → k ≡ count-B cb1) lem14 cb1eq)   } where
+            cbs = count-B (suc i)
+            lem14 : count-B (suc i) ≡ suc (count-B i)
+            lem14 with  is-B (fun← cn (suc i))
+            ... | yes _ = refl
+            ... | no ne = ⊥-elim (ne isb)
             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
+            lem12 cb1 iscb1 cbeq = lem06 (suc i) cb1 isb iscb1 (trans lem14 cbeq)
+        ... | no nisb = 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))
+        ... | case2 (s≤s lt) with is-B (fun← cn 0) in eq1
+        ... | yes isb = ⊥-elim ( nat-≤> (≤-trans (s≤s lt) (refl-≤≡ eq) ) (s≤s (s≤s z≤n)) )
+        ... | no nisb = ⊥-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
+        ... | case2 (s≤s lt) with is-B (fun← cn (suc i)) in eq1
+        ... | yes isb = lem09 i j lt (cong pred eq)
+        ... | no nisb = lem09 i (suc j) (≤-trans lt a≤sa) eq
 
     bton : B → ℕ
     bton b = pred (count-B (fun→ cn (g b)))
@@ -853,18 +865,18 @@
     -- 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
+    biso1 b with count-B (fun→ cn (g b)) in eq1
+    ... | zero  = ⊥-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 
+        lem21 0 eq with is-B (fun← cn 0) in eq1
+        ... | yes isb = ≤-refl
+        ... | no nisb = ⊥-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)) in eq2
+        ... | yes isb = s≤s z≤n
+        ... | no nisb = ⊥-elim ( nisb record { a = b ; fa=c = trans (sym (fiso← cn _)) (cong (fun← cn) (sym eq)) } )
+    ... | suc n = 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 _ ⟩
@@ -991,27 +1003,27 @@
 -- 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← = ?
-     }
+-- 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 093e386c10a2 -r c298981108c1 automaton-in-agda/src/derive.agda
--- a/automaton-in-agda/src/derive.agda	Thu Aug 10 09:59:47 2023 +0900
+++ b/automaton-in-agda/src/derive.agda	Sun Sep 24 11:32:01 2023 +0900
@@ -238,6 +238,9 @@
      fb00 record { s = s ; is-sub = (sub* is-sub) } = {!!}
      fb00 record { s = (z & (x *)) ; is-sub = (sub*& z x lt is-sub) } = case1 record { z = z ; is-sub = is-sub ; lt = lt }
 
+d-ISB : (r : Regex Σ) → ISB r → (s : Σ) → ISB r → Bool
+d-ISB r x s y = ?
+
 toSB : (r : Regex   Σ) →  ISB r → Bool
 toSB r record { s = s ; is-sub = is-sub } with rg-eq? r s
 ... | yes _ = true
@@ -274,24 +277,8 @@
 sbderive : (r : Regex Σ) →  (ISB r → Bool) → Σ → ISB r → Bool
 sbderive ε f s record { s = .ε ; is-sub = sε } = false
 sbderive φ f s record { s = t ; is-sub = sφ } = false
-sbderive (r *) f s record { s = t ; is-sub = sub* is-sub } with f record { s = t ; is-sub = sub* is-sub } 
-... | false = true
-... | true with derivative r s
-... | ε = true
-... | φ = false
-... | t₁ * = false
-... | t₁ & t₂ = false
-... | t₁ || t₂ = false
-... | < x > = false
-sbderive (r *) f s record { s = .(x & (r *)) ; is-sub = sub*& x .r x₁ is-sub } with f record { s = (x & (r *)) ; is-sub = sub*& x r x₁ is-sub } 
-... | false = true
-... | true with derivative r s
-... | ε = false
-... | φ = false
-... | t₁ * = true
-... | t₁ & t₂ = true
-... | t₁ || t₂ = true
-... | < s > = true
+sbderive (r *) f s record { s = t ; is-sub = sub* is-sub } = ?
+sbderive (r *) f s record { s = .(x & (r *)) ; is-sub = sub*& x .r x₁ is-sub } = ?
 sbderive (r & r₁) f s record { s = t ; is-sub = sub&1 .r .r₁ .t is-sub } with f record { s = t ; is-sub = sub&1 r r₁ t is-sub } 
 ... | false = true
 ... | true = false
diff -r 093e386c10a2 -r c298981108c1 automaton-in-agda/src/fin.agda
--- a/automaton-in-agda/src/fin.agda	Thu Aug 10 09:59:47 2023 +0900
+++ b/automaton-in-agda/src/fin.agda	Sun Sep 24 11:32:01 2023 +0900
@@ -1,9 +1,9 @@
-{-# OPTIONS --allow-unsolved-metas #-} 
+{-# OPTIONS --cubical-compatible  --safe #-}
 
 module fin where
 
 open import Data.Fin hiding (_<_ ; _≤_ ; _>_ ; _+_ )
-open import Data.Fin.Properties as DFP hiding (≤-trans ;  <-trans ;  ≤-refl  ) renaming ( <-cmp to <-fcmp )
+open import Data.Fin.Properties hiding (≤-trans ;  <-trans ;  ≤-refl  ) renaming ( <-cmp to <-fcmp )
 open import Data.Nat
 open import Data.Nat.Properties
 open import logic
@@ -23,7 +23,7 @@
 
 pred<n : {n : ℕ} {f : Fin (suc n)} → n > 0  → Data.Nat.pred (toℕ f) < n
 pred<n {suc n} {zero} (s≤s z≤n) = s≤s z≤n
-pred<n {suc n} {suc f} (s≤s z≤n) = fin<n f
+pred<n {suc n} {suc f} (s≤s z≤n) = fin<n _
 
 fin<asa : {n : ℕ} → toℕ (fromℕ< {n} a<sa) ≡ n
 fin<asa = toℕ-fromℕ< nat.a<sa
@@ -33,17 +33,20 @@
 toℕ→from {0} {zero} refl = refl
 toℕ→from {suc n} {suc x} eq = cong (λ k → suc k ) ( toℕ→from {n} {x} (cong (λ k → Data.Nat.pred k ) eq ))
 
-0≤fmax : {n : ℕ } → (# 0) Data.Fin.≤ fromℕ< {n} a<sa
-0≤fmax  = subst (λ k → 0 ≤ k ) (sym (toℕ-fromℕ< a<sa)) z≤n
+-- 0≤fmax : {n : ℕ } → (# 0) Data.Fin.≤ fromℕ< {n} a<sa
+-- 0≤fmax {n} = ?
 
-0<fmax : {n : ℕ } → (# 0) Data.Fin.< fromℕ< {suc n} a<sa
-0<fmax = subst (λ k → 0 < k ) (sym (toℕ-fromℕ< a<sa)) (s≤s z≤n)
+-- 0<fmax : {n : ℕ } → (# 0) Data.Fin.< fromℕ< {suc n} a<sa
+-- 0<fmax {n} = subst (λ k → 0 < k ) (sym (toℕ-fromℕ< {suc n} {suc (suc n)} a<sa)) (s≤s z≤n)
 
 -- toℕ-injective
 i=j : {n : ℕ} (i j : Fin n) → toℕ i ≡ toℕ j → i ≡ j
 i=j {suc n} zero zero refl = refl
 i=j {suc n} (suc i) (suc j) eq = cong ( λ k → suc k ) ( i=j i j (cong ( λ k → Data.Nat.pred k ) eq) )
 
+fin1≡0 : (f : Fin 1) → # 0 ≡ f
+fin1≡0 zero = refl
+
 -- raise 1
 fin+1 :  { n : ℕ } → Fin n → Fin (suc n)
 fin+1  zero = zero 
@@ -51,9 +54,6 @@
 
 open import Data.Nat.Properties as NatP  hiding ( _≟_ )
 
-fin1≡0 : (f : Fin 1) → # 0 ≡ f
-fin1≡0 zero = refl
-
 fin+1≤ : { i n : ℕ } → (a : i < n)  → fin+1 (fromℕ< a) ≡ fromℕ< (<-trans a a<sa)
 fin+1≤ {0} {suc i} (s≤s z≤n) = refl
 fin+1≤ {suc n} {suc (suc i)} (s≤s (s≤s a)) = cong (λ k → suc k ) ( fin+1≤ {n} {suc i} (s≤s a) )
@@ -90,32 +90,39 @@
 lemma12 {zero} {suc m} (s≤s z≤n) zero refl = refl
 lemma12 {suc n} {suc m} (s≤s n<m) (suc f) refl =  cong suc ( lemma12 {n} {m} n<m f refl  ) 
 
-open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
+-- this requires K
+--
+-- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
 
 -- <-irrelevant
-<-nat=irr : {i j n : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → i<n ≅ j<n  
-<-nat=irr {zero} {zero} {suc n} refl {s≤s z≤n} {s≤s z≤n} = HE.refl
-<-nat=irr {suc i} {suc i} {suc n} refl {s≤s i<n} {s≤s j<n} = HE.cong (λ k → s≤s k ) ( <-nat=irr {i} {i} {n} refl  )
+-- <-nat=irr : {i j n : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → i<n ≅ j<n  
+-- <-nat=irr {zero} {zero} {suc n} refl {s≤s z≤n} {s≤s z≤n} = HE.refl
+-- <-nat=irr {suc i} {suc i} {suc n} refl {s≤s i<n} {s≤s j<n} = HE.cong (λ k → s≤s k ) ( <-nat=irr {i} {i} {n} refl  )
+
+-- lemma8 : {i j n : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → i<n ≅ j<n  
+-- lemma8 {zero} {zero} {suc n} refl {s≤s z≤n} {s≤s z≤n} = HE.refl
+-- lemma8 {suc i} {suc i} {suc n} refl {s≤s i<n} {s≤s j<n} = HE.cong (λ k → s≤s k ) ( lemma8 {i} {i} {n} refl  )
 
-lemma8 : {i j n : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → i<n ≅ j<n  
-lemma8 {zero} {zero} {suc n} refl {s≤s z≤n} {s≤s z≤n} = HE.refl
-lemma8 {suc i} {suc i} {suc n} refl {s≤s i<n} {s≤s j<n} = HE.cong (λ k → s≤s k ) ( lemma8 {i} {i} {n} refl  )
+lemma10 : {n i j  : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n }  → fromℕ< i<n ≡ fromℕ< j<n
+lemma10 {.(suc _)} {zero} {zero} refl {s≤s z≤n} {s≤s z≤n} = refl
+lemma10 {suc n} {suc i} {suc i} refl {s≤s i<n} {s≤s j<n} = cong suc (lemma10 {n} {i} {i} refl {i<n} {j<n})
 
--- fromℕ<-irrelevant 
-lemma10 : {n i j  : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n }  → fromℕ< i<n ≡ fromℕ< j<n
-lemma10 {n} refl  = HE.≅-to-≡ (HE.cong (λ k → fromℕ< k ) (lemma8 refl  ))
+fpred-comm : {n : ℕ } → (x : Fin n) → toℕ (Data.Fin.pred x) ≡ toℕ x ∸ 1
+fpred-comm {suc n} zero = refl
+fpred-comm {suc n} (suc x) = begin
+       toℕ (Data.Fin.pred (suc x)) ≡⟨ sym ( toℕ-fromℕ< _ ) ⟩
+       toℕ (fromℕ< (fin<n _) ) ≡⟨ cong toℕ (lemma10 (toℕ-inject₁ _ ) ) ⟩
+       toℕ (fromℕ< (<-trans (fin<n _) a<sa) ) ≡⟨  toℕ-fromℕ< _ ⟩
+       toℕ (suc x) ∸ 1 ∎  where open ≡-Reasoning
 
-lemma31 : {a b c : ℕ } → { a<b : a < b } { b<c : b < c } { a<c : a < c } → NatP.<-trans a<b b<c ≡ a<c
-lemma31 {a} {b} {c} {a<b} {b<c} {a<c} = HE.≅-to-≡ (lemma8 refl) 
+-- lemma31 : {a b c : ℕ } → { a<b : a < b } { b<c : b < c } { a<c : a < c } → NatP.<-trans a<b b<c ≡ a<c
+-- lemma31 {a} {b} {c} {a<b} {b<c} {a<c} = HE.≅-to-≡ (lemma8 refl) 
 
 -- toℕ-fromℕ<
 lemma11 : {n m : ℕ } {x : Fin n } → (n<m : n < m ) → toℕ (fromℕ< (NatP.<-trans (toℕ<n x) n<m)) ≡ toℕ x
 lemma11 {n} {m} {x} n<m  = begin
-              toℕ (fromℕ< (NatP.<-trans (toℕ<n x) n<m))
-           ≡⟨ toℕ-fromℕ< _ ⟩
-              toℕ x
-           ∎  where
-               open ≡-Reasoning
+      toℕ (fromℕ< (NatP.<-trans (toℕ<n x) n<m)) ≡⟨ toℕ-fromℕ< _ ⟩
+      toℕ x ∎  where open ≡-Reasoning
 
 x<y→fin-1 : {n : ℕ } → { x y : Fin (suc n)} →  toℕ x < toℕ y  → Fin n
 x<y→fin-1 {n} {x} {y} lt = fromℕ< (≤-trans lt (fin≤n _ ))
@@ -140,12 +147,21 @@
 -- find duplicate element in a List (Fin n)
 --
 --    if the length is longer than n, we can find duplicate element as FDup-in-list 
+--
+--  How about do it in ℕ ?
 
-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 y)  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
+-- fin-count q (q0 ∷ qs ) with <-fcmp q q0 
+-- ... | tri-e = suc (fin-count q qs)
+-- ... | false = fin-count q qs
+
+-- fin-not-dup-in-list : { n : ℕ}  (qs : List (Fin n) ) → Set
+-- fin-not-dup-in-list {n} qs = (q : Fin n) → fin-count q ≤ 1
+
+-- this is far easier
+-- fin-not-dup-in-list→len<n : { n : ℕ}  (qs : List (Fin n) ) → ( (q : Fin n) → fin-not-dup-in-list qs q) → length qs ≤ n
+-- fin-not-dup-in-list→len<n = ?
 
 fin-phase2 : { n : ℕ }  (q : Fin n) (qs : List (Fin n) ) → Bool  -- find the dup
 fin-phase2 q [] = false
@@ -175,6 +191,11 @@
 ... | tri≈ ¬a b ¬c = list-less ls
 ... | tri> ¬a ¬b c = x<y→fin-1 c ∷ list-less ls
 
+fin010 : {n m : ℕ } {x : Fin n} (c : suc (toℕ x) ≤ toℕ (fromℕ< {m} a<sa) ) → toℕ (fromℕ< (≤-trans c (fin≤n (fromℕ< a<sa)))) ≡ toℕ x
+fin010 {_} {_} {x} c = begin 
+           toℕ (fromℕ< (≤-trans c (fin≤n (fromℕ< a<sa))))  ≡⟨ toℕ-fromℕ< _ ⟩
+           toℕ x  ∎   where open ≡-Reasoning
+
 ---
 ---  if List (Fin n) is longer than n, there is at most one duplication
 ---
@@ -233,7 +254,7 @@
           ... | tri< a ¬b ¬c₁ = f1-phase1 qs p (case2 q1)
           ... | tri≈ ¬a₁ b₁ ¬c₁ = ⊥-elim (fdup-10 b b₁) where
                fdup-10 : fromℕ< a<sa ≡ x → fin+1 i ≡ x → ⊥
-               fdup-10 eq eq1 = nat-≡< (cong toℕ (trans eq1 (sym eq))) (subst₂ (λ j k → j < k ) (sym fin+1-toℕ) (sym fin<asa) (fin<n _)) 
+               fdup-10 eq eq1 = nat-≡< (cong toℕ (trans eq1 (sym eq))) (subst₂ (λ j k → j < k ) (sym fin+1-toℕ) (sym fin<asa) (fin<n _) ) 
           ... | tri> ¬a₁ ¬b c = f1-phase1 qs p (case2 q1)
           f1-phase1 (x ∷ qs) p (case1 q1) | tri> ¬a ¬b c with <-fcmp i (fromℕ< (≤-trans c (fin≤n (fromℕ< a<sa)))) | <-fcmp (fin+1 i) x
           ... | tri< a ¬b₁ ¬c | tri< a₁ ¬b₂ ¬c₁ = f1-phase1 qs p (case1 q1)
@@ -259,9 +280,9 @@
           ... | tri> ¬a₁ ¬b₁ c₁ | tri≈ ¬a₂ b ¬c = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) (sym fin+1-toℕ) (toℕ-fromℕ< _) c₁ ))
           ... | tri> ¬a₁ ¬b₁ c₁ | tri> ¬a₂ ¬b₂ c₂ = f1-phase1 qs p (case2 q1)
      fdup-phase0 : FDup-in-list (suc n) qs 
-     fdup-phase0 with fin-dup-in-list (fromℕ< a<sa) qs | inspect (fin-dup-in-list (fromℕ< a<sa)) qs
-     ... | true  | record { eq = eq } = record { dup = fromℕ< a<sa ; is-dup = eq }
-     ... | false | record { eq = ne } = fdup+1 qs (FDup-in-list.dup fdup) ne (FDup-in-list.is-dup fdup)  where
+     fdup-phase0 with fin-dup-in-list (fromℕ< a<sa) qs in eq 
+     ... | true  = record { dup = fromℕ< a<sa ; is-dup = eq }
+     ... | false = fdup+1 qs (FDup-in-list.dup fdup) eq (FDup-in-list.is-dup fdup)  where
            -- if no dup in the max element, the list without the element is only one length shorter
            fless : (qs : List (Fin (suc n))) → length qs > suc n  → fin-dup-in-list (fromℕ< a<sa) qs ≡ false → n < length (list-less qs) 
            fless qs lt p = fl-phase1 n qs lt p where
@@ -283,6 +304,6 @@
                ... | tri> ¬a ¬b c = s≤s ( fl-phase1 n1 qs lt p )
            -- if the list without the max element is only one length shorter, we can recurse
            fdup : FDup-in-list n (list-less qs)
-           fdup = fin-dup-in-list>n (list-less qs) (fless qs lt ne)
+           fdup = fin-dup-in-list>n (list-less qs) (fless qs lt eq)
 
 --
diff -r 093e386c10a2 -r c298981108c1 automaton-in-agda/src/finiteSet.agda
--- a/automaton-in-agda/src/finiteSet.agda	Thu Aug 10 09:59:47 2023 +0900
+++ b/automaton-in-agda/src/finiteSet.agda	Sun Sep 24 11:32:01 2023 +0900
@@ -1,4 +1,4 @@
-{-# OPTIONS --allow-unsolved-metas #-}
+{-# OPTIONS --cubical-compatible --safe #-}
 module finiteSet  where
 
 open import Data.Nat hiding ( _≟_ )
@@ -12,7 +12,7 @@
 open import nat
 open import Data.Nat.Properties hiding ( _≟_ )
 
-open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
+-- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
 
 record FiniteSet ( Q : Set ) : Set  where
      field
diff -r 093e386c10a2 -r c298981108c1 automaton-in-agda/src/finiteSetUtil.agda
--- a/automaton-in-agda/src/finiteSetUtil.agda	Thu Aug 10 09:59:47 2023 +0900
+++ b/automaton-in-agda/src/finiteSetUtil.agda	Sun Sep 24 11:32:01 2023 +0900
@@ -1,4 +1,4 @@
-{-# OPTIONS --allow-unsolved-metas #-} 
+{-# OPTIONS --cubical-compatible  --safe #-}
 
 module finiteSetUtil  where
 
@@ -14,7 +14,6 @@
 open import finiteSet
 open import fin
 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
      field
@@ -25,13 +24,12 @@
 
 open import Axiom.Extensionality.Propositional
 open import Level hiding (suc ; zero)
-postulate f-extensionality : { n : Level}  → Axiom.Extensionality.Propositional.Extensionality n n -- (Level.suc n)
 
 module _ {Q : Set } (F : FiniteSet Q) where
      open FiniteSet F
      equal?-refl  : { x : Q } → equal? x x ≡ true 
      equal?-refl {x} with F←Q x ≟ F←Q x
-     ... | yes refl = refl
+     ... | yes eq = refl
      ... | no ne = ⊥-elim (ne refl)
      equal→refl  : { x y : Q } → equal? x y ≡ true → x ≡ y
      equal→refl {q0} {q1} eq with F←Q q0 ≟ F←Q q1
@@ -89,9 +87,9 @@
      found← : { p : Q → Bool } → exists p ≡ true → Found Q p
      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
-             lemma = f-extensionality ( λ q → subst (λ k → p k ≡ p q ) (sym (finiso→ q)) refl )
+         found2 0 m<n end = ⊥-elim ( ¬-bool f01 exst ) where
+             f01 : exists p ≡ false
+             f01 = not-found (λ q → subst ( λ k → p k ≡ false  ) (finiso→ _) (end (F←Q q)  z≤n ))
          found2 (suc m)  m<n end with bool-≡-? (p (Q←F (fromℕ< m<n))) true
          found2 (suc m)  m<n end | yes eq = record { found-q = Q←F (fromℕ< m<n) ; found-p = eq }
          found2 (suc m)  m<n end | no np = 
@@ -289,7 +287,7 @@
        open ≡-Reasoning
        open Data.Product
 
-cast-iso : {n m : ℕ } → (eq : n ≡ m ) → (f : Fin m ) → cast eq ( cast (sym eq ) f)  ≡ f
+cast-iso : {n m : ℕ } → (eq : n ≡ m ) → (f : Fin m ) → Data.Fin.cast eq ( Data.Fin.cast (sym eq ) f)  ≡ f
 cast-iso refl zero =  refl
 cast-iso refl (suc f) = cong ( λ k → suc k ) ( cast-iso refl f )
 
@@ -338,8 +336,6 @@
 ... | 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
--- postulate f-extensionality : { n : Level}  →  Axiom.Extensionality.Propositional.Extensionality n n 
 
 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
@@ -363,9 +359,7 @@
     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) ( λ q q<n → k q q<n ))
-              (f-extensionality ( λ q →  
-              (f-extensionality ( λ q<n →  lemma4 q q<n )))) ⟩
+       ≡⟨  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
@@ -410,9 +404,9 @@
     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 x = lemma where
-      lemma : List2Func fin a<sa (F2L fin a<sa (λ q _ → x q)) ≡ x
-      lemma = f-extensionality ( λ q → L2F-iso fin x q )
+    fiso→ iso f = lemma where
+      lemma : List2Func fin a<sa (F2L fin a<sa (λ q _ → f q)) ≡ f
+      lemma = ?
     
 
 Fin2Finite : ( n : ℕ ) → FiniteSet (Fin n) 
@@ -427,21 +421,10 @@
 get-< : { n : ℕ }  { A : Set } {fa : FiniteSet A } {n<m : n < FiniteSet.finite fa }→ (f : fin-less fa n<m ) → toℕ (FiniteSet.F←Q fa (get-elm f )) < n
 get-< (elm1 _ b ) = b
 
-fin-less-cong : { n : ℕ }  { A : Set } (fa : FiniteSet A ) (n<m : n < FiniteSet.finite fa )
-   → (x y : fin-less fa n<m ) → get-elm {n} {A} {fa} x ≡ get-elm {n} {A} {fa} y → get-< x ≅  get-< y → x ≡ y
-fin-less-cong fa n<m (elm1 elm x) (elm1 elm x) refl HE.refl = refl
-
 fin-< : {A : Set} → { n : ℕ } → (fa : FiniteSet A ) → (n<m : n < FiniteSet.finite fa ) → FiniteSet (fin-less fa n<m ) 
 fin-< {A}  {n} fa n<m = iso-fin (Fin2Finite n) iso where
     m = FiniteSet.finite fa
     iso : Bijection (Fin n) (fin-less fa n<m )
-    lemma8f : {i j n : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → i<n ≅ j<n  
-    lemma8f {zero} {zero} {suc n} refl {s≤s z≤n} {s≤s z≤n} = HE.refl
-    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 } → 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ℕ< (NP.<-trans (toℕ<n x) n<m)) ≡ toℕ x
     lemma11f {n} {x} n<m  = begin
          toℕ (fromℕ< (NP.<-trans (toℕ<n x) n<m))
@@ -475,7 +458,7 @@
           open ≡-Reasoning
           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
+    fiso→ iso (elm1 elm x) = ? where -- 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
             toℕ (fromℕ< x)
@@ -489,7 +472,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 )) (HE.≅-to-≡ (lemma8 refl)) ⟩
+         ≡⟨ cong (λ k → FiniteSet.Q←F fa (fromℕ< k )) ? ⟩
            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 )
@@ -545,22 +528,22 @@
 dup-in-list+fin {Q} finq q qs p = i-phase1 qs p where
     i-phase2 : (qs : List Q) →   fin-phase2 (F←Q  finq q) (map (F←Q finq) qs) ≡ true
         → phase2 finq q qs ≡ true 
-    i-phase2 (x ∷ qs) p with equal? finq q x | inspect (equal? finq q ) x | <-fcmp  (F←Q finq q)  (F←Q finq x)
-    ... | true | _ | t = refl
-    ... | false | _ | tri< a ¬b ¬c = i-phase2 qs p
-    ... | false | record { eq = eq }  | tri≈ ¬a b ¬c = ⊥-elim (¬-bool eq
+    i-phase2 (x ∷ qs) p with equal? finq q x in eq | <-fcmp  (F←Q finq q)  (F←Q finq x)
+    ... | true |  t = refl
+    ... | false |  tri< a ¬b ¬c = i-phase2 qs p
+    ... | false |  tri≈ ¬a b ¬c = ⊥-elim (¬-bool eq
         (subst₂ (λ j k → equal? finq j k ≡ true) (finiso→ finq q) (subst (λ k →  Q←F finq k ≡ x) (sym b) (finiso→ finq x)) ( equal?-refl finq  )))
-    ... | false | _ | tri> ¬a ¬b c = i-phase2 qs p
+    ... | false |  tri> ¬a ¬b c = i-phase2 qs p
     i-phase1 : (qs : List Q) → fin-phase1 (F←Q  finq q) (map (F←Q finq) qs) ≡ true 
         → phase1 finq q qs ≡ true 
-    i-phase1 (x ∷ qs) p with equal? finq q x |  inspect (equal? finq q ) x | <-fcmp  (F←Q finq q)  (F←Q finq x)
-    ... | true | record { eq = eq }  | tri< a ¬b ¬c =  ⊥-elim ( nat-≡< (cong (λ x → toℕ (F←Q finq x)) ( equal→refl finq eq )) a )
-    ... | true | _ | tri≈ ¬a b ¬c = i-phase2 qs p
-    ... | true | record { eq = eq}  | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (cong (λ x → toℕ (F←Q finq x)) (sym ( equal→refl finq eq ))) c )
-    ... | false | _ | tri< a ¬b ¬c = i-phase1 qs p
-    ... | false | record {eq = eq} | tri≈ ¬a b ¬c = ⊥-elim (¬-bool eq
+    i-phase1 (x ∷ qs) p with equal? finq q x in eq | <-fcmp  (F←Q finq q)  (F←Q finq x)
+    ... | true |  tri< a ¬b ¬c =  ⊥-elim ( nat-≡< (cong (λ x → toℕ (F←Q finq x)) ( equal→refl finq eq )) a )
+    ... | true |  tri≈ ¬a b ¬c = i-phase2 qs p
+    ... | true |  tri> ¬a ¬b c = ⊥-elim ( nat-≡< (cong (λ x → toℕ (F←Q finq x)) (sym ( equal→refl finq eq ))) c )
+    ... | false |  tri< a ¬b ¬c = i-phase1 qs p
+    ... | false |  tri≈ ¬a b ¬c = ⊥-elim (¬-bool eq
         (subst₂ (λ j k → equal? finq j k ≡ true) (finiso→ finq q) (subst (λ k →  Q←F finq k ≡ x) (sym b) (finiso→ finq x)) ( equal?-refl finq  )))
-    ... | false | _ | tri> ¬a ¬b c = i-phase1 qs p
+    ... | false |  tri> ¬a ¬b c = i-phase1 qs p
 
 record Dup-in-list {Q : Set } (finq : FiniteSet Q) (qs : List Q)  : Set where
    field
@@ -587,8 +570,8 @@
    → (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 with finite fa | inspect finite fa
-... | zero | record { eq = eq1 } = record {
+inject-fin {A} {B} fa fi is-B with finite fa in eq1 
+... | zero = record {
        finite = 0
        ; Q←F = λ ()
        ; F←Q = λ b → ⊥-elim ( lem00 b)
@@ -598,7 +581,7 @@
           lem00 : ( b : B) → ⊥
           lem00 b with subst (λ k → Fin k ) eq1 (F←Q fa (InjectiveF.f fi b))
           ... | ()
-... | suc pfa | record { eq = eq1 } = record {
+... | suc pfa = record {
        finite = maxb
        ; Q←F = λ fb → CountB.b (cb00 _ (fin<n {_} fb))
        ; F←Q = λ b → fromℕ< (cb<mb b)
@@ -643,28 +626,32 @@
              lem01 zero with <-cmp (finite fa) 1 
              lem01 zero | tri< a ¬b ¬c = ≤-refl
              lem01 zero | tri≈ ¬a b ¬c = ≤-refl
-             lem01 zero | tri> ¬a ¬b c with is-B (Q←F fa (fromℕ< c)) | is-B (Q←F fa ( fromℕ< {0} 0<fa )) | inspect count-B 0
-             ... | yes isb1 | yes isb0  | record { eq = eq0 } = s≤s z≤n
-             ... | yes isb1 | no  nisb0 | record { eq = eq0 } = z≤n
-             ... | no nisb1 | yes isb0  | record { eq = eq0 } = refl-≤≡ (sym eq0)
-             ... | no nisb1 | no  nisb0 | record { eq = eq0 } = z≤n
-             lem01 (suc i) with <-cmp (finite fa) (suc i) | <-cmp (finite fa) (suc (suc i)) | inspect count-B (suc i) | inspect count-B (suc (suc i))
-             ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ | record { eq = eq0 } | record { eq = eq1 } = refl-≤≡ (sym eq0)
-             ... | 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₁ | record { eq = eq0 }  | _ = refl-≤≡ (sym eq0)
-             ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ | _ | _ = ⊥-elim (nat-≡< (sym b) (subst (λ k → _ < k ) (sym b₁) a<sa) )
-             ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c | _ | _ = ⊥-elim (nat-≡< (sym b) (<-trans a<sa c))
-             ... | tri> ¬a ¬b c | tri< a ¬b₁ ¬c | _ | _ = ⊥-elim (nat-≤> a (<-transʳ  c a<sa ) )
-             ... | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c | record { eq = eq0 } | record { eq = eq1 } with is-B (Q←F fa (fromℕ< c))   
-             ... | yes  isb = refl-≤≡ (sym eq0)
-             ... | no  nisb = refl-≤≡ (sym eq0)
-             lem01 (suc i) | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ | record { eq = eq0 } | record { eq = eq1 } 
+             lem01 zero | tri> ¬a ¬b c with is-B (Q←F fa (fromℕ< c)) | is-B (Q←F fa ( fromℕ< {0} 0<fa )) 
+             ... | yes isb1 | yes isb0  = s≤s z≤n
+             ... | yes isb1 | no  nisb0 = z≤n
+             ... | no nisb1 | yes isb0  = refl-≤≡ (sym lem14 ) where
+                  lem14 : count-B 0 ≡ 1
+                  lem14 with is-B (Q←F fa ( fromℕ< {0} 0<fa ))
+                  ... | yes isb = refl
+                  ... | 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₁ = ⊥-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 ?)
+             ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = ⊥-elim (nat-≡< (sym b) (subst (λ k → _ < k ) (sym b₁) a<sa) )
+             ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c = ⊥-elim (nat-≡< (sym b) (<-trans a<sa c))
+             ... | tri> ¬a ¬b c | tri< a ¬b₁ ¬c = ⊥-elim (nat-≤> a (<-transʳ  c a<sa ) )
+             ... | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c with is-B (Q←F fa (fromℕ< c))   
+             ... | yes  isb = refl-≤≡ (sym ?)
+             ... | no  nisb = refl-≤≡ (sym ?)
+             lem01 (suc i) | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ 
                   with is-B (Q←F fa (fromℕ< c)) | is-B (Q←F fa (fromℕ< c₁)) 
-             ... | yes  isb0 | yes  isb1 = ≤-trans (refl-≤≡ (sym eq0)) a≤sa
-             ... | yes  isb0 | no  nisb1 = refl-≤≡ (sym eq0)
-             ... | no  nisb0 | yes  isb1 = ≤-trans (refl-≤≡ (sym eq0)) a≤sa
-             ... | no  nisb0 | no  nisb1 = refl-≤≡ (sym eq0)
+             ... | yes  isb0 | yes  isb1 = ≤-trans (refl-≤≡ (sym ?)) a≤sa
+             ... | yes  isb0 | no  nisb1 = refl-≤≡ (sym ?)
+             ... | no  nisb0 | yes  isb1 = ≤-trans (refl-≤≡ (sym ?)) a≤sa
+             ... | no  nisb0 | no  nisb1 = refl-≤≡ (sym ?)
 
     lem31 : (b : B) → 0 < count-B (toℕ (F←Q fa (f b)))
     lem31 b = lem32 (toℕ (F←Q fa (f b))) refl where
@@ -679,10 +666,10 @@
               Q←F fa ( fromℕ< (fin<n _) )  ≡⟨ cong (λ k → Q←F fa k) (fromℕ<-cong _ _ eq (fin<n _) 0<fa) ⟩
               Q←F fa ( fromℕ< {0} 0<fa ) ∎ where
                 open ≡-Reasoning
-        lem32 (suc i) eq with <-cmp (finite fa) (suc i) | inspect count-B (suc i) 
-        ... | tri< a ¬b ¬c | _ = ⊥-elim ( nat-≡< eq (<-trans (fin<n _) a) )
-        ... | tri≈ ¬a eq1 ¬c | _ = ⊥-elim ( nat-≡< eq (subst (λ k → toℕ (F←Q fa (f b)) < k ) eq1 (fin<n _)))
-        ... | tri> ¬a ¬b c | record { eq = eq1 } with is-B (Q←F fa (fromℕ< c))   
+        lem32 (suc i) eq with <-cmp (finite fa) (suc i) 
+        ... | tri< a ¬b ¬c = ⊥-elim ( nat-≡< eq (<-trans (fin<n _) a) )
+        ... | tri≈ ¬a eq1 ¬c = ⊥-elim ( nat-≡< eq (subst (λ k → toℕ (F←Q fa (f b)) < k ) eq1 (fin<n _)))
+        ... | tri> ¬a ¬b c with is-B (Q←F fa (fromℕ< c))   
         ... | yes isb = s≤s z≤n 
         ... | no nisb = ⊥-elim ( nisb record { a = b ; fa=c = lem33 } ) where
             lem33 : f b ≡ Q←F fa ( fromℕ< c)
@@ -713,17 +700,17 @@
             lem20 zero (suc j) i<j i<fa j<fa bi bj with <-cmp (finite fa) (suc j) 
             ... | tri< a ¬b ¬c = ⊥-elim (¬c j<fa)
             ... | tri≈ ¬a b ¬c = ⊥-elim (¬c j<fa)
-            ... | tri> ¬a ¬b c with  is-B (Q←F fa ( fromℕ< 0<fa )) | inspect count-B 0 | is-B (Q←F fa (fromℕ< c)) | inspect count-B (suc j)
-            ... | no nisc  | _ | _ | _ = ⊥-elim (nisc record { a = Is.a bi ; fa=c = lem26 } ) where
+            ... | tri> ¬a ¬b c with  is-B (Q←F fa ( fromℕ< 0<fa )) |  is-B (Q←F fa (fromℕ< c)) 
+            ... | no nisc  | _ = ⊥-elim (nisc record { a = Is.a bi ; fa=c = lem26 } ) where
                  lem26 : f (Is.a bi) ≡ Q←F fa (fromℕ< 0<fa)
                  lem26 = trans (Is.fa=c bi) (cong (Q←F fa) (fromℕ<-cong _ _ refl i<fa 0<fa) )
-            ... |  yes _ | _ | no nisc | _  = ⊥-elim (nisc record { a = Is.a bj ; fa=c = lem26 } ) where
+            ... |  yes _ | no nisc = ⊥-elim (nisc record { a = Is.a bj ; fa=c = lem26 } ) where
                  lem26 : f (Is.a bj) ≡ Q←F fa (fromℕ< c)
                  lem26 = trans (Is.fa=c bj) (cong (Q←F fa) (fromℕ<-cong _ _ refl j<fa c) )
-            ... | yes _ | record { eq = eq1 } | yes _ | record { eq = eq2 } = lem25 where
+            ... | yes _ |  yes _ = lem25 where
                  lem25 : 2 ≤ suc (count-B j)
                  lem25 = begin
-                    2 ≡⟨ cong suc (sym eq1) ⟩
+                    2 ≡⟨ cong suc (sym ?) ⟩
                     suc (count-B 0) ≤⟨ s≤s (count-B-mono {0} {j} z≤n) ⟩
                     suc (count-B j)  ∎ where open ≤-Reasoning
             lem20 (suc i) zero () i<fa j<fa bi bj 
@@ -736,9 +723,9 @@
                  lem23 with <-cmp (finite fa) (suc j)
                  ... | tri< a ¬b ¬c = ⊥-elim (¬c j<fa)
                  ... | tri≈ ¬a b ¬c = ⊥-elim (¬c j<fa)
-                 ... | tri> ¬a ¬b c with is-B (Q←F fa (fromℕ< c)) | inspect count-B (suc j)
-                 ... | yes _ | record { eq = eq1 } = refl
-                 ... | no nisa | _ = ⊥-elim ( nisa record { a = Is.a bj ; fa=c = lem26 } ) where
+                 ... | tri> ¬a ¬b c with is-B (Q←F fa (fromℕ< c)) 
+                 ... | yes _ = refl
+                 ... | no nisa = ⊥-elim ( nisa record { a = Is.a bj ; fa=c = lem26 } ) where
                      lem26 : f (Is.a bj) ≡ Q←F fa (fromℕ< c)
                      lem26 = trans (Is.fa=c bj) (cong (Q←F fa) (fromℕ<-cong _ _ refl j<fa c) )
                  lem21 : count-B (suc i) < count-B (suc j)
@@ -755,10 +742,10 @@
             ... | tri> ¬a ¬b c₁ = ⊥-elim (nat-≡< (sym eq) ( lem20 j i c₁ j<fa i<fa bj bi ))
 
         lem09 : (i j : ℕ) →  suc n ≤ j → j ≡ count-B i →  CountB n
-        lem09 0 (suc j) (s≤s le) eq with is-B (Q←F fa (fromℕ< {0} 0<fa )) | inspect count-B 0
-        ... | no nisb | record { eq = eq1 } = ⊥-elim ( nat-≡< (sym eq) (s≤s z≤n) )
-        ... | yes isb | record { eq = eq1 } with ≤-∨ (s≤s le)
-        ... | case1 eq2 = record { b = Is.a isb ; cb = 0 ; b=cn = lem10 ; cb=n = trans eq1 (sym (trans eq2 eq))
+        lem09 0 (suc j) (s≤s le) eq with is-B (Q←F fa (fromℕ< {0} 0<fa )) 
+        ... | no nisb = ⊥-elim ( nat-≡< (sym eq) (s≤s z≤n) )
+        ... | yes isb with ≤-∨ (s≤s le)
+        ... | case1 eq2 = record { b = Is.a isb ; cb = 0 ; b=cn = lem10 ; cb=n = trans ? (sym (trans eq2 eq))
                 ; cb-inject = λ cb1 c1<fa b1 eq → lem06 0 cb1 0<fa c1<fa isb b1 eq } where
              lem10 : 0 ≡ toℕ (F←Q fa (f (Is.a isb)))
              lem10 = begin
@@ -767,13 +754,13 @@
                 toℕ (F←Q fa (Q←F fa (fromℕ< {0} 0<fa )))  ≡⟨ cong (λ k → toℕ ((F←Q fa k))) (sym (Is.fa=c isb)) ⟩
                 toℕ (F←Q fa (f (Is.a isb))) ∎ where open ≡-Reasoning
         ... | case2 (s≤s lt) = ⊥-elim ( nat-≡< (sym eq) (s≤s (<-transʳ z≤n lt)  ))
-        lem09 (suc i) (suc j) (s≤s le) eq with <-cmp (finite fa) (suc i) | inspect count-B (suc i)
-        ... | tri< a ¬b ¬c | _ = lem09 i (suc j) (s≤s le) eq
-        ... | tri≈ ¬a b ¬c | _ = lem09 i (suc j) (s≤s le) eq
-        ... | tri> ¬a ¬b c | record { eq = eq1 } with is-B (Q←F fa (fromℕ< c))
+        lem09 (suc i) (suc j) (s≤s le) eq with <-cmp (finite fa) (suc i) 
+        ... | tri< a ¬b ¬c = lem09 i (suc j) (s≤s le) eq
+        ... | tri≈ ¬a b ¬c = lem09 i (suc j) (s≤s le) eq
+        ... | tri> ¬a ¬b c with is-B (Q←F fa (fromℕ< c))
         ... | no nisb = lem09 i (suc j) (s≤s le) eq
         ... | yes isb with ≤-∨ (s≤s le)
-        ... | case1 eq2 = record { b = Is.a isb ; cb = suc i ;  b=cn = lem11 ; cb=n = trans eq1 (sym (trans eq2 eq ))
+        ... | case1 eq2 = record { b = Is.a isb ; cb = suc i ;  b=cn = lem11 ; cb=n = trans ? (sym (trans eq2 eq ))
                 ; cb-inject = λ cb1 c1<fa b1 eq → lem06 (suc i) cb1 c c1<fa isb b1 eq } where
               lem11 : suc i ≡ toℕ (F←Q fa (f (Is.a isb)))
               lem11 = begin
diff -r 093e386c10a2 -r c298981108c1 automaton-in-agda/src/logic.agda
--- a/automaton-in-agda/src/logic.agda	Thu Aug 10 09:59:47 2023 +0900
+++ b/automaton-in-agda/src/logic.agda	Sun Sep 24 11:32:01 2023 +0900
@@ -1,3 +1,5 @@
+{-# OPTIONS --cubical-compatible --safe #-}
+
 module logic where
 
 open import Level
@@ -10,10 +12,6 @@
     true : Bool
     false : Bool
 
-data Two : Set where
-   i0 : Two
-   i1 : Two
-
 record  _∧_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n ⊔ m) where
    constructor ⟪_,_⟫
    field
@@ -27,13 +25,6 @@
 _⇔_ : {n m : Level } → ( A : Set n ) ( B : Set m )  → Set (n ⊔ m)
 _⇔_ A B =  ( A → B ) ∧ ( B → A )
 
-∧-exch : {n m : Level} {A  : Set n} { B : Set m } → A ∧ B → B ∧ A
-∧-exch p = ⟪ _∧_.proj2 p , _∧_.proj1 p ⟫
-
-∨-exch : {n m : Level} {A  : Set n} { B : Set m } → A ∨ B → B ∨ A
-∨-exch (case1 x) = case2 x
-∨-exch (case2 x) = case1 x
-
 contra-position : {n m : Level } {A : Set n} {B : Set m} → (A → B) → ¬ B → ¬ A
 contra-position {n} {m} {A} {B}  f ¬b a = ¬b ( f a )
 
@@ -47,10 +38,6 @@
 de-morgan {n} {A} {B} and (case1 ¬A) = ⊥-elim ( ¬A ( _∧_.proj1 and ))
 de-morgan {n} {A} {B} and (case2 ¬B) = ⊥-elim ( ¬B ( _∧_.proj2 and ))
 
-de-morgan∨ : {n  : Level } {A B : Set n} →  A ∨ B  → ¬ ( (¬ A ) ∧ (¬ B ) )
-de-morgan∨ {n} {A} {B} (case1 a) and = ⊥-elim (  _∧_.proj1 and a )
-de-morgan∨ {n} {A} {B} (case2 b) and = ⊥-elim (  _∧_.proj2 and b )
-
 dont-or :　{n m : Level} {A  : Set n} { B : Set m } →  A ∨ B → ¬ A → B
 dont-or {A} {B} (case1 a) ¬A = ⊥-elim ( ¬A a )
 dont-or {A} {B} (case2 b) ¬A = b
@@ -71,7 +58,7 @@
 false \/ false = false
 _ \/ _ = true
 
-not : Bool → Bool 
+not_ : Bool → Bool 
 not true = false
 not false = true 
 
@@ -80,11 +67,10 @@
 false <=> false = true
 _ <=> _ = false
 
-open import Relation.Binary.PropositionalEquality
+infixr  130 _\/_
+infixr  140 _/\_
 
-not-not-bool : { b : Bool } → not (not b) ≡ b
-not-not-bool {true} = refl
-not-not-bool {false} = refl
+open import Relation.Binary.PropositionalEquality
 
 record Bijection {n m : Level} (R : Set n) (S : Set m) : Set (n Level.⊔ m)  where
    field
@@ -97,13 +83,14 @@
 injection R S f = (x y : R) → f x ≡ f y → x ≡ y
 
 
+not-not-bool : { b : Bool } → not (not b) ≡ b
+not-not-bool {true} = refl
+not-not-bool {false} = refl
+
 ¬t=f : (t : Bool ) → ¬ ( not t ≡ t) 
 ¬t=f true ()
 ¬t=f false ()
 
-infixr  130 _\/_
-infixr  140 _/\_
-
 ≡-Bool-func : {A B : Bool } → ( A ≡ true → B ≡ true ) → ( B ≡ true → A ≡ true ) → A ≡ B
 ≡-Bool-func {true} {true} a→b b→a = refl
 ≡-Bool-func {false} {true} a→b b→a with b→a refl
@@ -130,89 +117,57 @@
 ¬-bool refl ()
 
 lemma-∧-0 : {a b : Bool} → a /\ b ≡ true → a ≡ false → ⊥
-lemma-∧-0 {true} {true} refl ()
 lemma-∧-0 {true} {false} ()
 lemma-∧-0 {false} {true} ()
 lemma-∧-0 {false} {false} ()
+lemma-∧-0 {true} {true} eq1 ()
 
 lemma-∧-1 : {a b : Bool} → a /\ b ≡ true → b ≡ false → ⊥
-lemma-∧-1 {true} {true} refl ()
 lemma-∧-1 {true} {false} ()
 lemma-∧-1 {false} {true} ()
 lemma-∧-1 {false} {false} ()
+lemma-∧-1 {true} {true} eq1 ()
 
 bool-and-tt : {a b : Bool} → a ≡ true → b ≡ true → ( a /\ b ) ≡ true
 bool-and-tt refl refl = refl
 
 bool-∧→tt-0 : {a b : Bool} → ( a /\ b ) ≡ true → a ≡ true 
-bool-∧→tt-0 {true} {true} refl = refl
+bool-∧→tt-0 {true} {true} eq =  refl
 bool-∧→tt-0 {false} {_} ()
 
 bool-∧→tt-1 : {a b : Bool} → ( a /\ b ) ≡ true → b ≡ true 
-bool-∧→tt-1 {true} {true} refl = refl
+bool-∧→tt-1 {true} {true} eq = refl
 bool-∧→tt-1 {true} {false} ()
 bool-∧→tt-1 {false} {false} ()
 
 bool-or-1 : {a b : Bool} → a ≡ false → ( a \/ b ) ≡ b 
-bool-or-1 {false} {true} refl = refl
-bool-or-1 {false} {false} refl = refl
+bool-or-1 {false} {true} eq = refl
+bool-or-1 {false} {false} eq = refl
 bool-or-2 : {a b : Bool} → b ≡ false → (a \/ b ) ≡ a 
-bool-or-2 {true} {false} refl = refl
-bool-or-2 {false} {false} refl = refl
+bool-or-2 {true} {false} eq = refl
+bool-or-2 {false} {false} eq = refl
 
 bool-or-3 : {a : Bool} → ( a \/ true ) ≡ true 
 bool-or-3 {true} = refl
 bool-or-3 {false} = refl
 
 bool-or-31 : {a b : Bool} → b ≡ true  → ( a \/ b ) ≡ true 
-bool-or-31 {true} {true} refl = refl
-bool-or-31 {false} {true} refl = refl
+bool-or-31 {true} {true} eq = refl
+bool-or-31 {false} {true} eq = refl
 
 bool-or-4 : {a : Bool} → ( true \/ a ) ≡ true 
 bool-or-4 {true} = refl
 bool-or-4 {false} = refl
 
 bool-or-41 : {a b : Bool} → a ≡ true  → ( a \/ b ) ≡ true 
-bool-or-41 {true} {b} refl = refl
+bool-or-41 {true} {b} eq = refl
 
 bool-and-1 : {a b : Bool} →  a ≡ false → (a /\ b ) ≡ false
-bool-and-1 {false} {b} refl = refl
+bool-and-1 {false} {b} eq = refl
 bool-and-2 : {a b : Bool} →  b ≡ false → (a /\ b ) ≡ false
-bool-and-2 {true} {false} refl = refl
-bool-and-2 {false} {false} refl = refl
+bool-and-2 {true} {false} eq = refl
+bool-and-2 {false} {false} eq = refl
+bool-and-2 {true} {true} ()
+bool-and-2 {false} {true} ()
 
 
-open import Data.Nat
-open import Data.Nat.Properties
-
-_≥b_ : ( x y : ℕ) → Bool
-x ≥b y with <-cmp x y
-... | tri< a ¬b ¬c = false
-... | tri≈ ¬a b ¬c = true
-... | tri> ¬a ¬b c = true
-
-_>b_ : ( x y : ℕ) → Bool
-x >b y with <-cmp x y
-... | tri< a ¬b ¬c = false
-... | tri≈ ¬a b ¬c = false
-... | tri> ¬a ¬b c = true
-
-_≤b_ : ( x y : ℕ) → Bool
-x ≤b y  = y ≥b x
-
-_<b_ : ( x y : ℕ) → Bool
-x <b y  = y >b x
-
-open import Relation.Binary.PropositionalEquality
-
-¬i0≡i1 : ¬ ( i0 ≡ i1 )
-¬i0≡i1 ()
-
-¬i0→i1 : {x : Two} → ¬ (x ≡ i0 ) → x ≡ i1 
-¬i0→i1 {i0} ne = ⊥-elim ( ne refl )
-¬i0→i1 {i1} ne = refl
-
-¬i1→i0 : {x : Two} → ¬ (x ≡ i1 ) → x ≡ i0 
-¬i1→i0 {i0} ne = refl
-¬i1→i0 {i1} ne = ⊥-elim ( ne refl )
-
diff -r 093e386c10a2 -r c298981108c1 automaton-in-agda/src/nat.agda
--- a/automaton-in-agda/src/nat.agda	Thu Aug 10 09:59:47 2023 +0900
+++ b/automaton-in-agda/src/nat.agda	Sun Sep 24 11:32:01 2023 +0900
@@ -1,4 +1,5 @@
-{-# OPTIONS --allow-unsolved-metas #-}
+{-# OPTIONS --cubical-compatible --safe #-}
+
 module nat where
 
 open import Data.Nat 
@@ -104,15 +105,15 @@
 div2-eq : (x : ℕ ) → div2-rev ( div2 x ) ≡ x
 div2-eq zero = refl
 div2-eq (suc zero) = refl
-div2-eq (suc (suc x)) with div2 x | inspect div2 x 
-... | ⟪ x1 , true ⟫ | record { eq = eq1 } = begin -- eq1 : div2 x ≡ ⟪ x1 , true ⟫
+div2-eq (suc (suc x)) with div2 x in eq1 
+... | ⟪ x1 , true ⟫ = begin -- eq1 : div2 x ≡ ⟪ x1 , true ⟫
      div2-rev ⟪ suc x1 , true ⟫ ≡⟨⟩
      suc (suc (x1 + suc x1)) ≡⟨ cong (λ k → suc (suc k )) (+-comm x1  _ ) ⟩
      suc (suc (suc (x1 + x1))) ≡⟨⟩    
      suc (suc (div2-rev ⟪ x1 , true ⟫)) ≡⟨ cong (λ k → suc (suc (div2-rev k ))) (sym eq1) ⟩ 
      suc (suc (div2-rev (div2 x)))      ≡⟨ cong (λ k → suc (suc k)) (div2-eq x) ⟩ 
      suc (suc x) ∎  where open ≡-Reasoning
-... | ⟪ x1 , false ⟫ | record { eq = eq1 } = begin
+... | ⟪ x1 , false ⟫ = begin
      div2-rev ⟪ suc x1 , false ⟫ ≡⟨⟩
      suc (x1 + suc x1) ≡⟨ cong (λ k → (suc k )) (+-comm x1  _ ) ⟩
      suc (suc (x1 + x1)) ≡⟨⟩    
@@ -138,6 +139,40 @@
 
 _-_ = minus
 
+sn-m=sn-m : {m n : ℕ } →  m ≤ n → suc n - m ≡ suc ( n - m )
+sn-m=sn-m {0} {n} z≤n = refl
+sn-m=sn-m {suc m} {suc n} (s≤s m<n) = sn-m=sn-m m<n
+
+si-sn=i-n : {i n : ℕ } → n < i  → suc (i - suc n) ≡ (i - n)
+si-sn=i-n {i} {n} n<i = begin
+   suc (i - suc n) ≡⟨ sym (sn-m=sn-m n<i )  ⟩
+   suc i - suc n ≡⟨⟩
+   i - n
+   ∎  where
+      open ≡-Reasoning
+
+refl-≤s : {x : ℕ } → x ≤ suc x
+refl-≤s {zero} = z≤n
+refl-≤s {suc x} = s≤s (refl-≤s {x})
+
+a≤sa = refl-≤s
+
+n-m<n : (n m : ℕ ) →  n - m ≤ n
+n-m<n zero zero = z≤n
+n-m<n (suc n) zero = s≤s (n-m<n n zero)
+n-m<n zero (suc m) = z≤n
+n-m<n (suc n) (suc m) = ≤-trans (n-m<n n m ) refl-≤s
+
+n-n-m=m : {m n : ℕ } → m ≤ n  → m ≡ (n - (n - m))
+n-n-m=m {0} {zero} z≤n = refl
+n-n-m=m {0} {suc n} z≤n = n-n-m=m {0} {n} z≤n
+n-n-m=m {suc m} {suc n} (s≤s m≤n) = sym ( begin
+   suc n - ( n - m )    ≡⟨ sn-m=sn-m (n-m<n  n m) ⟩
+   suc (n - ( n - m ))  ≡⟨ cong (λ k → suc k ) (sym (n-n-m=m m≤n)) ⟩
+   suc m
+   ∎  ) where
+      open ≡-Reasoning
+
 m+= : {i j  m : ℕ } → m + i ≡ m + j → i ≡ j
 m+= {i} {j} {zero} refl = refl
 m+= {i} {j} {suc m} eq = m+= {i} {j} {m} ( cong (λ k → pred k ) eq )
@@ -238,12 +273,6 @@
 ... | 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})
@@ -696,15 +725,15 @@
           m ∎  where open ≤-Reasoning  
 
 0<factor : { m k : ℕ } → k > 0 → m > 0 →  (d :  Dividable k m ) → Dividable.factor d > 0
-0<factor {m} {k} k>0 m>0 d with Dividable.factor d | inspect Dividable.factor d 
-... | zero | record { eq = eq1 } = ⊥-elim ( nat-≡< ff1 m>0 ) where
+0<factor {m} {k} k>0 m>0 d with Dividable.factor d in eq1 
+... | zero = ⊥-elim ( nat-≡< ff1 m>0 ) where
     ff1 : 0 ≡ m 
     ff1 = begin
           0 ≡⟨⟩
           0 * k + 0 ≡⟨ cong  (λ j → j * k + 0) (sym eq1) ⟩
           Dividable.factor d * k + 0 ≡⟨ Dividable.is-factor d  ⟩
           m ∎  where open ≡-Reasoning  
-... | suc t | _ = s≤s z≤n 
+... | suc t = s≤s z≤n 
 
 div→k≤m : { m k : ℕ } → k > 1 → m > 0 →  Dividable k m → m ≥ k
 div→k≤m {m} {k} k>1 m>0 d with <-cmp m k
diff -r 093e386c10a2 -r c298981108c1 automaton-in-agda/src/non-regular.agda
--- a/automaton-in-agda/src/non-regular.agda	Thu Aug 10 09:59:47 2023 +0900
+++ b/automaton-in-agda/src/non-regular.agda	Sun Sep 24 11:32:01 2023 +0900
@@ -312,7 +312,21 @@
                     count1 x + count1 y + count1 z ∎ where open ≡-Reasoning
                -- this takes very long time to check and needs 10GB
                bb22 : count0 y ≡ count1 y
-               bb22 = ?
+               bb22 = begin
+                    count0 y ≡⟨ sym ( +-cancelʳ-≡  {count1 z  + count0 x + count0 y + count0 z} (count1 y) (count0 y)  (+-cancelˡ-≡ (count1 x + count1 y) (
+                       begin 
+                       count1 x + count1 y + (count1 y + (count1 z + count0 x + count0 y + count0 z))  ≡⟨ solve +-0-monoid  ⟩
+                       (count1 x + count1 y + count1 y + count1 z)  + (count0 x + count0 y + count0 z) ≡⟨ sym (cong₂ _+_ nn21 (sym nn20)) ⟩
+                       (count0 x + count0 y + count0 y + count0 z)  + (count1 x + count1 y + count1 z) ≡⟨  +-comm _ (count1 x + count1 y + count1 z) ⟩
+                       (count1 x + count1 y + count1 z) + (count0 x + count0 y + count0 y + count0 z)    ≡⟨  solve +-0-monoid ⟩
+                        count1 x + count1 y + (count1 z + (count0 x + count0 y)) + count0 y + count0 z    
+                            ≡⟨  cong (λ k → count1 x + count1 y + (count1 z + k) + count0 y + count0 z) (+-comm (count0 x) _) ⟩
+                        count1 x + count1 y + (count1 z + (count0 y + count0 x)) + count0 y + count0 z    ≡⟨ solve +-0-monoid ⟩
+                        count1 x + count1 y + ((count1 z + count0 y) + count0 x) + count0 y + count0 z    
+                            ≡⟨  cong (λ k → count1 x + count1 y + (k + count0 x) + count0 y + count0 z    ) (+-comm (count1 z) _) ⟩
+                        count1 x + count1 y + (count0 y + count1 z + count0 x) + count0 y + count0 z    ≡⟨  solve +-0-monoid ⟩
+                        count1 x + count1 y + (count0 y + (count1 z + count0 x + count0 y + count0 z))    ∎ ))) ⟩
+                    count1 y ∎ where open ≡-Reasoning
                --
                --  y contains i0 and i1 , so we have i1 → i0 transition in y ++ y
                --
diff -r 093e386c10a2 -r c298981108c1 automaton-in-agda/src/pumping.agda
--- a/automaton-in-agda/src/pumping.agda	Thu Aug 10 09:59:47 2023 +0900
+++ b/automaton-in-agda/src/pumping.agda	Sun Sep 24 11:32:01 2023 +0900
@@ -65,7 +65,7 @@
 
 open Data.Maybe
 
-open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
+-- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
 open import Relation.Binary.Definitions
 open import Data.Unit using (⊤ ; tt)
 open import Data.Nat.Properties
diff -r 093e386c10a2 -r c298981108c1 automaton-in-agda/src/regular-star.agda
--- a/automaton-in-agda/src/regular-star.agda	Thu Aug 10 09:59:47 2023 +0900
+++ b/automaton-in-agda/src/regular-star.agda	Sun Sep 24 11:32:01 2023 +0900
@@ -74,7 +74,7 @@
     open Found
 
     closed-in-star← : contain (M-Star A ) x ≡ true → Star (contain A)  x ≡ true
-    closed-in-star← C with subset-construction-lemma← (SNFA-exist A ) NFA {!!} x C 
+    closed-in-star← C with subset-construction-lemma← (SNFA-exist A ) NFA (Star-NFA-start A) x C 
     ... | CC = {!!}