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

diff -r dfaf230f7b9a -r af8f630b7e60 automaton-in-agda/src/automaton-ex.agda
--- a/automaton-in-agda/src/automaton-ex.agda	Sun Sep 24 13:20:31 2023 +0900
+++ b/automaton-in-agda/src/automaton-ex.agda	Sun Sep 24 18:02:04 2023 +0900
@@ -1,4 +1,5 @@
-{-# OPTIONS --allow-unsolved-metas #-}
+{-# OPTIONS --cubical-compatible --safe #-}
+
 module automaton-ex where
 
 open import Data.Nat
@@ -102,6 +103,24 @@
 test11 : count-chars (  i1  ∷ i1  ∷ i0  ∷ []  ) i0 ≡ 1
 test11 = refl
 
+_≥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
+
 ex1_4a : (x : List In2) → Bool
 ex1_4a x =  ( count-chars x i0 ≥b 3 ) /\ ( count-chars x i1 ≥b 2 )
 
@@ -138,5 +157,5 @@
 am14a-tr' a00 i0 = a10
 am14a-tr' _ _ = a10
 
-am14a'  :  Automaton  am14s  In2
-am14a'  =  record {  δ = am14a-tr' ; aend = λ x → {!!} }
+-- am14a'  :  Automaton  am14s  In2
+-- am14a'  =  record {  δ = am14a-tr' ; aend = λ x → {!!} }
diff -r dfaf230f7b9a -r af8f630b7e60 automaton-in-agda/src/cfg.agda
--- a/automaton-in-agda/src/cfg.agda	Sun Sep 24 13:20:31 2023 +0900
+++ b/automaton-in-agda/src/cfg.agda	Sun Sep 24 18:02:04 2023 +0900
@@ -1,3 +1,5 @@
+{-# OPTIONS --cubical-compatible #-}
+
 module cfg where
 
 open import Level renaming ( suc to succ ; zero to Zero )
diff -r dfaf230f7b9a -r af8f630b7e60 automaton-in-agda/src/cfg1.agda
--- a/automaton-in-agda/src/cfg1.agda	Sun Sep 24 13:20:31 2023 +0900
+++ b/automaton-in-agda/src/cfg1.agda	Sun Sep 24 18:02:04 2023 +0900
@@ -1,3 +1,5 @@
+{-# OPTIONS --cubical-compatible  #-}
+
 module cfg1 where
 
 open import Level renaming ( suc to succ ; zero to Zero )
@@ -35,7 +37,7 @@
    field
       cfg : Symbol → Body Symbol 
       top : Symbol
-      eq? : Symbol → Symbol → Bool
+      eqP : Symbol → Symbol → Bool
       typeof : Symbol →  Node Symbol
 
 infixr  80 _｜_
@@ -64,11 +66,11 @@
 cfg-language1 :  {Symbol  : Set} → CFGGrammer Symbol   → Seq Symbol  →  List Symbol → Bool
 cfg-language1 cg Error x = false
 cfg-language1 cg (S ， seq) x with typeof cg S
-cfg-language1 cg (_ ， seq) (x' ∷ t) | T x =  eq? cg x x' /\ cfg-language1 cg seq t
+cfg-language1 cg (_ ， seq) (x' ∷ t) | T x =  eqP cg x x' /\ cfg-language1 cg seq t
 cfg-language1 cg (_ ， seq) [] | T x = false
 cfg-language1 cg (_ ， seq) x | N nonTerminal = split (cfg-language0 cg (cfg cg nonTerminal) )(cfg-language1 cg seq ) x
 cfg-language1 cg (S ．) x with typeof cg S
-cfg-language1 cg (_ ．) (x' ∷ []) | T x =  eq? cg x x'
+cfg-language1 cg (_ ．) (x' ∷ []) | T x =  eqP cg x x'
 cfg-language1 cg (_ ．) _ | T x = false
 cfg-language1 cg (_ ．) x | N nonTerminal = cfg-language0 cg (cfg cg nonTerminal) x
 
@@ -117,7 +119,7 @@
 IFGrammer = record {
       cfg = cfg'
     ; top = statement
-    ; eq? = token-eq?
+    ; eqP = token-eq?
     ; typeof = typeof-IFG 
    } where
      cfg' : IFToken → Body IFToken 
@@ -168,7 +170,7 @@
 E1Grammer = record {
       cfg = cfgE
     ; top = expr
-    ; eq? = E1-token-eq?
+    ; eqP = E1-token-eq?
     ; typeof = typeof-E1
    } where
      cfgE : E1Token → Body E1Token
@@ -286,7 +288,7 @@
 pda→cfg pda = record {
       cfg = {!!}
     ; top = {!!}
-    ; eq? = {!!}
+    ; eqP = {!!}
     ; typeof = {!!}
    } 
 
@@ -299,6 +301,6 @@
    field
       cdg : Seq Symbol  → Body Symbol 
       top : Symbol
-      eq? : Symbol → Symbol → Bool
+      eqP : Symbol → Symbol → Bool
       typeof : Symbol →  Node Symbol
 
diff -r dfaf230f7b9a -r af8f630b7e60 automaton-in-agda/src/chap0.agda
--- a/automaton-in-agda/src/chap0.agda	Sun Sep 24 13:20:31 2023 +0900
+++ b/automaton-in-agda/src/chap0.agda	Sun Sep 24 18:02:04 2023 +0900
@@ -1,3 +1,5 @@
+{-# OPTIONS --cubical-compatible --safe #-}
+
 module chap0 where
 
 open import Data.List
@@ -149,7 +151,7 @@
     indirect :  ( z : V  ) -> E x z  →  connected {V} E z y → connected E x y
 
 lemma1 : connected ( edge graph012a ) 1 2
-lemma1 = direct refl  where
+lemma1 = direct refl  
 
 lemma1-2 : connected ( edge graph012a ) 1 3
 lemma1-2 = indirect 2 refl (direct refl ) 
@@ -188,7 +190,7 @@
 even2 : (n : ℕ ) → n % 2 ≡ 0 → (n + 2) % 2 ≡ 0 
 even2 0 refl = refl
 even2 1 () 
-even2 (suc (suc n)) eq = trans ([a+n]%n≡a%n n _) eq -- [a+n]%n≡a%n : ∀ a n → (a + suc n) % suc n ≡ a % suc n
+even2 (suc (suc n)) eq = ? -- trans ([a+n]%n≡a%n n _) eq -- [a+n]%n≡a%n : ∀ a n → (a + suc n) % suc n ≡ a % suc n
 
 sum-of-dgree : ( g : List ( ℕ × ℕ )) → ℕ
 sum-of-dgree [] = 0
@@ -202,7 +204,7 @@
        (2 + sum-of-dgree t ) % 2       
     ≡⟨ cong ( λ k → k % 2 ) ( +-comm 2 (sum-of-dgree t) )  ⟩
        (sum-of-dgree t + 2) % 2 
-    ≡⟨ [a+n]%n≡a%n (sum-of-dgree t) _ ⟩
+    ≡⟨ ? ⟩ -- [a+n]%n≡a%n (sum-of-dgree t) _ ⟩
        sum-of-dgree t % 2
     ≡⟨ dgree-even t ⟩
        0
diff -r dfaf230f7b9a -r af8f630b7e60 automaton-in-agda/src/derive.agda
--- a/automaton-in-agda/src/derive.agda	Sun Sep 24 13:20:31 2023 +0900
+++ b/automaton-in-agda/src/derive.agda	Sun Sep 24 18:02:04 2023 +0900
@@ -5,6 +5,7 @@
 open import Data.List hiding ( [_] )
 open import Data.Empty 
 open import finiteSet
+open import finiteFunc
 open import fin
 
 module derive ( Σ : Set) ( fin : FiniteSet Σ ) ( eq? : (x y : Σ) → Dec (x ≡ y)) where
@@ -74,7 +75,7 @@
 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
 
 -- open import nfa
-open import Data.Nat
+open import Data.Nat hiding (eq?)
 open import Data.Nat.Properties hiding ( eq? )
 open import nat
 open import finiteSetUtil
@@ -261,10 +262,10 @@
    sb01 : (isb : ISB (r & r₁)) → ( ISB.is-sub isb ≡ sub&1 _ _ _ ? ) 
         ∨ ( ISB.is-sub isb ≡ sub&2 _ _ _ ? )
         ∨ ( ISB.is-sub isb ≡ subst (λ k → SB ? ?) ? (sub&& _ _ _ ? ? ))
-   sb01 isb with ISB.is-sub isb | inspect ISB.is-sub isb 
-   ... | sub&1 .r .r₁ .(ISB.s isb) t | record { eq = refl } = case1 refl
-   ... | sub&2 .r .r₁ .(ISB.s isb) t | record { eq = refl } = case2 (case1 refl)
-   ... | sub&& .r .r₁ z x t | record { eq = refl } = case2 (case2 refl)
+   sb01 isb with ISB.is-sub isb in eq
+   ... | sub&1 .r .r₁ .(ISB.s isb) t = case1 ?
+   ... | sub&2 .r .r₁ .(ISB.s isb) t = case2 (case1 ?)
+   ... | sub&& .r .r₁ z x t = case2 (case2 ?)
    sb00 : ISB r → Bool
    sb00 record { s = s ; is-sub = is-sub } = f record { s = s ; is-sub = sub&1 _ _ _ is-sub }
 sbempty? (r || r₁) f with f record { s = r ; is-sub = sub|1 ? } | f record { s = r₁ ; is-sub = sub|2 ? }
diff -r dfaf230f7b9a -r af8f630b7e60 automaton-in-agda/src/deriveUtil.agda
--- a/automaton-in-agda/src/deriveUtil.agda	Sun Sep 24 13:20:31 2023 +0900
+++ b/automaton-in-agda/src/deriveUtil.agda	Sun Sep 24 18:02:04 2023 +0900
@@ -1,3 +1,5 @@
+{-# OPTIONS --cubical-compatible --safe #-}
+
 module deriveUtil where
 
 open import Level renaming ( suc to succ ; zero to Zero )
diff -r dfaf230f7b9a -r af8f630b7e60 automaton-in-agda/src/even.agda
--- a/automaton-in-agda/src/even.agda	Sun Sep 24 13:20:31 2023 +0900
+++ b/automaton-in-agda/src/even.agda	Sun Sep 24 18:02:04 2023 +0900
@@ -1,3 +1,5 @@
+{-# OPTIONS --cubical-compatible --safe #-}
+
 module even where
 
 open import Data.Nat 
diff -r dfaf230f7b9a -r af8f630b7e60 automaton-in-agda/src/extended-automaton.agda
--- a/automaton-in-agda/src/extended-automaton.agda	Sun Sep 24 13:20:31 2023 +0900
+++ b/automaton-in-agda/src/extended-automaton.agda	Sun Sep 24 18:02:04 2023 +0900
@@ -1,4 +1,6 @@
-{-# OPTIONS --allow-unsolved-metas #-}
+{-# OPTIONS --cubical-compatible --safe #-}
+
+-- {-# OPTIONS --allow-unsolved-metas #-}
 module extended-automaton where
 
 open import Level renaming ( suc to succ ; zero to Zero )
diff -r dfaf230f7b9a -r af8f630b7e60 automaton-in-agda/src/finiteSetUtil.agda
--- a/automaton-in-agda/src/finiteSetUtil.agda	Sun Sep 24 13:20:31 2023 +0900
+++ b/automaton-in-agda/src/finiteSetUtil.agda	Sun Sep 24 18:02:04 2023 +0900
@@ -27,7 +27,7 @@
 
 module _ {Q : Set } (F : FiniteSet Q) where
      open FiniteSet F
-     equal?-refl  : { x : Q } → equal? x x ≡ true 
+     equal?-refl  : { x : Q } → equal? x x ≡ true
      equal?-refl {x} with F←Q x ≟ F←Q x
      ... | yes eq = refl
      ... | no ne = ⊥-elim (ne refl)
@@ -47,24 +47,24 @@
      ... | yes eq = yes (subst₂ (λ j k → j ≡ k ) (finiso→ x) (finiso→ y) (cong Q←F eq) )
      ... | no n = no (λ eq → n (cong F←Q eq))
      End : (m : ℕ ) → (p : Q → Bool ) → Set
-     End m p = (i : Fin finite) → m ≤ toℕ i → p (Q←F i )  ≡ false 
+     End m p = (i : Fin finite) → m ≤ toℕ i → p (Q←F i )  ≡ false
      first-end :  ( p : Q → Bool ) → End finite p
      first-end p i i>n = ⊥-elim (nat-≤> i>n (fin<n {finite} i) )
      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 NP.<-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 
+              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  (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
-         found1 (suc m)  m<n end | yes eq = subst (λ k → k \/ exists1 m (<to≤  m<n) p ≡ true ) (sym eq) (bool-or-4 {exists1 m (<to≤  m<n) p} ) 
+         found1 (suc m)  m<n end | yes eq = subst (λ k → k \/ exists1 m (<to≤  m<n) p ≡ true ) (sym eq) (bool-or-4 {exists1 m (<to≤  m<n) p} )
          found1 (suc m)  m<n end | no np = begin
                  p (Q←F (fromℕ< m<n)) \/ exists1 m (<to≤  m<n) p
               ≡⟨ bool-or-1 (¬-bool-t np ) ⟩
@@ -78,9 +78,9 @@
          not-found2  zero  _ = refl
          not-found2 ( suc m ) m<n with pn (Q←F (fromℕ< {m} {finite} m<n))
          not-found2 (suc m) m<n | eq = begin
-                  p (Q←F (fromℕ< m<n)) \/ exists1 m (<to≤ m<n) p 
+                  p (Q←F (fromℕ< m<n)) \/ exists1 m (<to≤ m<n) p
               ≡⟨ bool-or-1 eq ⟩
-                  exists1 m (<to≤ m<n) p 
+                  exists1 m (<to≤ m<n) p
               ≡⟨ not-found2 m (<to≤ m<n)  ⟩
                   false
               ∎  where open ≡-Reasoning
@@ -92,9 +92,9 @@
              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 = 
-               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 
+         found2 (suc m)  m<n end | no np =
+               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)
@@ -103,16 +103,16 @@
 
 
 
-iso-fin : {A B : Set} → FiniteSet A  → Bijection A B → FiniteSet B 
+iso-fin : {A B : Set} → FiniteSet A  → Bijection A B → FiniteSet B
 iso-fin {A} {B}  fin iso = record {
        Q←F = λ f → fun→ iso ( FiniteSet.Q←F fin f )
      ; F←Q = λ b → FiniteSet.F←Q fin (fun← iso b )
-     ; finiso→ = finiso→ 
-     ; finiso← = finiso← 
+     ; finiso→ = finiso→
+     ; finiso← = finiso←
    } where
    finiso→ : (q : B) → fun→ iso (FiniteSet.Q←F fin (FiniteSet.F←Q fin (Bijection.fun← iso q))) ≡ q
    finiso→ q = begin
-             fun→ iso (FiniteSet.Q←F fin (FiniteSet.F←Q fin (Bijection.fun← iso q))) 
+             fun→ iso (FiniteSet.Q←F fin (FiniteSet.F←Q fin (Bijection.fun← iso q)))
            ≡⟨ cong (λ k → fun→ iso k ) (FiniteSet.finiso→ fin _ ) ⟩
              fun→ iso (Bijection.fun← iso q)
            ≡⟨ fiso→ iso _ ⟩
@@ -120,9 +120,9 @@
            ∎  where open ≡-Reasoning
    finiso← : (f : Fin (FiniteSet.finite fin ))→ FiniteSet.F←Q fin (Bijection.fun← iso (Bijection.fun→ iso (FiniteSet.Q←F fin f))) ≡ f
    finiso← f = begin
-              FiniteSet.F←Q fin (Bijection.fun← iso (Bijection.fun→ iso (FiniteSet.Q←F fin f))) 
+              FiniteSet.F←Q fin (Bijection.fun← iso (Bijection.fun→ iso (FiniteSet.Q←F fin f)))
            ≡⟨ cong (λ k → FiniteSet.F←Q fin k ) (Bijection.fiso← iso _) ⟩
-              FiniteSet.F←Q fin (FiniteSet.Q←F fin f) 
+              FiniteSet.F←Q fin (FiniteSet.Q←F fin f)
            ≡⟨ FiniteSet.finiso← fin _  ⟩
               f
            ∎  where
@@ -136,7 +136,7 @@
     fin00 : (q : One) → one ≡ q
     fin00 one = refl
 
-fin-∨1 : {B : Set} → (fb : FiniteSet B ) → FiniteSet (One ∨ B) 
+fin-∨1 : {B : Set} → (fb : FiniteSet B ) → FiniteSet (One ∨ B)
 fin-∨1 {B} fb =  record {
        Q←F = Q←F
      ; F←Q =  F←Q
@@ -149,7 +149,7 @@
    Q←F (suc f) = case2 (FiniteSet.Q←F fb f)
    F←Q : One ∨ B → Fin (suc b)
    F←Q (case1 one) = zero
-   F←Q (case2 f ) = suc (FiniteSet.F←Q fb f) 
+   F←Q (case2 f ) = suc (FiniteSet.F←Q fb f)
    finiso→ : (q : One ∨ B) → Q←F (F←Q q) ≡ q
    finiso→ (case1 one) = refl
    finiso→ (case2 b) = cong (λ k → case2 k ) (FiniteSet.finiso→ fb b)
@@ -158,7 +158,7 @@
    finiso← (suc f) = cong ( λ k → suc k ) (FiniteSet.finiso← fb f)
 
 
-fin-∨2 : {B : Set} → ( a : ℕ ) → FiniteSet B  → FiniteSet (Fin a ∨ B) 
+fin-∨2 : {B : Set} → ( a : ℕ ) → FiniteSet B  → FiniteSet (Fin a ∨ B)
 fin-∨2 {B} zero  fb = iso-fin fb iso where
  iso : Bijection B (Fin zero ∨ B)
  iso =  record {
@@ -168,7 +168,7 @@
       ; fiso← = λ _ → refl
     } where
      fun←1 : Fin zero ∨ B → B
-     fun←1 (case2 x) = x 
+     fun←1 (case2 x) = x
      fiso→1 : (f : Fin zero ∨ B ) → case2 (fun←1 f) ≡ f
      fiso→1 (case2 x)  = refl
 fin-∨2 {B} (suc a) fb =  iso-fin (fin-∨1 (fin-∨2 a fb) ) iso
@@ -193,9 +193,9 @@
 fun→ (FiniteSet→Fin fin) f = FiniteSet.Q←F fin f
 fiso← (FiniteSet→Fin fin) = FiniteSet.finiso← fin
 fiso→ (FiniteSet→Fin fin) =  FiniteSet.finiso→ fin
-   
+
 
-fin-∨ : {A B : Set} → FiniteSet A → FiniteSet B → FiniteSet (A ∨ B) 
+fin-∨ : {A B : Set} → FiniteSet A → FiniteSet B → FiniteSet (A ∨ B)
 fin-∨ {A} {B}  fa fb = iso-fin (fin-∨2 a  fb ) iso2 where
     a = FiniteSet.finite fa
     ia = FiniteSet→Fin fa
@@ -211,14 +211,14 @@
 
 open import Data.Product hiding ( map )
 
-fin-× : {A B : Set} → FiniteSet A → FiniteSet B → FiniteSet (A × B) 
+fin-× : {A B : Set} → FiniteSet A → FiniteSet B → FiniteSet (A × B)
 fin-× {A} {B}  fa fb with FiniteSet→Fin fa
 ... | a=f = iso-fin (fin-×-f a ) iso-1 where
    a = FiniteSet.finite fa
    b = FiniteSet.finite fb
    iso-1 : Bijection (Fin a × B) ( A × B )
-   fun← iso-1 x = ( FiniteSet.F←Q fa (proj₁ x)  , proj₂ x) 
-   fun→ iso-1 x = ( FiniteSet.Q←F fa (proj₁ x)  , proj₂ x) 
+   fun← iso-1 x = ( FiniteSet.F←Q fa (proj₁ x)  , proj₂ x)
+   fun→ iso-1 x = ( FiniteSet.Q←F fa (proj₁ x)  , proj₂ x)
    fiso← iso-1 x  =  lemma  where
      lemma : (FiniteSet.F←Q fa (FiniteSet.Q←F fa (proj₁ x)) , proj₂ x) ≡ ( proj₁ x , proj₂ x )
      lemma = cong ( λ k → ( k ,  proj₂ x ) )  (FiniteSet.finiso← fa _ )
@@ -234,19 +234,19 @@
    fiso→ iso-2 (zero , b ) = refl
    fiso→ iso-2 (suc a , b ) = refl
 
-   fin-×-f : ( a  : ℕ ) → FiniteSet ((Fin a) × B) 
+   fin-×-f : ( a  : ℕ ) → FiniteSet ((Fin a) × B)
    fin-×-f zero = record { Q←F = λ () ; F←Q = λ () ; finiso→ = λ () ; finiso← = λ () ; finite = 0 }
    fin-×-f (suc a) = iso-fin ( fin-∨ fb ( fin-×-f a ) ) iso-2
 
 open _∧_
 
-fin-∧ : {A B : Set} → FiniteSet A → FiniteSet B → FiniteSet (A ∧ B) 
+fin-∧ : {A B : Set} → FiniteSet A → FiniteSet B → FiniteSet (A ∧ B)
 fin-∧ {A} {B} fa fb with FiniteSet→Fin fa    -- same thing for our tool
 ... | a=f = iso-fin (fin-×-f a ) iso-1 where
    a = FiniteSet.finite fa
    b = FiniteSet.finite fb
    iso-1 : Bijection (Fin a ∧ B) ( A ∧ B )
-   fun← iso-1 x = record { proj1 = FiniteSet.F←Q fa (proj1 x)  ; proj2 =  proj2 x} 
+   fun← iso-1 x = record { proj1 = FiniteSet.F←Q fa (proj1 x)  ; proj2 =  proj2 x}
    fun→ iso-1 x = record { proj1 = FiniteSet.Q←F fa (proj1 x)  ; proj2 =  proj2 x}
    fiso← iso-1 x  =  lemma  where
      lemma : record { proj1 = FiniteSet.F←Q fa (FiniteSet.Q←F fa (proj1 x)) ; proj2 =  proj2 x} ≡ record {proj1 =  proj1 x ; proj2 =  proj2 x }
@@ -263,7 +263,7 @@
    fiso→ iso-2 (record { proj1 = zero ; proj2 =  b }) = refl
    fiso→ iso-2 (record { proj1 = suc a ; proj2 =  b }) = refl
 
-   fin-×-f : ( a  : ℕ ) → FiniteSet ((Fin a) ∧ B) 
+   fin-×-f : ( a  : ℕ ) → FiniteSet ((Fin a) ∧ B)
    fin-×-f zero = record { Q←F = λ () ; F←Q = λ () ; finiso→ = λ () ; finiso← = λ () ; finite = 0 }
    fin-×-f (suc a) = iso-fin ( fin-∨ fb ( fin-×-f a ) ) iso-2
 
@@ -292,12 +292,12 @@
 cast-iso refl (suc f) = cong ( λ k → suc k ) ( cast-iso refl f )
 
 
-fin2List : {n : ℕ } → FiniteSet (Vec Bool n) 
+fin2List : {n : ℕ } → FiniteSet (Vec Bool n)
 fin2List {zero} = record {
    Q←F = λ _ → Vec.[]
  ; F←Q =  λ _ → # 0
- ; finiso→ = finiso→ 
- ; finiso← = finiso← 
+ ; finiso→ = finiso→
+ ; finiso← = finiso←
    } where
    Q = Vec Bool zero
    finiso→ : (q : Q) → [] ≡ q
@@ -309,7 +309,7 @@
    QtoR : Vec Bool (suc  n) →  Vec Bool n ∨ Vec Bool n
    QtoR ( true ∷ x ) = case1 x
    QtoR ( false ∷ x ) = case2 x
-   RtoQ : Vec Bool n ∨ Vec Bool n → Vec Bool (suc  n) 
+   RtoQ : Vec Bool n ∨ Vec Bool n → Vec Bool (suc  n)
    RtoQ ( case1 x ) = true ∷ x
    RtoQ ( case2 x ) = false ∷ x
    isoRQ : (x : Vec Bool (suc  n) ) → RtoQ ( QtoR x ) ≡ x
@@ -329,17 +329,17 @@
    qb1 : (q : Q) → toℕ (FiniteSet.F←Q fin q) < n → Bool
    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 : 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 (NP.<-trans n<m a<sa ) t q
 
-open import Level renaming ( suc to Suc ; zero to Zero) 
+open import Level renaming ( suc to Suc ; zero to Zero)
 
 
 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 
+L2F fin n<m x q q<n = List2Func fin n<m x q
 
 L2F-iso : { Q : Set } → (fin : FiniteSet Q ) → (f : Q → Bool ) → (q : Q ) → (L2F fin a<sa (F2L fin a<sa (λ q _ → f q) )) q (toℕ<n _) ≡ f q
 L2F-iso {Q} fin f q = l2f m a<sa (toℕ<n _) where
@@ -352,93 +352,25 @@
      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 
+     lemma12f : {n m : ℕ } → (n<m : n < m ) → (f : Fin m )  → toℕ f ≡ n → f ≡ fromℕ< n<m
      lemma12f {zero} {suc m} (s≤s z≤n) zero refl = refl
      lemma12f {suc n} {suc m} (s≤s n<m) (suc f) refl = subst ( λ k → suc f ≡ k ) (sym (lemma3f n<m) ) ( cong ( λ k → suc k ) ( lemma12f {n} {m} n<m f refl  ) )
   l2f :  (n : ℕ ) → (n<m : n < suc m ) → (q<n : toℕ (FiniteSet.F←Q fin q ) < n )  →  (L2F fin n<m (F2L fin n<m  (λ q _ → f q))) q q<n ≡ f q
   l2f zero (s≤s z≤n) ()
-  l2f (suc n) (s≤s n<m) (s≤s n<q) with FiniteSet.F←Q fin q ≟ fromℕ< n<m 
-  l2f (suc n) (s≤s n<m) (s≤s n<q) | yes p = begin 
-        f (FiniteSet.Q←F fin (fromℕ< n<m)) 
+  l2f (suc n) (s≤s n<m) (s≤s n<q) with FiniteSet.F←Q fin q ≟ fromℕ< n<m
+  l2f (suc n) (s≤s n<m) (s≤s n<q) | yes p = begin
+        f (FiniteSet.Q←F fin (fromℕ< n<m))
      ≡⟨ cong ( λ k → f (FiniteSet.Q←F fin k )) (sym p)  ⟩
         f (FiniteSet.Q←F fin ( FiniteSet.F←Q fin q ))
      ≡⟨ cong ( λ k → f k ) (FiniteSet.finiso→ fin _ ) ⟩
-        f q 
+        f q
      ∎  where
        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)
 
-Fin2Finite : ( n : ℕ ) → FiniteSet (Fin n) 
+Fin2Finite : ( n : ℕ ) → FiniteSet (Fin n)
 Fin2Finite n = record { F←Q = λ x → x ; Q←F = λ x → x ; finiso← = λ q → refl ; finiso→ = λ q → refl }
 
-data fin-less { n : ℕ } { A : Set }  (fa : FiniteSet A ) (n<m : n < FiniteSet.finite fa ) : Set where
-  elm1 : (elm : A ) → toℕ (FiniteSet.F←Q fa elm ) < n → fin-less fa n<m 
-
-get-elm : { n : ℕ }  { A : Set } {fa : FiniteSet A } {n<m : n < FiniteSet.finite fa } → fin-less fa n<m → A
-get-elm (elm1 a _ ) = a
-
-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-< : {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 )
-    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))
-      ≡⟨ toℕ-fromℕ< _ ⟩
-         toℕ x
-      ∎  where
-          open ≡-Reasoning
-    fun← iso (elm1 elm x) = fromℕ< x
-    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ℕ< (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ℕ< (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ℕ< (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 _ ) ) ⟩
-           fromℕ< lemma6
-        ≡⟨ lemma10 (lemma11 n<m ) ⟩
-           fromℕ< ( toℕ<n x )
-        ≡⟨ fromℕ<-toℕ _ _ ⟩
-           x 
-        ∎  where
-          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) = ? 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)
-         ≡⟨ toℕ-fromℕ< _ ⟩
-            toℕ (FiniteSet.F←Q fa elm)
-         ∎  where open ≡-Reasoning
-      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ℕ< (NP.<-trans (toℕ<n (Bijection.fun← iso (elm1 elm 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ℕ< ( NP.<-trans x n<m))
-         ≡⟨ 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 )
-         ≡⟨ FiniteSet.finiso→ fa _ ⟩
-            elm 
-         ∎  where open ≡-Reasoning
-
 open import Data.List
 
 open FiniteSet
@@ -473,28 +405,28 @@
 ... | false = phase1 finq q qs
 
 dup-in-list : { Q : Set }  (finq : FiniteSet Q) (q : Q) (qs : List Q ) → Bool
-dup-in-list {Q} finq q qs = phase1 finq q qs 
+dup-in-list {Q} finq q qs = phase1 finq q qs
 
 --
 -- if length of the list is longer than kinds of a finite set, there is a duplicate
 -- prove this based on the theorem on Data.Fin
 --
 
-dup-in-list+fin : { Q : Set }  (finq : FiniteSet Q) 
+dup-in-list+fin : { Q : Set }  (finq : FiniteSet Q)
    → (q : Q) (qs : List Q )
    → fin-dup-in-list (F←Q  finq q) (map (F←Q finq) qs) ≡ true
    → dup-in-list finq q qs ≡ true
 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 
+        → phase2 finq q qs ≡ true
     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
-    i-phase1 : (qs : List Q) → fin-phase1 (F←Q  finq q) (map (F←Q finq) qs) ≡ true 
-        → phase1 finq q qs ≡ true 
+    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 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
@@ -523,13 +455,13 @@
 
 open import bijection using ( InjectiveF ; Is )
 
--- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
+-- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
 
-inject-fin : {A B : Set}  (fa : FiniteSet A ) 
-   → (fi : InjectiveF B A) 
+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 with finite fa in eq1 
+inject-fin {A} {B} fa fi is-B with finite fa in eq1
 ... | zero = record {
        finite = 0
        ; Q←F = λ ()
@@ -551,7 +483,7 @@
     pfa<fa : pfa < finite fa
     pfa<fa = subst (λ k → pfa < k ) (sym eq1) a<sa
     0<fa : 0 < finite fa
-    0<fa = <-transˡ (s≤s z≤n) pfa<fa  
+    0<fa = <-transˡ (s≤s z≤n) pfa<fa
 
     count-B : ℕ → ℕ
     count-B zero with is-B (Q←F fa ( fromℕ< {0} 0<fa ))
@@ -582,46 +514,93 @@
          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 <-cmp (finite fa) 1 
+             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 )) 
+             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 : count-B 0 ≡ 1    -- in-equality does not work we have to repeat the proof
                   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)) 
+             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 lem14) where
                   lem14 : count-B (suc i) ≡ count-B i
-                  lem14 with <-cmp (finite fa) (suc 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 ?)
+             ... | 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 = refl
+                  ... | tri> ¬a ¬b c = ⊥-elim ( ¬c c )
              ... | 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 ?)) a≤sa
-             ... | yes  isb0 | no  nisb1 = refl-≤≡ (sym ?)
-             ... | no  nisb0 | yes  isb1 = ≤-trans (refl-≤≡ (sym ?)) a≤sa
-             ... | no  nisb0 | no  nisb1 = refl-≤≡ (sym ?)
+             ... | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c with is-B (Q←F fa (fromℕ< c))
+             ... | yes  isb = refl-≤≡ (sym lem14) where
+                  lem14 : count-B (suc i) ≡ suc (count-B i)
+                  lem14 with <-cmp (finite fa) (suc i)
+                  ... | tri< a₂ ¬b₂ ¬c₂ = ⊥-elim (¬c₂ c)
+                  ... | tri≈ ¬a₂ b₂ ¬c₂ = ⊥-elim (¬c₂ c)
+                  ... | tri> ¬a₂ ¬b₂ c₂ with is-B (Q←F fa ( fromℕ< c₂ ))
+                  ... | yes isb = refl
+                  ... | no ne = ⊥-elim (ne record {a = Is.a isb ; fa=c = trans (Is.fa=c isb) (cong (λ k → Q←F fa k) (lemma10 refl )) } )
+             ... | no  nisb = refl-≤≡ (sym lem14) where
+                  lem14 : count-B (suc i) ≡ count-B i
+                  lem14 with <-cmp (finite fa) (suc i)
+                  ... | tri< a₂ ¬b₂ ¬c₂ = ⊥-elim (¬c₂ c)
+                  ... | tri≈ ¬a₂ b₂ ¬c₂ = ⊥-elim (¬c₂ c)
+                  ... | tri> ¬a₂ ¬b₂ c₂ with is-B (Q←F fa ( fromℕ< c₂ ))
+                  ... | yes isb = ⊥-elim (nisb record {a = Is.a isb ; fa=c = trans (Is.fa=c isb) (cong (λ k → Q←F fa k) (lemma10 refl )) } )
+                  ... | no ne = refl
+             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 lem14)) a≤sa where
+                  lem14 : count-B (suc i) ≡ suc (count-B i)
+                  lem14 with <-cmp (finite fa) (suc i)
+                  ... | tri< a₂ ¬b₂ ¬c₂ = ⊥-elim (¬c₂ c)
+                  ... | tri≈ ¬a₂ b₂ ¬c₂ = ⊥-elim (¬c₂ c)
+                  ... | tri> ¬a₂ ¬b₂ c₂ with is-B (Q←F fa ( fromℕ< c₂ ))
+                  ... | no ne = ⊥-elim (ne record {a = Is.a isb0 ; fa=c = trans (Is.fa=c isb0) (cong (λ k → Q←F fa k) (lemma10 refl )) } )
+                  ... | yes isb = refl
+             ... | yes  isb0 | no  nisb1 = refl-≤≡ (sym lem14) where
+                  lem14 : count-B (suc i) ≡ suc (count-B i)
+                  lem14 with <-cmp (finite fa) (suc i)
+                  ... | tri< a₂ ¬b₂ ¬c₂ = ⊥-elim (¬c₂ c)
+                  ... | tri≈ ¬a₂ b₂ ¬c₂ = ⊥-elim (¬c₂ c)
+                  ... | tri> ¬a₂ ¬b₂ c₂ with is-B (Q←F fa ( fromℕ< c₂ ))
+                  ... | no ne = ⊥-elim (ne record {a = Is.a isb0 ; fa=c = trans (Is.fa=c isb0) (cong (λ k → Q←F fa k) (lemma10 refl )) } )
+                  ... | yes isb = refl
+             ... | no  nisb0 | yes  isb1 = ≤-trans (refl-≤≡ (sym lem14)) a≤sa where
+                  lem14 : count-B (suc i) ≡ count-B i
+                  lem14 with <-cmp (finite fa) (suc i)
+                  ... | tri< a₂ ¬b₂ ¬c₂ = ⊥-elim (¬c₂ c)
+                  ... | tri≈ ¬a₂ b₂ ¬c₂ = ⊥-elim (¬c₂ c)
+                  ... | tri> ¬a₂ ¬b₂ c₂ with is-B (Q←F fa ( fromℕ< c₂ ))
+                  ... | no ne = refl
+                  ... | yes isb = ⊥-elim (nisb0 record {a = Is.a isb ; fa=c = trans (Is.fa=c isb) (cong (λ k → Q←F fa k) (lemma10 refl )) } )
+             ... | no  nisb0 | no  nisb1 = refl-≤≡ (sym lem14) where
+                  lem14 : count-B (suc i) ≡ count-B i
+                  lem14 with <-cmp (finite fa) (suc i)
+                  ... | tri< a₂ ¬b₂ ¬c₂ = ⊥-elim (¬c₂ c)
+                  ... | tri≈ ¬a₂ b₂ ¬c₂ = ⊥-elim (¬c₂ c)
+                  ... | tri> ¬a₂ ¬b₂ c₂ with is-B (Q←F fa ( fromℕ< c₂ ))
+                  ... | no ne = refl
+                  ... | yes isb = ⊥-elim (nisb0 record {a = Is.a isb ; fa=c = trans (Is.fa=c isb) (cong (λ k → Q←F fa k) (lemma10 refl )) } )
 
     lem31 : (b : B) → 0 < count-B (toℕ (F←Q fa (f b)))
     lem31 b = lem32 (toℕ (F←Q fa (f b))) refl where
-        lem32 : (i : ℕ) → toℕ (F←Q fa (f b)) ≡ i → 0 < count-B i 
+        lem32 : (i : ℕ) → toℕ (F←Q fa (f b)) ≡ i → 0 < count-B i
         lem32 zero   eq with is-B (Q←F fa ( fromℕ< {0} 0<fa ))
-        ... | yes isb = s≤s z≤n 
+        ... | yes isb = s≤s z≤n
         ... | no nisb = ⊥-elim ( nisb record { a = b ; fa=c = lem33 } ) where
             lem33 : f b ≡ Q←F fa ( fromℕ< {0} 0<fa )
             lem33 = begin
@@ -630,11 +609,11 @@
               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) 
+        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 
+        ... | 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)
             lem33 = begin
@@ -643,41 +622,45 @@
               Q←F fa ( fromℕ< (fin<n _) )  ≡⟨ cong (λ k → Q←F fa k) (fromℕ<-cong _ _ eq (fin<n _) c ) ⟩
               Q←F fa ( fromℕ< c ) ∎ where
                 open ≡-Reasoning
- 
+
     cb<mb : (b : B) → pred (count-B (toℕ (F←Q fa (f b)))) < maxb
     cb<mb b = sx≤y→x<y ( begin
-        suc ( pred (count-B (toℕ (F←Q fa (f b)))))  ≡⟨ sucprd (lem31 b) ⟩ 
-        count-B (toℕ (F←Q fa (f b)))  ≤⟨ lem02 ⟩ 
+        suc ( pred (count-B (toℕ (F←Q fa (f b)))))  ≡⟨ sucprd (lem31 b) ⟩
+        count-B (toℕ (F←Q fa (f b)))  ≤⟨ lem02 ⟩
         count-B (finite fa)   ∎ ) where
           open ≤-Reasoning
           lem02 : count-B (toℕ (F←Q fa (f b))) ≤ count-B (finite fa)
-          lem02 = count-B-mono (<to≤ (fin<n {_} (F←Q fa (f b)))) 
+          lem02 = count-B-mono (<to≤ (fin<n {_} (F←Q fa (f b))))
 
     cb00 : (n : ℕ) → n < count-B (finite fa) → CountB n
     cb00 n n<cb = lem09 (finite fa) (count-B (finite fa)) (<-transˡ a<sa n<cb) refl where
 
-        lem06 : (i j : ℕ) → (i<fa : i < finite fa) (j<fa : j < finite fa) 
+        lem06 : (i j : ℕ) → (i<fa : i < finite fa) (j<fa : j < finite fa)
             →  Is B A f (Q←F fa (fromℕ< i<fa)) → Is B A f (Q←F fa (fromℕ< j<fa)) → count-B i ≡ count-B j → i ≡ j
         lem06 i j i<fa j<fa bi bj eq = lem08 where
-            lem20 : (i j : ℕ) → i < j → (i<fa : i < finite fa) (j<fa : j < finite fa) 
+            lem20 : (i j : ℕ) → i < j → (i<fa : i < finite fa) (j<fa : j < finite fa)
                 →  Is B A f (Q←F fa (fromℕ< i<fa)) → Is B A f (Q←F fa (fromℕ< j<fa)) → count-B i < count-B j
-            lem20 zero (suc j) i<j i<fa j<fa bi bj with <-cmp (finite fa) (suc j) 
+            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 )) |  is-B (Q←F fa (fromℕ< c)) 
+            ... | 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
                  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 _ |  yes _ = lem25 where
