--- 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
 --