+            ... | yes isb1 |  yes _ = lem25 where
+                 lem14 : count-B 0 ≡ 1
+                 lem14 with is-B (Q←F fa ( fromℕ< 0<fa ))
+                 ... | no ne = ⊥-elim (ne record {a = Is.a isb1 ; fa=c = trans (Is.fa=c isb1) (cong (λ k → Q←F fa k) (lemma10 refl )) } )
+                 ... | yes isb = refl
                  lem25 : 2 ≤ suc (count-B j)
                  lem25 = begin
-                    2 ≡⟨ cong suc (sym ?) ⟩
+                    2 ≡⟨ cong suc (sym lem14) ⟩
                     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 
+            lem20 (suc i) zero () i<fa j<fa bi bj
             lem20 (suc i) (suc j) (s≤s i<j) i<fa j<fa bi bj = lem21 where
                  --
                  --                    i  <     suc i  ≤    j
@@ -687,7 +670,7 @@
                  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)) 
+                 ... | 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)
@@ -706,11 +689,15 @@
             ... | 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 )) 
+        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))
+        ... | case1 eq2 = record { b = Is.a isb ; cb = 0 ; b=cn = lem10 ; cb=n = trans lem14 (sym (trans eq2 eq))
                 ; cb-inject = λ cb1 c1<fa b1 eq → lem06 0 cb1 0<fa c1<fa isb b1 eq } where
+             lem14 : count-B 0 ≡ 1
+             lem14 with is-B (Q←F fa ( fromℕ< 0<fa ))
+             ... | no ne = ⊥-elim (ne record {a = Is.a isb ; fa=c = trans (Is.fa=c isb) (cong (λ k → Q←F fa k) (lemma10 refl )) } )
+             ... | yes isb = refl
              lem10 : 0 ≡ toℕ (F←Q fa (f (Is.a isb)))
              lem10 = begin
                 0 ≡⟨ sym ( toℕ-fromℕ< 0<fa ) ⟩
@@ -718,14 +705,21 @@
                 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) 
+        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 ? (sym (trans eq2 eq ))
+        ... | case1 eq2 = record { b = Is.a isb ; cb = suc i ;  b=cn = lem11 ; cb=n = trans lem14 (sym (trans eq2 eq ))
                 ; cb-inject = λ cb1 c1<fa b1 eq → lem06 (suc i) cb1 c c1<fa isb b1 eq } where
+              lem14 : count-B (suc i) ≡ suc (count-B i)
+              lem14 with <-cmp (finite fa) (suc i)
+              ... | tri< a₂ ¬b₂ ¬c₂ = ⊥-elim (¬c₂ c)
+              ... | tri≈ ¬a₂ b₂ ¬c₂ = ⊥-elim (¬c₂ c)
+              ... | tri> ¬a₂ ¬b₂ c₂ with is-B (Q←F fa ( fromℕ< c₂ ))
+              ... | yes isb = refl
+              ... | no ne = ⊥-elim (ne record {a = Is.a isb ; fa=c = trans (Is.fa=c isb) (cong (λ k → Q←F fa k) (lemma10 refl )) } )
               lem11 : suc i ≡ toℕ (F←Q fa (f (Is.a isb)))
               lem11 = begin
                 suc i ≡⟨ sym ( toℕ-fromℕ< c) ⟩
@@ -734,14 +728,14 @@
                 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 : 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 
+         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) ⟩ 
+            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 _)
@@ -757,17 +751,17 @@
              CB = cb00 (toℕ (fromℕ< (cb<mb b))) (fin<n _)
              isb : Is B A f (Q←F fa (fromℕ< (fin<n {_} (F←Q fa (f b)) )))
              isb = record { a = b ; fa=c = lem33 } where
-                 lem33 : f b ≡ Q←F fa (fromℕ< (fin<n (F←Q fa (f b)))) 
+                 lem33 : f b ≡ Q←F fa (fromℕ< (fin<n (F←Q fa (f b))))
                  lem33 = begin
                      f b ≡⟨ sym (finiso→ fa _) ⟩
                      Q←F fa (F←Q fa (f b))  ≡⟨ cong (Q←F fa) (sym (fromℕ<-toℕ _ (fin<n (F←Q fa (f b))))) ⟩
-                     Q←F fa (fromℕ< (fin<n (F←Q fa (f b))))  ∎ 
+                     Q←F fa (fromℕ< (fin<n (F←Q fa (f b))))  ∎
              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 b) ⟩
-                 count-B (toℕ (F←Q fa (f b))) ∎ 
+                 count-B (toℕ (F←Q fa (f b))) ∎
 
 
 -- end
diff -r dfaf230f7b9a -r af8f630b7e60 automaton-in-agda/src/flcagl.agda
--- a/automaton-in-agda/src/flcagl.agda	Sun Sep 24 13:20:31 2023 +0900
+++ b/automaton-in-agda/src/flcagl.agda	Sun Sep 24 18:02:04 2023 +0900
@@ -1,3 +1,5 @@
+{-# OPTIONS --cubical-compatible #-}
+
 {-# OPTIONS --sized-types #-}
 open import Relation.Nullary
 open import Relation.Binary.PropositionalEquality
diff -r dfaf230f7b9a -r af8f630b7e60 automaton-in-agda/src/gcd.agda
--- a/automaton-in-agda/src/gcd.agda	Sun Sep 24 13:20:31 2023 +0900
+++ b/automaton-in-agda/src/gcd.agda	Sun Sep 24 18:02:04 2023 +0900
@@ -1,4 +1,6 @@
-{-# OPTIONS --allow-unsolved-metas #-}
+{-# OPTIONS --cubical-compatible --safe #-}
+
+-- {-# OPTIONS --allow-unsolved-metas #-}
 module gcd where
 
 open import Data.Nat 
@@ -16,7 +18,7 @@
 gcd1 : ( i i0 j j0 : ℕ ) → ℕ
 gcd1 zero i0 zero j0 with <-cmp i0 j0
 ... | tri< a ¬b ¬c = i0
-... | tri≈ ¬a refl ¬c = i0
+... | tri≈ ¬a b ¬c = i0
 ... | tri> ¬a ¬b c = j0
 gcd1 zero i0 (suc zero) j0 = 1
 gcd1 zero zero (suc (suc j)) j0 = j0
@@ -46,7 +48,7 @@
 gcdmm : (n m : ℕ) → gcd1 n m n m ≡ m
 gcdmm zero m with <-cmp m m
 ... | tri< a ¬b ¬c = refl
-... | tri≈ ¬a refl ¬c = refl
+... | tri≈ ¬a b ¬c = refl
 ... | tri> ¬a ¬b c = refl
 gcdmm (suc n) m  = subst (λ k → k ≡ m) (sym (gcd22 n m n m )) (gcdmm n m )
 
@@ -56,7 +58,7 @@
 ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = ⊥-elim (nat-≡< (sym b) a) 
 ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = refl
 ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = ⊥-elim (nat-≡< (sym b) a) 
-... | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = refl
+... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = b
 ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c = ⊥-elim (nat-≡< b c) 
 ... | tri> ¬a ¬b c | tri< a ¬b₁ ¬c = refl
 ... | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c = ⊥-elim (nat-≡< b c) 
@@ -317,7 +319,7 @@
         ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = ⊥-elim (¬b (sym b))
         ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = refl
         ... | tri≈ ¬a refl ¬c | tri< a ¬b ¬c₁ = ⊥-elim (¬b refl)
-        ... | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = refl
+        ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = refl
         ... | tri≈ ¬a refl ¬c | tri> ¬a₁ ¬b c = ⊥-elim (¬b refl)
         ... | tri> ¬a ¬b c | tri< a ¬b₁ ¬c = refl
         ... | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c = ⊥-elim (¬b (sym b))
@@ -694,7 +696,11 @@
       1 ∎ where open ≡-Reasoning
 
 m*n=m→n : {m n : ℕ } → 0 < m → m * n ≡ m * 1 → n ≡ 1
-m*n=m→n {suc m} {n} (s≤s lt) eq = *-cancelˡ-≡ m eq 
+m*n=m→n {suc m} {n} (s≤s lt) eq = begin 
+    n ≡⟨ *-cancelˡ-≡ n 1 (suc m) ( begin
+       suc m * n ≡⟨ eq ⟩
+       suc m * 1  ∎ ) ⟩
+    1   ∎ where open ≡-Reasoning
 
 gcd-is-gratest :  { i j  k : ℕ } → i > 0 → j > 0 → k > 1 → Dividable k i → Dividable k j → k ≤ gcd i j 
 gcd-is-gratest {i} {j} {k} i>0 j>0 k>1 ki kj = div→k≤m k>1 (gcd>0 i j i>0 j>0 ) gcd001 where
@@ -712,16 +718,16 @@
    jd  : Dividable d (suc j)
    jd  = proj2 (gcd-dividable (suc i) (suc j))
    cop : gcd (Dividable.factor id) (Dividable.factor jd) ≡ 1
-   cop with (gcd (Dividable.factor id) (Dividable.factor jd)) | inspect (gcd (Dividable.factor id)) (Dividable.factor jd)
-   ... | zero | record { eq  = eq1 } = ⊥-elim ( nat-≡< (sym eq1) (gcd>0 (Dividable.factor id) (Dividable.factor jd)
+   cop with (gcd (Dividable.factor id) (Dividable.factor jd)) in eq
+   ... | zero = ⊥-elim ( nat-≡< (sym eq) (gcd>0 (Dividable.factor id) (Dividable.factor jd)
        (0<factor d>0 (s≤s z≤n) id) (0<factor d>0 (s≤s z≤n) jd) ))
-   ... | suc zero | record { eq  = eq1 } = refl
-   ... | suc (suc t) | record { eq  = eq1 } = ⊥-elim ( nat-≤> (gcd-is-gratest {suc i} {(suc j)} (s≤s z≤n) (s≤s z≤n) co1 d1id d1jd ) gcd<d1 ) where
+   ... | suc zero = refl
+   ... | suc (suc t) = ⊥-elim ( nat-≤> (gcd-is-gratest {suc i} {(suc j)} (s≤s z≤n) (s≤s z≤n) co1 d1id d1jd ) gcd<d1 ) where
         -- gcd-is-gratest :  { i j  k : ℕ } → i > 0 → j > 0 → k > 1 → Dividable k i → Dividable k j → k ≤ gcd i j
         d1 : ℕ
         d1 = gcd (Dividable.factor id) (Dividable.factor jd)
         d1>1 : gcd (Dividable.factor id) (Dividable.factor jd) > 1
-        d1>1 = subst (λ k → 1 < k ) (sym eq1) (s≤s (s≤s z≤n))
+        d1>1 = subst (λ k → 1 < k ) (sym eq) (s≤s (s≤s z≤n))
         mul1 :  {x : ℕ} → 1 * x ≡ x
         mul1 {zero} = refl
         mul1 {suc x} = begin
diff -r dfaf230f7b9a -r af8f630b7e60 automaton-in-agda/src/halt.agda
--- a/automaton-in-agda/src/halt.agda	Sun Sep 24 13:20:31 2023 +0900
+++ b/automaton-in-agda/src/halt.agda	Sun Sep 24 18:02:04 2023 +0900
@@ -1,3 +1,5 @@
+{-# OPTIONS --cubical-compatible  #-}
+
 module halt where
 
 open import Level renaming ( zero to Zero ; suc to Suc )
@@ -92,8 +94,8 @@
      h-just h y eq with h y
      h-just h y refl | true = refl
      TN1 :  (h : List Bool → Bool) → (y : List Bool ) → Halt.halt halt (UTM.utm utm) (tenc h y) ≡ h y
-     TN1 h y with h y | inspect h y
-     ... | true  | record { eq = eq1 } = begin
+     TN1 h y with h y in eq1
+     ... | true  = begin
         Halt.halt halt (UTM.utm utm)  (tenc h y) ≡⟨ proj2 (is-halt halt (UTM.utm utm) (tenc h y) ) (case1 (sym tm-tenc)) ⟩
         true ∎  where
           tm-tenc :  tm (UTM.utm utm) (tenc h y) ≡ just true
@@ -101,7 +103,7 @@
               tm (UTM.utm utm) (tenc h y)  ≡⟨  is-tm utm _ y ⟩
               h1 h y ≡⟨ h-just h y eq1  ⟩
               just true  ∎  
-     ... | false | record { eq = eq1 } = begin
+     ... | false = begin
         Halt.halt halt (UTM.utm utm)  (tenc h y) ≡⟨ proj2 (is-not-halt halt (UTM.utm utm) (tenc h y) ) (sym tm-tenc) ⟩
         false ∎  where
           tm-tenc :  tm (UTM.utm utm) (tenc h y) ≡ nothing
diff -r dfaf230f7b9a -r af8f630b7e60 automaton-in-agda/src/induction-ex.agda
--- a/automaton-in-agda/src/induction-ex.agda	Sun Sep 24 13:20:31 2023 +0900
+++ b/automaton-in-agda/src/induction-ex.agda	Sun Sep 24 18:02:04 2023 +0900
@@ -1,4 +1,5 @@
-{-# OPTIONS --guardedness --sized-types #-}
+{-# OPTIONS --cubical-compatible --guardedness --sized-types #-}
+
 module induction-ex where
 
 open import Relation.Binary.PropositionalEquality
diff -r dfaf230f7b9a -r af8f630b7e60 automaton-in-agda/src/lang-text.agda
--- a/automaton-in-agda/src/lang-text.agda	Sun Sep 24 13:20:31 2023 +0900
+++ b/automaton-in-agda/src/lang-text.agda	Sun Sep 24 18:02:04 2023 +0900
@@ -3,7 +3,7 @@
 open import Data.List
 open import Data.String
 open import Data.Char
-open import Data.Char.Unsafe
+-- open import Data.Char.Unsafe
 open import Relation.Binary.PropositionalEquality
 open import Relation.Nullary
 open import logic
@@ -36,19 +36,19 @@
 ex15c : Set
 
 -- w is any string not in a*b*
-ex15c = (w : String ) → ( ¬ (contains w "ab"  ≡ true )  /\ ( ¬ (contains w "ba"  ≡ true ) 
+ex15c = (w : String ) → ( ¬ (contains w "ab"  ≡ true ))  /\ ( ¬ (contains w "ba"  ≡ true ) ) 
 
-ex15d : {!!}
-ex15d = {!!}
+ex15d : ?
+ex15d = ?
 
-ex15e : {!!}
-ex15e = {!!}
+ex15e : ?
+ex15e = ?
 
-ex15f : {!!}
-ex15f = {!!}
+ex15f : ?
+ex15f = ?
 
-ex15g : {!!}
-ex15g = {!!}
+ex15g : ?
+ex15g = ?
 
-ex15h : {!!}
-ex15h = {!!}
+ex15h : ?
+ex15h = ?
diff -r dfaf230f7b9a -r af8f630b7e60 automaton-in-agda/src/libbijection.agda
--- a/automaton-in-agda/src/libbijection.agda	Sun Sep 24 13:20:31 2023 +0900
+++ b/automaton-in-agda/src/libbijection.agda	Sun Sep 24 18:02:04 2023 +0900
@@ -1,3 +1,5 @@
+{-# OPTIONS --cubical-compatible --safe #-}
+
 module libbijection where
 
 open import Level renaming ( zero to Zero ; suc to Suc )
@@ -7,7 +9,7 @@
 open import Data.Nat.Properties
 open import Relation.Nullary
 open import Data.Empty
-open import Data.Unit hiding ( _≤_ )
+open import Data.Unit 
 open import  Relation.Binary.Core hiding (_⇔_)
 open import  Relation.Binary.Definitions
 open import Relation.Binary.PropositionalEquality
diff -r dfaf230f7b9a -r af8f630b7e60 automaton-in-agda/src/nfa.agda
--- a/automaton-in-agda/src/nfa.agda	Sun Sep 24 13:20:31 2023 +0900
+++ b/automaton-in-agda/src/nfa.agda	Sun Sep 24 18:02:04 2023 +0900
@@ -254,9 +254,9 @@
 
 to-list1 : {Q : Set } (qs : Q → Bool ) →  (all : List Q) → foldr (λ q x → qs q /\ x ) true (ssQ  qs all ) ≡ true
 to-list1 qs []  = refl
-to-list1 qs (x ∷ all)  with qs x  | inspect qs x
-... | false | record { eq = eq } = to-list1 qs all 
-... | true  | record { eq = eq } = subst (λ k → k /\ foldr (λ q → _/\_ (qs q)) true (ssQ qs all) ≡ true ) (sym eq) ( bool-t1 (to-list1 qs all) )
+to-list1 qs (x ∷ all)  with qs x  in eq
+... | false = to-list1 qs all 
+... | true  = subst (λ k → k /\ foldr (λ q → _/\_ (qs q)) true (ssQ qs all) ≡ true ) (sym eq) ( bool-t1 (to-list1 qs all) )
 
 existsS1-valid : ¬ ( (qs : States1 → Bool ) →  ( existsS1 qs ≡ true ) )
 existsS1-valid n = ¬-bool refl ( n ( λ x → false ))
diff -r dfaf230f7b9a -r af8f630b7e60 automaton-in-agda/src/non-regular.agda
--- a/automaton-in-agda/src/non-regular.agda	Sun Sep 24 13:20:31 2023 +0900
+++ b/automaton-in-agda/src/non-regular.agda	Sun Sep 24 18:02:04 2023 +0900
@@ -1,3 +1,5 @@
+{-# OPTIONS --cubical-compatible --safe #-}
+
 module non-regular where
 
 open import Data.Nat
@@ -66,8 +68,10 @@
 t5 : ( n : ℕ ) → Set
 t5 n = inputnn1 ( inputnn0 n  )  ≡ true
 
-cons-inject : {A : Set} {x1 x2 : List A } { a : A } → a ∷ x1 ≡ a ∷ x2 → x1 ≡ x2
-cons-inject refl = refl
+import Level 
+
+cons-inject : {n : Level.Level } (A : Set n) { a b : A } {x1 x2 : List A} → a ∷ x1 ≡ b ∷ x2 → x1 ≡ x2
+cons-inject _ refl = refl
 
 append-[] : {A : Set} {x1 : List A } → x1 ++ [] ≡ x1
 append-[] {A} {[]} = refl
@@ -90,23 +94,23 @@
 nn01  : (i : ℕ) → inputnn1 ( inputnn0 i  ) ≡ true
 nn01  i = subst₂ (λ j k → inputnn1-i1 j k ≡ true) (sym (nn07 i 0 refl)) (sym (nn09 i)) (nn04 i)  where
      nn07 : (j x : ℕ) → x + j ≡ i  → proj1 ( inputnn1-i0 x (input-addi0 j (input-addi1 i))) ≡ x + j
-     nn07 zero x eq with input-addi1 i | inspect input-addi1 i
-     ... | [] | _ = +-comm 0 _
-     ... | i0 ∷ t | record { eq = eq1 } = ⊥-elim ( nn08 i eq1 ) where
+     nn07 zero x eq with input-addi1 i in eq1
+     ... | [] = +-comm 0 _
+     ... | i0 ∷ t = ⊥-elim ( nn08 i eq1 ) where
           nn08 : (i : ℕ) → ¬ (input-addi1 i ≡ i0 ∷ t )
           nn08 zero ()
           nn08 (suc i) ()
-     ... | i1 ∷ t | _ = +-comm 0 _
+     ... | i1 ∷ t = +-comm 0 _
      nn07 (suc j) x eq = trans (nn07 j (suc x) (trans (cong (λ k → k + j) (+-comm 1 _ )) (trans (+-assoc x _ _) eq)) )
                                                (trans (+-assoc 1 x _) (trans (cong (λ k → k + j) (+-comm 1 _) ) (+-assoc x 1 _) ))
      nn09 : (x : ℕ) → proj2 ( inputnn1-i0 0 (input-addi0 x (input-addi1 i))) ≡ input-addi1 i
-     nn09 zero with input-addi1 i | inspect input-addi1 i
-     ... | [] | _ = refl
-     ... | i0 ∷ t | record { eq = eq1 } = ⊥-elim ( nn08 i eq1 ) where
+     nn09 zero with input-addi1 i in eq1
+     ... | [] = refl
+     ... | i0 ∷ t = ⊥-elim ( nn08 i eq1 ) where
           nn08 : (i : ℕ) → ¬ (input-addi1 i ≡ i0 ∷ t )
           nn08 zero ()
           nn08 (suc i) ()
-     ... | i1 ∷ t | _ = refl
+     ... | i1 ∷ t = refl
      nn09 (suc j) = trans (nn30 (input-addi0 j (input-addi1 i)) 0) (nn09 j )
      nn04 : (i : ℕ) → inputnn1-i1 i (input-addi1 i) ≡ true
      nn04 zero = refl
@@ -267,7 +271,7 @@
                     nn18 (i0 ∷ t) eq = t
                     nn19 : (a : List In2 ) → (eq : i0 ∷ x₁ ≡ a ++ ( i1 ∷ i0 ∷ i1i0.b li)  )
                        → x₁ ≡ nn18 a eq ++ i1 ∷ i0 ∷ i1i0.b li
-                    nn19 (i0 ∷ a) eq = cons-inject eq
+                    nn19 (i0 ∷ a) eq = cons-inject In2 eq
                nn17 (i1 ∷ x₁) i eq li = nn20 (i1 ∷ x₁) i eq li where
                     -- second half
                     nn20 : (x : List In2) → (i : ℕ) → inputnn1-i1 i x ≡ true → i1i0 x → ⊥
@@ -281,7 +285,7 @@
                        nn21 (x ∷ a) (i0 ∷ x₁) (suc i) () eq0
                        nn21 [] (i1 ∷ i0 ∷ x₁) (suc zero) () eq0
                        nn21 [] (i1 ∷ i0 ∷ x₁) (suc (suc i)) () eq0
-                       nn21 (i1 ∷ a) (i1 ∷ x₁) (suc i) eq1 eq0 = nn21 a x₁ i eq1 (cons-inject eq0)
+                       nn21 (i1 ∷ a) (i1 ∷ x₁) (suc i) eq1 eq0 = nn21 a x₁ i eq1 (cons-inject In2 eq0)
           nn11 : (x y z : List In2 ) → ¬ y ≡ [] → inputnn1  (x ++ y ++ z) ≡ true → ¬ ( inputnn1  (x ++ y ++ y ++ z) ≡ true )
           nn11 x y z ny xyz xyyz = ⊥-elim ( nn12 (x ++ y ++ y ++ z ) xyyz record { a = x ++ i1i0.a (bb23 bb22 )
                                                  ; b = i1i0.b (bb23 bb22) ++ z ; i10 = bb24 } )  where
@@ -313,19 +317,20 @@
                -- this takes very long time to check and needs 10GB
                bb22 : count0 y ≡ count1 y
                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))    ∎ ))) ⟩
+                    count0 y ≡⟨ ? ⟩
+--                     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
@@ -366,9 +371,9 @@
                     (x ++ i1i0.a (bb23 bb22)) ++ i1 ∷ i0 ∷ i1i0.b (bb23 bb22) ++ z ∎ where open ≡-Reasoning
 
           nn10 : (x y z : List In2 ) → ¬ y ≡ [] → inputnn1  (x ++ y ++ z) ≡ true → inputnn1  (x ++ y ++ y ++ z) ≡ false
-          nn10 x y z my eq with inputnn1  (x ++ y ++ y ++ z)  | inspect inputnn1  (x ++ y ++ y ++ z)
-          ... | true | record { eq = eq1 } = ⊥-elim ( nn11 x y z my eq eq1 )
-          ... | false | _ = refl
+          nn10 x y z my eq with inputnn1  (x ++ y ++ y ++ z)  in eq1
+          ... | true = ⊥-elim ( nn11 x y z my eq eq1 )
+          ... | false  = refl
 
 
 
diff -r dfaf230f7b9a -r af8f630b7e60 automaton-in-agda/src/prime.agda
--- a/automaton-in-agda/src/prime.agda	Sun Sep 24 13:20:31 2023 +0900
+++ b/automaton-in-agda/src/prime.agda	Sun Sep 24 18:02:04 2023 +0900
@@ -1,3 +1,5 @@
+{-# OPTIONS --cubical-compatible --safe #-}
+
 module prime where
 
 open import Data.Nat 
diff -r dfaf230f7b9a -r af8f630b7e60 automaton-in-agda/src/pumping.agda
--- a/automaton-in-agda/src/pumping.agda	Sun Sep 24 13:20:31 2023 +0900
+++ b/automaton-in-agda/src/pumping.agda	Sun Sep 24 18:02:04 2023 +0900
@@ -1,3 +1,5 @@
+{-# OPTIONS --cubical-compatible --safe #-}
+
 module pumping where
 
 open import Data.Nat
@@ -115,10 +117,10 @@
    open TA
    tra-phase2 : (q : Q)  → (is : List Σ)  → (tr : Trace fa is  q )
        → phase2 finq qd (tr→qs fa is q tr) ≡ true → TA1 fa finq q qd is
-   tra-phase2 q (i ∷ is) (tnext q tr) p with equal? finq qd q | inspect ( equal? finq qd) q
-   ... | true | record { eq = eq } = record { y = [] ; z = i ∷ is ; yz=is = refl ; q=qd = qd-nil q (tnext q tr) eq
+   tra-phase2 q (i ∷ is) (tnext q tr) p with equal? finq qd q in eq
+   ... | true = record { y = [] ; z = i ∷ is ; yz=is = refl ; q=qd = qd-nil q (tnext q tr) eq
         ; trace-z  = subst (λ k → Trace fa (i ∷ is) k ) (sym (equal→refl finq eq)) (tnext q tr) ; trace-yz = tnext q tr }
-   ... | false | record { eq = ne } = record { y = i ∷ TA1.y ta ; z = TA1.z ta ; yz=is = cong (i ∷_ ) (TA1.yz=is ta )
+   ... | false = record { y = i ∷ TA1.y ta ; z = TA1.z ta ; yz=is = cong (i ∷_ ) (TA1.yz=is ta )
        ; q=qd = tra-08
        ; trace-z = TA1.trace-z ta ; trace-yz = tnext q ( TA1.trace-yz ta ) } where
             ta : TA1 fa finq (δ fa q i) qd is
@@ -126,10 +128,10 @@
             tra-07 : Trace fa (TA1.y ta ++ TA1.z ta) (δ fa q i)
             tra-07 = subst (λ k → Trace fa k (δ fa q i)) (sym (TA1.yz=is ta)) tr
             tra-08 : QDSEQ finq qd (TA1.z ta) (tnext q (TA1.trace-yz ta))
-            tra-08 = qd-next (TA1.y ta) q (TA1.trace-yz (tra-phase2 (δ fa q i) is tr p))  ne (TA1.q=qd ta)
+            tra-08 = qd-next (TA1.y ta) q (TA1.trace-yz (tra-phase2 (δ fa q i) is tr p)) eq (TA1.q=qd ta)
    tra-phase1 : (q : Q)  → (is : List Σ)  → (tr : Trace fa is  q ) → phase1 finq qd (tr→qs fa is q tr) ≡ true  → TA fa q is
-   tra-phase1 q (i ∷ is) (tnext q tr) p with equal? finq qd q | inspect (equal? finq qd) q
-   ... | true | record { eq = eq } = record { x = [] ; y = i ∷ TA1.y ta ;  z = TA1.z ta ; xyz=is =  cong (i ∷_ ) (TA1.yz=is ta)
+   tra-phase1 q (i ∷ is) (tnext q tr) p with equal? finq qd q in eq
+   ... | true = record { x = [] ; y = i ∷ TA1.y ta ;  z = TA1.z ta ; xyz=is =  cong (i ∷_ ) (TA1.yz=is ta)
            ; non-nil-y = λ ()
            ; trace-xyz  = tnext q (TA1.trace-yz ta)
            ; trace-xyyz = tnext q tra-05 } where
@@ -145,16 +147,16 @@
         tra-04 : (y2 : List Σ) → (q : Q) → (tr : Trace fa (y2 ++ z1) q)
                →  QDSEQ finq qd z1 {q} {y2} tr 
                → Trace fa (y2 ++ (i ∷ y1) ++ z1) q
-        tra-04 [] q tr (qd-nil q _ x₁) with equal? finq qd q | inspect (equal? finq qd) q
-        ... | true | record { eq = eq } = subst (λ k → Trace fa (i ∷ y1 ++ z1) k) (equal→refl finq eq) tryz
-        ... | false | record { eq = ne } = ⊥-elim ( ¬-bool  refl x₁ ) 
-        tra-04 (y0 ∷ y2) q (tnext q tr) (qd-next _ _  _ x₁ qdseq) with equal? finq qd q | inspect (equal? finq qd) q
-        ... | true | record { eq = eq } = ⊥-elim ( ¬-bool x₁ refl ) 
-        ... | false | record { eq = ne } = tnext q (tra-04 y2 (δ fa q y0) tr qdseq ) 
+        tra-04 [] q tr (qd-nil q _ x₁) with equal? finq qd q in eq
+        ... | true = subst (λ k → Trace fa (i ∷ y1 ++ z1) k) (equal→refl finq eq) tryz
+        ... | false = ⊥-elim ( ¬-bool  refl x₁ ) 
+        tra-04 (y0 ∷ y2) q (tnext q tr) (qd-next _ _  _ x₁ qdseq) with equal? finq qd q in eq
+        ... | true = ⊥-elim ( ¬-bool x₁ refl ) 
+        ... | false = tnext q (tra-04 y2 (δ fa q y0) tr qdseq ) 
         tra-05 : Trace fa (TA1.y ta ++ (i ∷ TA1.y ta) ++ TA1.z ta) (δ fa q i)
         tra-05 with equal→refl finq eq
         ... | refl = tra-04 y1  (δ fa qd i) (TA1.trace-yz ta) (TA1.q=qd ta)
-   ... | false | _ = record { x = i ∷ x ta ; y = y ta ; z = z ta ; xyz=is = cong (i ∷_ ) (xyz=is ta) 
+   ... | false = record { x = i ∷ x ta ; y = y ta ; z = z ta ; xyz=is = cong (i ∷_ ) (xyz=is ta) 
            ; non-nil-y = non-nil-y ta
             ; trace-xyz = tnext q (trace-xyz ta ) ; trace-xyyz = tnext q (trace-xyyz ta )} where
         ta : TA fa (δ fa q i ) is
diff -r dfaf230f7b9a -r af8f630b7e60 automaton-in-agda/src/pushdown.agda
--- a/automaton-in-agda/src/pushdown.agda	Sun Sep 24 13:20:31 2023 +0900
+++ b/automaton-in-agda/src/pushdown.agda	Sun Sep 24 18:02:04 2023 +0900
@@ -1,3 +1,5 @@
+{-# OPTIONS --cubical-compatible --safe #-}
+
 module pushdown where
 
 open import Level renaming ( suc to succ ; zero to Zero )
diff -r dfaf230f7b9a -r af8f630b7e60 automaton-in-agda/src/regex.agda
--- a/automaton-in-agda/src/regex.agda	Sun Sep 24 13:20:31 2023 +0900
+++ b/automaton-in-agda/src/regex.agda	Sun Sep 24 18:02:04 2023 +0900
@@ -1,4 +1,6 @@
-{-# OPTIONS --allow-unsolved-metas #-}
+{-# OPTIONS --cubical-compatible --safe #-}
+
+-- {-# OPTIONS --allow-unsolved-metas #-}
 module regex where
 
 open import Level renaming ( suc to succ ; zero to Zero )
diff -r dfaf230f7b9a -r af8f630b7e60 automaton-in-agda/src/regex2.agda
--- a/automaton-in-agda/src/regex2.agda	Sun Sep 24 13:20:31 2023 +0900
+++ b/automaton-in-agda/src/regex2.agda	Sun Sep 24 18:02:04 2023 +0900
@@ -1,4 +1,6 @@
-{-# OPTIONS --allow-unsolved-metas #-}
+{-# OPTIONS --cubical-compatible --safe #-}
+
+-- {-# OPTIONS --allow-unsolved-metas #-}
 
 open import Relation.Binary.PropositionalEquality hiding ( [_] )
 open import Relation.Nullary using (¬_; Dec; yes; no)
diff -r dfaf230f7b9a -r af8f630b7e60 automaton-in-agda/src/regular-language.agda
--- a/automaton-in-agda/src/regular-language.agda	Sun Sep 24 13:20:31 2023 +0900
+++ b/automaton-in-agda/src/regular-language.agda	Sun Sep 24 18:02:04 2023 +0900
@@ -1,3 +1,5 @@
+{-# OPTIONS --cubical-compatible --safe #-}
+
 module regular-language where
 
 open import Level renaming ( suc to Suc ; zero to Zero )
@@ -31,10 +33,10 @@
 Concat : {Σ : Set} → ( A B : language {Σ} ) → language {Σ}
 Concat {Σ} A B = split A B
 
-{-# TERMINATING #-}
-Star1 : {Σ : Set} → ( A : language {Σ} ) → language {Σ}
-Star1 {Σ} A [] = true
-Star1 {Σ} A (h ∷ t) = split A ( Star1 {Σ} A ) (h ∷ t)
+-- {-# TERMINATING #-}
+-- Star1 : {Σ : Set} → ( A : language {Σ} ) → language {Σ}
+-- Star1 {Σ} A [] = true
+-- Star0 {Σ} A (h ∷ t) = split A ( Star1 {Σ} A ) (h ∷ t)
 
 -- Terminating version of Star1
 --
diff -r dfaf230f7b9a -r af8f630b7e60 automaton-in-agda/src/root2.agda
--- a/automaton-in-agda/src/root2.agda	Sun Sep 24 13:20:31 2023 +0900
+++ b/automaton-in-agda/src/root2.agda	Sun Sep 24 18:02:04 2023 +0900
@@ -1,3 +1,5 @@
+{-# OPTIONS --cubical-compatible --safe #-}
+
 module root2 where
 
 open import Data.Nat 
@@ -86,7 +88,7 @@
     df = Dividable.factor dm
     dn : Dividable p n
     dn = divdable^2 n p 1<sp n>1 pn record { factor = df * df  ; is-factor = begin
-        df * df * p + 0  ≡⟨ *-cancelʳ-≡ _ _ {p0} ( begin 
+        df * df * p + 0  ≡⟨ *-cancelʳ-≡ _ _ (suc p0) ( begin 
           (df * df * p + 0) * p ≡⟨  cong (λ k → k * p)  (+-comm (df * df * p) 0)  ⟩
           ((df * df) * p  ) * p ≡⟨ cong (λ k → k * p) (*-assoc df df p ) ⟩
             (df * (df * p)) * p ≡⟨ cong (λ k → (df * k ) * p) (*-comm df p)  ⟩
@@ -196,7 +198,7 @@
       Rational.i r * Rational.i r  ∎ where open ≡-Reasoning
 
 *<-2 : {x y z : ℕ} → z > 0  → x < y → z * x < z * y   
-*<-2 {x} {y} {suc z} (s≤s z>0) x<y = *-monoʳ-< z x<y
+*<-2 {x} {y} {suc z} (s≤s z>0) x<y = ? -- *-monoʳ-< z x<y
 
 r15 : {p : ℕ} → p > 1 → p < p * p
 r15 {p} p>1 = subst (λ k → k < p * p ) m*1=m (*<-2 (<-trans a<sa p>1) p>1 )
diff -r dfaf230f7b9a -r af8f630b7e60 automaton-in-agda/src/sbconst2.agda
--- a/automaton-in-agda/src/sbconst2.agda	Sun Sep 24 13:20:31 2023 +0900
+++ b/automaton-in-agda/src/sbconst2.agda	Sun Sep 24 18:02:04 2023 +0900
@@ -1,3 +1,5 @@
+-- {-# OPTIONS --cubical-compatible --safe #-}
+
 module sbconst2 where
 
 open import Level renaming ( suc to succ ; zero to Zero )