Mercurial > hg > Members > kono > Proof > automaton

changeset 412:b85402051cdb default tip

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add mul
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 05 Apr 2024 13:38:20 +0900
parents 207e6c4e155c
children
files a11/lecture.ind a13/lecture.ind automaton-in-agda/src/cfg1.agda automaton-in-agda/src/derive.agda automaton-in-agda/src/deriveUtil.agda automaton-in-agda/src/finiteSet.agda automaton-in-agda/src/flcagl.agda automaton-in-agda/src/halt.agda automaton-in-agda/src/mul.agda automaton-in-agda/src/non-regular.agda automaton-in-agda/src/omega-automaton.agda automaton-in-agda/src/regular-concat.agda automaton-in-agda/src/regular-language.agda
diffstat 13 files changed, 383 insertions(+), 174 deletions(-) [+]
line wrap: on
line diff
--- a/a11/lecture.ind	Wed Nov 29 17:40:55 2023 +0900
+++ b/a11/lecture.ind	Fri Apr 05 13:38:20 2024 +0900
@@ -6,43 +6,6 @@
 
 例えば、信号機は停まらずにずーっと動くことが期待されていて、正しい信号機の動作とそうでない動作がある。そして信号機はオートマトン的に動作している。
 
---ωオートマトンの定義
-
-オートマトンの定義は同じものを用いる。ただし、入力は無限にある。
-
-    record Automaton ( Q : Set ) ( Σ : Set  )
-           : Set  where
-        field
-            δ : Q → Σ → Q
-            astart : Q
-            aend : Q → Bool
-
-automaton の定義にはもともと入力の実装が何かは記述されていない。
-
-Agda では無限の長さのリストを扱うことはできない。その代わり、自然数 n から入力Σを生成する関数( ℕ → Σ )を用いる。
-これを用いて、
-
-
-    ω-run : { Q  Σ : Set } → (Ω : Automaton Q Σ ) →  ℕ → ( ℕ → Σ )  → Q
-    ω-run Ω zero s = astart Ω
-    ω-run Ω (suc n) s = δ Ω (ω-run Ω n s) ( s n )
-
-と言う形でオートマトンが無限に実行される。
-
-この無限長の入力をどう受け付けるかを定義する必要がある。これには二通りの方法がある。
-
-    record Buchi { Q  Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) : Set where
-        field
-            from : ℕ
-            stay : (n : ℕ ) → n > from → aend Ω ( ω-run Ω n S ) ≡ true
-
-    record Muller { Q  Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) : Set where
-        field
-            next     : (n : ℕ ) → ℕ 
-            infinite : (n : ℕ ) →  aend Ω ( ω-run Ω (n + (next n)) S ) ≡ true 
-
-Buchi ではある時刻から先では、aend で定義される状態の集合にずーっと留まる。Muller ではaendで定義されるある状態の集合を無限回通る。
-
 --ωオートマトンと様相論理
 
 これらは時間の様相を表す論理に関係している。
@@ -92,12 +55,55 @@
          ;  aend = mark1
       }  
 
-ここで、[] <> p *  ( 上では ts* ) を無限回通れば、 [] <> p が成立していることになる。(Muller automaton )
+ここで、[] <> p *  ( 上では ts* ) を無限回通れば、 [] <> p が成立していることになる。(Buchi automaton )
+
+これの否定は、<> [] ( ¬ p ) ということになる。これは、ある時点からずーっと ¬ p が続く。(Muller automaton )
+
+--ωオートマトンの定義
+
+オートマトンの定義は同じものを用いる。ただし、入力は無限にある。
 
-これの否定は、<> [] ( ¬ p ) ということになる。これは、ある時点からずーっと ¬ p が続く。(Buchi automaton )
+    record Automaton ( Q : Set ) ( Σ : Set  )
+           : Set  where
+        field
+            δ : Q → Σ → Q
+            astart : Q
+            aend : Q → Bool
+
+automaton の定義にはもともと入力の実装が何かは記述されていない。
+
+Agda では無限の長さのリストを扱うことはできない。その代わり、自然数 n から入力Σを生成する関数( ℕ → Σ )を用いる。
+これを用いて、
 
 
+    ω-run : { Q  Σ : Set } → (Ω : Automaton Q Σ ) →  ℕ → ( ℕ → Σ )  → Q
+    ω-run Ω zero s = astart Ω
+    ω-run Ω (suc n) s = δ Ω (ω-run Ω n s) ( s n )
+
+と言う形でオートマトンが無限に実行される。
+
+この無限長の入力をどう受け付けるかを定義する必要がある。これには二通りの方法がある。
+
+    record Muller { Q  Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) : Set where
+        field
+            from : ℕ
+            stay : (x : Q) → (n : ℕ ) → n > from → aend Ω ( ω-run Ω x S n ) ≡ true
+
+    record Buchi { Q  Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) : Set where
+        field
+            next     : (n : ℕ ) → ℕ
+            infinite : (x : Q) → (n : ℕ ) →  aend Ω ( ω-run Ω x  S (n + (suc (next n)))) ≡ true
 
 
+Muller ではある時刻から先では、aend で定義される状態の集合にずーっと留まる。Buchi ではaendで定義されるある状態の集合を無限回通る。
 
+--Muller automaton と Buchi automaton の関係
 
+    B→M : { Q  Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) → Q 
+        → Muller Ω S → ¬ ( Buchi record { δ = δ Ω ; aend = λ q → not (aend Ω q)} S )
+
+    M→B : { Q  Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) → Q 
+        → Buchi Ω S → ¬ ( Muller record { δ = δ Ω ; aend = λ q → not (aend Ω q)} S )
+
+これが証明できる
+
--- a/a13/lecture.ind	Wed Nov 29 17:40:55 2023 +0900
+++ b/a13/lecture.ind	Fri Apr 05 13:38:20 2024 +0900
@@ -22,6 +22,8 @@
 
 Javaのモデル検査器。Thread を見てくれる。
 
+<a href="https://ie.u-ryukyu.ac.jp/~kono/lecture/os/ex/problem/265.html"> JavaPathFinder </a>
+
 --CPAcheker
 
 Cで書いたプログラムを検証してくれる
--- a/automaton-in-agda/src/cfg1.agda	Wed Nov 29 17:40:55 2023 +0900
+++ b/automaton-in-agda/src/cfg1.agda	Fri Apr 05 13:38:20 2024 +0900
@@ -60,6 +60,10 @@
   split (λ t1 → x (  h ∷ t1 ))  (λ t2 → y t2 ) t
 
 
+--
+-- we can rewrite cfg-language without Termination check violation
+--
+
 cfg-language0 :  {Symbol  : Set} → CFGGrammer Symbol   → Body Symbol  →  List Symbol → Bool
 
 {-# TERMINATING #-}
--- a/automaton-in-agda/src/derive.agda	Wed Nov 29 17:40:55 2023 +0900
+++ b/automaton-in-agda/src/derive.agda	Fri Apr 05 13:38:20 2024 +0900
@@ -66,7 +66,8 @@
 derive-step r d0 s = derive (is-derived d0) s refl
 
 regex→automaton : (r : Regex   Σ) → Automaton (Derivative r) Σ
-regex→automaton r = record { δ = λ d s → record { state = derivative (state d) s ; is-derived = derive (is-derived d) s refl } 
+regex→automaton r = record { δ = λ d s → 
+        record { state = derivative (state d) s ; is-derived = derive (is-derived d) s refl } 
    ; aend = λ d → empty? (state d) }  
 
 regex-match : (r : Regex   Σ) →  (List Σ) → Bool
@@ -183,6 +184,21 @@
         s : Regex Σ
         is-sub : SB r s
 
+SubtermS : (x : Regex Σ ) → Set
+SubtermS x =  (y : Regex Σ) → SB x y → Bool
+
+nderivative :  (x : Regex  Σ) → SubtermS x → Σ → SubtermS x
+nderivative = ?
+
+open import nfa
+
+regex→nautomaton : (r : Regex   Σ) → NAutomaton ? Σ
+regex→nautomaton r = record { δ = λ d s → record { state = derivative (state d) s ; is-derived = derive (is-derived d) s refl } 
+   ; aend = λ d → empty? (state d) }  
+
+regex-nmatch : (r : Regex   Σ) →  (List Σ) → Bool
+regex-nmatch ex is = ? -- accept ( regex→nautomaton ex ) record { state =  ex ; is-derived = unit refl } is 
+
 open import bijection using ( InjectiveF ; Is )  
 
 finISB : (r : Regex Σ) → FiniteSet (ISB r)
@@ -396,4 +412,23 @@
 
 
 
+---
+--     empty?  ((< a > * || < b > * ) & < c > )  = falsee
+--
+--     derive  ((< a > * || < b > * ) & < c > ) a   = < a > * & < c >
+--     derive  ((< a > * || < b > * ) & < c > ) b   = < b > * & < c >
+--     derive  ((< a > * || < b > * ) & < c > ) c   = ε
+--     derive  ((< a > * || < b > * ) & < c > ) d   = φ
+--     
+--     empty?  ((< a > * ) & < c > )  = falsee
+--     derive  (< a > * & < c > ) a = < a > * & < c >
+--     derive  (< a > * & < c > ) b = φ
+--     derive  (< a > * & < c > ) c = ε
+--     derive  (< a > * & < c > ) d = φ
+--
+--     empty?  ((< b > * ) & < c > )  = falsee
+--     derive  (< b > * & < c > ) a = φ
+--     derive  (< b > * & < c > ) b = < b > * & < c >
+--     derive  (< b > * & < c > ) c = ε
+--     derive  (< b > * & < c > ) d = φ
 
--- a/automaton-in-agda/src/deriveUtil.agda	Wed Nov 29 17:40:55 2023 +0900
+++ b/automaton-in-agda/src/deriveUtil.agda	Fri Apr 05 13:38:20 2024 +0900
@@ -1,4 +1,4 @@
-{-# OPTIONS --cubical-compatible --safe #-}
+-- {-# OPTIONS --cubical-compatible safe #-}
 
 module deriveUtil where
 
--- a/automaton-in-agda/src/finiteSet.agda	Wed Nov 29 17:40:55 2023 +0900
+++ b/automaton-in-agda/src/finiteSet.agda	Fri Apr 05 13:38:20 2024 +0900
@@ -40,3 +40,12 @@
      equal? q0 q1 with F←Q q0 ≟ F←Q q1
      ... | yes p = true
      ... | no ¬p = false
+
+record FiniteSetF ( Q : Set ) : Set  where
+     field
+        finite : ℕ
+        Q←F : Fin finite → Q → Bool
+        F←Q : (Q → Bool) → Fin finite
+        finiso→ : (f : Q → Bool ) → (q : Q) → Q←F ( F←Q f ) q ≡ f q
+        finiso← : (f : Fin finite ) → F←Q ( Q←F f )  ≡ f 
+
--- a/automaton-in-agda/src/flcagl.agda	Wed Nov 29 17:40:55 2023 +0900
+++ b/automaton-in-agda/src/flcagl.agda	Fri Apr 05 13:38:20 2024 +0900
@@ -8,7 +8,7 @@
 --          bb : (y : aaa) → aaa
 --          cc : (y : aaa) → aaa
 --
---     Lang : {Σ : Set } → List Σ → Bool
+--     Lang : {Σ : Set } → Colist Σ → Bool
 --     Lang [] = ?
 --     Lang (h ∷ t)  = ?
 --     
@@ -46,28 +46,29 @@
 open import Level renaming ( zero to Zero ; suc to succ )
 open import Size 
 open import Data.Empty
+open import Data.List hiding (map ; foldr ; any)
 
-module List where
+module Colist where
 
-        data List (i : Size) (A : Set) : Set where
-          [] : List i A
-          _∷_ : {j : Size< i} (x : A) (xs : List j A) → List i A
+        data Colist (i : Size) (A : Set) : Set where
+          [] : Colist i A
+          _∷_ : {j : Size< i} (x : A) (xs : Colist j A) → Colist i A
 
 
-        map : ∀{i A B} → (A → B) → List i A → List i B
+        map : ∀{i A B} → (A → B) → Colist i A → Colist i B
         map f [] = []
         map f ( x ∷ xs)= f x ∷ map f xs
 
-        foldr : ∀{i} {A B : Set} → (A → B → B) → B → List i A → B
+        foldr : ∀{i} {A B : Set} → (A → B → B) → B → Colist i A → B
         foldr c n [] = n
         foldr c n (x ∷ xs) = c x (foldr c n xs)
 
-        any : ∀{i A} → (A → Bool) → List i A → Bool
+        any : ∀{i A} → (A → Bool) → Colist i A → Bool
         any p xs = foldr _∨_ false (map p xs)
 
 module Lang where
 
-        open List 
+        open Colist 
 
         -- Lnag ≅ Bool × (Σ → Lang)
         --
@@ -79,15 +80,19 @@
 
         open Lang
 
-        _∋_ : ∀{i} → Lang i → List i A → Bool
+        _∋_ : ∀{i} → Lang i → Colist i A → Bool
         l ∋ [] = ν l
         l ∋ ( a ∷ as ) = δ l a ∋ as
 
-        trie : ∀{i}  (f : List i A → Bool) → Lang i
+        trie : ∀{i}  (f : Colist i A → Bool) → Lang i
         ν (trie f) = f []
         δ (trie f) a = trie (λ as → f (a ∷ as))
 
-        -- trie' : ∀{i}  (f : List i A → Bool) → Lang i
+        -- _∋'_ : ∀{i} → Lang i → List A → Bool
+        -- l ∋' [] = ν l
+        -- l ∋' ( a ∷ as ) = δ l a ∋' as
+
+        -- trie' : ∀{i}  (f : Colist i A → Bool) → Lang i
         -- trie' {i} f = record { 
         --     ν = f []
         --   ; δ = λ {j} a → lem {j} a   -- we cannot write in this way
@@ -124,31 +129,41 @@
         δ (k · l) x = let k′l =  δ k x  · l in if ν k then k′l ∪ δ l x else k′l
 
         _+_ : ∀{i}  (k l : Lang i) → Lang i
-        ν (k + l) = ν k ∧ ν l
-        δ (k + l) x with ν k | ν l
-        ... | false | true = δ k x  + l 
-        ... | false | false = δ k x  + l 
-        ... | true  | true = (δ k x  + l )  ∪ δ l x 
-        ... | true  | false = (δ k x  + l )  ∪ δ l x 
+        ν (k + l) = ν l
+        δ (k + l) x with ν k 
+        ... | false = δ k x  + l 
+        ... | true  = (δ k x  + l )  ∪ δ l x 
 
         language : { Σ : Set } → Set
-        language {Σ}  = List ∞ Σ → Bool
+        language {Σ}  = Colist ∞ Σ → Bool
 
         split : {Σ : Set} → {i : Size } → (x y : language {Σ} ) → language {Σ}
-        split x y  [] = x [] ∨  y []
+        split x y  [] = x [] ∧  y []
         split x y (h  ∷ t) = (x [] ∧ y (h  ∷ t)) ∨
           split (λ t1 → x (  h ∷ t1 ))  (λ t2 → y t2 ) t
 
-        LtoSplit : (x y : Lang ∞ ) → (z : List ∞ A) → ((x  + y ) ∋ z) ≡ true →   split (λ w → x ∋ w) (λ w → y ∋ w) z ≡ true
-        LtoSplit x y [] xy with ν x | ν y
-        ... | true | true = refl
+        data In2 : Set where
+          i0 : In2
+          i1 : In2
+
+        test-AB→split : {Σ : Set} → {A B : Colist ∞ In2 → Bool} → split A B ( i0 ∷ i1 ∷ i0 ∷ [] ) ≡ (
+           ( A [] ∧ B ( i0 ∷ i1 ∷ i0 ∷ [] ) ) ∨
+           ( A ( i0 ∷ [] ) ∧ B ( i1 ∷ i0 ∷ [] ) ) ∨
+           ( A ( i0 ∷ i1 ∷ [] ) ∧ B ( i0 ∷ [] ) ) ∨
+           ( A ( i0 ∷ i1 ∷ i0 ∷ [] ) ∧ B  []  )
+            )
+        test-AB→split {_} {A} {B} = ?
+
+        LtoSplit : (x y : Lang ∞ ) → (z : Colist ∞ A) → ((x  ·  y ) ∋ z) ≡ true →   split (λ w → x ∋ w) (λ w → y ∋ w) z ≡ true
+        LtoSplit x y [] xy with ν x 
+        ... | true = xy
         LtoSplit x y (h ∷ z) xy = ?
 
-        SplitoL : (x y : Lang ∞ ) → (z : List ∞ A) → ((x  + y ) ∋ z) ≡ false →   split (λ w → x ∋ w) (λ w → y ∋ w) z ≡ false
+        SplitoL : (x y : Lang ∞ ) → (z : Colist ∞ A) → ((x  ·  y ) ∋ z) ≡ false →   split (λ w → x ∋ w) (λ w → y ∋ w) z ≡ false
         SplitoL x y [] xy with ν x | ν y 
         ... | false | false = refl
-        ... | false | true = ?
-        ... | true | false = ?
+        ... | false | true = refl
+        ... | true | false = refl
         SplitoL x y (h ∷ z) xy = ?
 
 
@@ -225,10 +240,10 @@
         ≅ν (union-cong p q) = cong₂ _∨_ (≅ν p) (≅ν q)
         ≅δ (union-cong p q) a = union-cong (≅δ p a) (≅δ q a)
 
-        withExample : (P : Bool → Set) (p : P true) (q : P false) →
-           {A : Set} (g : A → Bool) (x : A) → P (g x) withExample P p q g x with g x
-        ... | true = p
-        ... | false = q
+        -- withExample : (P : Bool → Set) (p : P true) (q : P false) →
+        --    {A : Set} (g : A → Bool) (x : A) → P (g x) withExample P p q g x with g x
+        -- ... | true = p
+        -- ... | false = q
 
         rewriteExample : {A : Set} {P : A → Set} {x : A} (p : P x)
             {g : A → A} (e : g x ≡ x) → P (g x)
@@ -406,15 +421,15 @@
                 ∎ where open EqR (Bis _)
 
 
-open List
+open Colist
 
 record DA (S : Set) : Set where
     field ν : (s : S) → Bool
           δ : (s : S)(a : A) → S
-    νs : ∀{i} (ss : List.List i S) → Bool
-    νs ss = List.any ν ss
-    δs : ∀{i} (ss : List.List i S) (a : A) → List.List i S
-    δs ss a = List.map (λ s → δ s a) ss
+    νs : ∀{i} (ss : Colist.Colist i S) → Bool
+    νs ss = Colist.any ν ss
+    δs : ∀{i} (ss : Colist.Colist i S) (a : A) → Colist.Colist i S
+    δs ss a = Colist.map (λ s → δ s a) ss
 
 open Lang 
 
@@ -459,7 +474,7 @@
 ν (da1 ⊕ da2) (s1 , s2) = ν da1 s1 ∨ ν da2 s2
 δ (da1 ⊕ da2) (s1 , s2) a = δ da1 s1 a , δ da2 s2 a
 
-powA : ∀{S} (da : DA S) → DA (List ∞ S)
+powA : ∀{S} (da : DA S) → DA (Colist ∞ S)
 ν (powA da) ss = νs da ss
 δ (powA da) ss a = δs da ss a
 
@@ -469,12 +484,12 @@
 ≅ν (powA-nil da) = refl
 ≅δ (powA-nil da) a = powA-nil da
 
-powA-cons : ∀{i S} (da : DA S) {s : S} {ss : List ∞ S} →
+powA-cons : ∀{i S} (da : DA S) {s : S} {ss : Colist ∞ S} →
         lang (powA da) (s ∷ ss) ≅⟨ i ⟩≅ lang da s ∪ lang (powA da) ss
 ≅ν (powA-cons da) = refl
 ≅δ (powA-cons da) a = powA-cons da
 
-composeA : ∀{S1 S2} (da1 : DA S1)(s2 : S2)(da2 : DA S2) → DA (S1 × List ∞ S2)
+composeA : ∀{S1 S2} (da1 : DA S1)(s2 : S2)(da2 : DA S2) → DA (S1 × Colist ∞ S2)
 ν (composeA da1 s2 da2) (s1 , ss2) = (ν da1 s1 ∧ ν da2 s2) ∨ νs da2 ss2
 δ (composeA da1 s2 da2) (s1 , ss2) a =
         δ da1 s1 a , δs da2 (if ν da1 s1 then s2 ∷ ss2 else ss2) a
@@ -482,7 +497,7 @@
 -- import Relation.Binary.EqReasoning as EqR
 import Relation.Binary.Reasoning.Setoid as EqR
 
-composeA-gen : ∀{i S1 S2} (da1 : DA S1) (da2 : DA S2) → ∀(s1 : S1)(s2 : S2)(ss : List ∞ S2) →
+composeA-gen : ∀{i S1 S2} (da1 : DA S1) (da2 : DA S2) → ∀(s1 : S1)(s2 : S2)(ss : Colist ∞ S2) →
         lang (composeA da1 s2 da2) (s1 , ss) ≅⟨ i ⟩≅ lang da1 s1 · lang da2 s2 ∪ lang (powA da2) ss
 ≅ν (composeA-gen da1 da2 s1 s2 ss) = refl
 ≅δ (composeA-gen da1 da2 s1 s2 ss) a with ν da1 s1
@@ -513,14 +528,14 @@
 
 
 
-finalToInitial : ∀{S} (da : DA (Maybe S)) → DA (List ∞ (Maybe S))
+finalToInitial : ∀{S} (da : DA (Maybe S)) → DA (Colist ∞ (Maybe S))
 ν (finalToInitial da) ss = νs da ss
 δ (finalToInitial da) ss a =
         let ss′ = δs da ss a
         in if νs da ss then δ da nothing a ∷ ss′ else ss′
 
 
-starA : ∀{S}(s0 : S)(da : DA S) → DA (List ∞(Maybe S))
+starA : ∀{S}(s0 : S)(da : DA S) → DA (Colist ∞(Maybe S))
 starA s0 da = finalToInitial (acceptingInitial s0 da)
 
 
@@ -529,12 +544,22 @@
    lang (acceptingInitial s0 da) (just s) ≅⟨ i ⟩≅ lang da s
  acceptingInitial-nothing : ∀{i S} (s0 : S) (da : DA S) →
         lang (acceptingInitial s0 da) nothing ≅⟨ i ⟩≅ ε ∪ lang da s0
- starA-lemma : ∀{i S}(da : DA S)(s0 : S)(ss : List ∞ (Maybe S))→
+ starA-lemma : ∀{i S}(da : DA S)(s0 : S)(ss : Colist ∞ (Maybe S))→
         lang (starA s0 da) ss ≅⟨ i ⟩≅ 
                 lang (powA (acceptingInitial s0 da)) ss · (lang da s0) *
  starA-correct : ∀{i S} (da : DA S) (s0 : S) →
    lang (starA s0 da) (nothing ∷ []) ≅⟨ i ⟩≅ (lang da s0) *
 
+record Automaton ( Q : Set ) ( Σ : Set  )
+       : Set  where
+    field
+        δ : Q → Σ → Q
+        aend : Q → Bool
+
+accept : ∀{i} {S} (da : Automaton S A) (s : S) → Lang i
+Lang.ν (accept da s) = Automaton.aend da s
+Lang.δ (accept da s) a = accept da (Automaton.δ da s a)
+
 record NAutomaton ( Q : Set ) ( Σ : Set  )
            : Set  where
         field
--- a/automaton-in-agda/src/halt.agda	Wed Nov 29 17:40:55 2023 +0900
+++ b/automaton-in-agda/src/halt.agda	Fri Apr 05 13:38:20 2024 +0900
@@ -25,7 +25,7 @@
        ffun→  :  (R → Bool) → S
        ffiso← : (f : R → Bool ) → (x : R)  → ffun← ( ffun→ f ) x ≡ f x 
 
-       -- ffun← ( ffun→ f )  ≡ f , if we have functional extensionality  but it is unsafe
+--       ffiso→ : (x : S)  → ffun→  ( ffun←  x ) ≡ x -- , if we have functional extensionality  but it is unsafe
 
 open FBijection 
 
@@ -86,6 +86,9 @@
 
 open Halt
 
+--
+--   List boot <-> ( List Bool → Bool )
+--
 TNLF : (halt : Halt ) → (utm : UTM) → FBijection (List Bool) (List Bool)
 TNLF halt utm = record {
        ffun←  = λ tm x → Halt.halt halt (UTM.utm utm) (tm ++ x)
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/automaton-in-agda/src/mul.agda	Fri Apr 05 13:38:20 2024 +0900
@@ -0,0 +1,122 @@
+module mul where
+
+open import  Relation.Binary.PropositionalEquality
+
+data ℕ : Set where
+  zero : ℕ
+  suc : ℕ → ℕ
+
+lemmm00 : ℕ
+lemmm00 = suc (suc zero)
+
+_+_ : ℕ → ℕ → ℕ
+zero + y = y
+suc x + y = suc (x + y)
+
+_*_ : ℕ → ℕ → ℕ
+zero * y = zero
+suc x * y = y + (x * y)
+
+lemmm01 : ℕ
+lemmm01 = suc (suc zero) + suc (suc zero)
+
++-comm : ∀ x y → (x + y) ≡ (y + x)
++-comm zero zero = refl
++-comm zero (suc y) = cong suc (+-comm zero y)
++-comm (suc x) zero = cong suc (+-comm x zero)
++-comm (suc x) (suc y) = begin
+   suc (x + suc y)   ≡⟨ (cong suc (+-comm x (suc y))) ⟩
+   suc (suc (y + x)) ≡⟨  cong suc (cong suc (+-comm y x)) ⟩
+   suc (suc (x + y)) ≡⟨  cong suc ( +-comm (suc x) y) ⟩
+   suc (y + suc x) ∎ where open ≡-Reasoning
+
++-assoc : ∀ x y z → (x + (y + z)) ≡ ((x + y) + z)
++-assoc zero y z = refl
++-assoc (suc x) y z = cong suc (+-assoc x y z)
+   
+*-distr-r : {y x z : ℕ } → (y * z) + (x * z) ≡ ((y + x) * z)
+*-distr-r {zero} {x} {z} = refl
+*-distr-r {suc y} {x} {z} = trans (sym (+-assoc z _ _)) (cong (λ k → z + k)(*-distr-r {y} {x} {z})) 
+
+*-distr-l : {y x z : ℕ } → (y * z) + (y * x) ≡ y * (z + x )
+*-distr-l {zero} {x}  = refl
+*-distr-l {suc y} {x} {z} = begin
+  (z + (y * z)) + (x + (y * x))  ≡⟨ +-assoc (z + (y * z)) x _ ⟩
+  ((z + (y * z)) + x) + (y * x)  ≡⟨ cong (λ k → k + (y * x)) (sym (+-assoc z _ _)) ⟩
+  (z + ((y * z) + x)) + (y * x)  ≡⟨ cong (λ k → (z + k) + (y * x)  ) (+-comm _ x) ⟩
+  (z + (x + (y * z))) + (y * x)  ≡⟨ cong (λ k → k + (y * x)) (+-assoc z _ _) ⟩
+  ((z + x) + (y * z)) + (y * x)  ≡⟨ sym (+-assoc (z + x) _ _) ⟩
+  (z + x) + ((y * z) + (y * x)) ≡⟨ cong (λ k → (z + x) + k) (*-distr-l {y} {x} {z}) ⟩
+  (z + x) + (y * (z + x)) ∎  where open ≡-Reasoning
+
+*-comm : ∀ x y → (x * y) ≡ (y * x)
+*-comm zero zero = refl
+*-comm zero (suc y) = *-comm zero y
+*-comm (suc x) y = lemma2 where 
+   lemma3 : {y : ℕ}　→  y ≡ (y * suc zero)
+   lemma3 {zero} = refl
+   lemma3 {suc y} = cong suc (lemma3 {y})
+   lemma2 : (y + (x * y)) ≡ (y * suc x)
+   lemma2 = begin
+      (y + (x * y)) ≡⟨ cong₂ (λ j k → j + k ) lemma3 (*-comm x y) ⟩
+      (y * suc zero) + (y * x) ≡⟨ *-distr-l {y} ⟩
+      y * suc x ∎ where open ≡-Reasoning
+
+*-assoc : ∀ x y z → (x * y) * z ≡ x * (y * z) 
+*-assoc zero y z = refl
+*-assoc (suc x) y z = begin
+    ((y + (x * y)) * z) ≡⟨ sym (*-distr-r {y} ) ⟩
+    (y * z) + ((x * y) * z) ≡⟨ cong (λ k → (y * z) + k) (*-assoc x y z) ⟩
+    (y * z) + (x * (y * z)) ∎ where open ≡-Reasoning
+
+_+ˡ_ : ℕ → ℕ → ℕ
+x +ˡ zero = x
+x +ˡ suc y = suc (x +ˡ y)
+
+theorem00 : ∀ x y → (x +ˡ y) ≡ (y + x)
+theorem00 x zero = refl
+theorem00 x (suc y) = cong suc (theorem00 x y)
+
+_*ˡ_ : ℕ → ℕ → ℕ
+x *ˡ zero = zero
+x *ˡ (suc y) = x +ˡ (x *ˡ y)
+
+                                      
+open import Data.Empty                                                
+open import Data.Unit                                                                         
+open import Relation.Nullary
+
+-- theorem000 : ¬ ( _*_ ≡ _*ˡ_ )
+-- theorem000 ()
+
+theorem01 : ∀ x y → (x *ˡ y) ≡ (y * x)
+theorem01 x zero = refl
+theorem01 x (suc y) = begin
+   (x *ˡ suc y) ≡⟨ refl ⟩
+   x +ˡ (x *ˡ y) ≡⟨ cong (λ k → x +ˡ k) (theorem01 x y) ⟩
+   x +ˡ (y * x) ≡⟨ theorem00 x _ ⟩
+   (y * x) + x ≡⟨ +-comm _ x ⟩
+   x + (y * x)  ∎ where open ≡-Reasoning
+
++ˡ-assoc : ∀ x y z → (x +ˡ (y +ˡ z)) ≡ ((x +ˡ y) +ˡ z)
++ˡ-assoc x y zero = refl
++ˡ-assoc x y (suc z) = cong suc (+ˡ-assoc x y z)
+   
+-- *ˡ-distr-l : {y x z : ℕ } → (y *ˡ z) +ˡ (y *ˡ x) ≡ y *ˡ (z +ˡ x )
+-- *ˡ-distr-l {y} {zero} {z} = refl
+-- *ˡ-distr-l {y} {suc x} {z} = trans ? (cong (λ k → y +ˡ k)(*ˡ-distr-l {y} {x} {z})) 
+
+
+theorem02 : ∀ x y → (x *ˡ y) ≡ (x * y)
+theorem02 x y = trans (theorem01 x y) (*-comm y x)
+
+-- record Monad (M : Set → Set) : Set₁ where
+--  field
+--    return : {A : Set} → A → M A
+--    _>>=_ : {A B : Set} → M A → (A → M B) → M B
+
+--*-Monad : { M : Set → Set } → Monad M → ℕ → ℕ → ℕ
+--*-Monad {M} m n n = ?
+
+
+
--- a/automaton-in-agda/src/non-regular.agda	Wed Nov 29 17:40:55 2023 +0900
+++ b/automaton-in-agda/src/non-regular.agda	Fri Apr 05 13:38:20 2024 +0900
@@ -40,6 +40,9 @@
 inputnn0 : ( n :  ℕ )  →  List  In2
 inputnn0 n = input-addi0 n (input-addi1 n)
 
+--
+--  using count of i0 and i1 makes the proof easier
+--
 inputnn1-i1 : (i : ℕ) → List In2 → Bool
 inputnn1-i1 zero [] = true
 inputnn1-i1 (suc _) [] = false
--- a/automaton-in-agda/src/omega-automaton.agda	Wed Nov 29 17:40:55 2023 +0900
+++ b/automaton-in-agda/src/omega-automaton.agda	Fri Apr 05 13:38:20 2024 +0900
@@ -1,3 +1,4 @@
+{-# OPTIONS --cubical-compatible --safe #-}
 module omega-automaton where
 
 open import Level renaming ( suc to succ ; zero to Zero )
@@ -19,14 +20,14 @@
 ω-run Ω x s (suc n) = δ Ω (ω-run Ω x s n) ( s n )
 
 --
--- accept as Buchi automaton
+-- accept as Muller automaton
 --
-record Buchi { Q  Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) : Set where
+record Muller { Q  Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) : Set where
     field
         from : ℕ
         stay : (x : Q) → (n : ℕ ) → n > from → aend Ω ( ω-run Ω x S n ) ≡ true
 
-open Buchi
+open Muller
 
 --  after sometimes, always p
 --
@@ -37,14 +38,14 @@
 --                       p
 
 --
--- accept as Muller automaton
+-- accept as Buchi automaton
 --
-record Muller { Q  Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) : Set where
+record Buchi { Q  Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) : Set where
     field
         next     : (n : ℕ ) → ℕ 
         infinite : (x : Q) → (n : ℕ ) →  aend Ω ( ω-run Ω x  S (n + (suc (next n)))) ≡ true 
 
-open  Muller 
+open  Buchi 
 --  always sometimes p
 --
 --                       not p 
@@ -56,12 +57,6 @@
 open import nat
 open import Data.Nat.Properties
 
--- LEMB : { Q  Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) → Q → Buchi Ω S ∨ (¬ ( Buchi Ω S ))
--- LEMB Ω S Q = {!!}  -- S need not to be constructive, so we have no constructive LEM
-
--- LEMM : { Q  Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) → Q → Muller Ω S ∨ (¬ ( Muller Ω S ))
--- LEMM = {!!}
-
 ω-run-eq : { Q  Σ : Set } → (Ω Ω' : Automaton Q Σ ) → (q : Q) →  ( S : ℕ → Σ )  → (x : ℕ)
     → δ Ω ≡ δ Ω'
     → ω-run Ω q S x ≡ ω-run Ω' q S x
@@ -77,7 +72,7 @@
 --
 
 
-B→M : { Q  Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) → Q → Buchi Ω S → ¬ ( Muller record { δ = δ Ω ; aend = λ q → not (aend Ω q)} S )
+B→M : { Q  Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) → Q → Muller Ω S → ¬ ( Buchi record { δ = δ Ω ; aend = λ q → not (aend Ω q)} S )
 B→M {Q} {Σ} Ω S q b m = ¬-bool bm04 bm02 where
    q1 : Q
    q1 = ω-run Ω q S (from b + suc (next m (from b)))
@@ -99,7 +94,7 @@
 -- [] <> p → ¬ <> [] ¬ p
 --
 
-M→B : { Q  Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) → Q → Muller Ω S → ¬ ( Buchi record { δ = δ Ω ; aend = λ q → not (aend Ω q)} S )
+M→B : { Q  Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) → Q → Buchi Ω S → ¬ ( Muller record { δ = δ Ω ; aend = λ q → not (aend Ω q)} S )
 M→B {Q} {Σ} Ω S q m b = ¬-bool bm04 bm02 where
    q1 : Q
    q1 = ω-run Ω q S (from b + suc (next m (from b)))
@@ -117,6 +112,23 @@
      not (aend Ω' (ω-run Ω' q S (from b + (suc (next m (from b)))))) ≡⟨ cong (λ k → not k ) bm03 ⟩
      false ∎  where open ≡-Reasoning
 
+open import finiteSet
+
+--    q₀ → q₁ → ... q 
+--    q₀ → q₁ → q₅ .... q₅  ... q 
+
+open FiniteSet
+
+descendSubset : { Q : Set } → (fin : FiniteSet Q) → ( I : Q → Bool) → ( P : Q → Bool ) 
+    → exists fin (λ q → I q /\ P q) ≡ true → Q → Bool
+descendSubset = ?
+
+is-Muller-valid : { Q  Σ : Set } (Ω : Automaton Q Σ ) → FiniteSet Q → Q → Dec ((S : ℕ → Σ) →  Muller Ω S) 
+is-Muller-valid = ?
+
+-- descendSubset monotonically descend
+-- derivation tree of Q will be constructed
+-- check contruction of Muller Ω S
 
 
 data  States3   : Set  where
@@ -127,6 +139,7 @@
 transition3 ts* true  = ts*
 transition3 ts* false  = ts
 transition3 ts true  = ts*
+
 transition3 ts false  = ts
 
 mark1 :  States3  → Bool
@@ -149,21 +162,21 @@
 flip-seq zero = false
 flip-seq (suc n) = not ( flip-seq n )
 
--- flip-seq is acceepted by Muller automaton ωa1 
+-- flip-seq is acceepted by Buchi automaton ωa1 
 
-lemma1 : Buchi ωa1 true-seq 
-lemma1 = record {
-        from = zero
-      ; stay = {!!}
-   } where
-      lem1 : ( n :  ℕ ) → n > zero → aend ωa1 (ω-run ωa1 {!!} true-seq n ) ≡ true
-      lem1 zero ()
-      lem1 (suc n) (s≤s z≤n) with ω-run ωa1 {!!} true-seq n
-      lem1 (suc n) (s≤s z≤n) | ts* = {!!}
-      lem1 (suc n) (s≤s z≤n) | ts = {!!}
+-- lemma1 : Muller ωa1 true-seq 
+-- lemma1 = record {
+--         from = zero
+--       ; stay = {!!}
+--    } where
+--       lem1 : ( n :  ℕ ) → n > zero → aend ωa1 (ω-run ωa1 {!!} true-seq n ) ≡ true
+--       lem1 zero ()
+--       lem1 (suc n) (s≤s z≤n) with ω-run ωa1 {!!} true-seq n
+--       lem1 (suc n) (s≤s z≤n) | ts* = {!!}
+--       lem1 (suc n) (s≤s z≤n) | ts = {!!}
 
-lemma0 : Muller ωa1 flip-seq 
-lemma0 = {!!}
+-- lemma0 : Buchi ωa1 flip-seq 
+-- lemma0 = {!!}
 
 ωa2 : Automaton States3 Bool
 ωa2 = record {
@@ -183,30 +196,30 @@
           ( not ( flip-seq n ) )
        ∎
 
-flip-dec2 : (n : ℕ ) → ? -- not flip-seq (suc n)  ≡  flip-seq n 
-flip-dec2 n = {!!}
+-- flip-dec2 : (n : ℕ ) → ? -- not flip-seq (suc n)  ≡  flip-seq n 
+-- flip-dec2 n = {!!}
 
 
-record flipProperty : Set where
-    field
-       flipP : (n : ℕ) →  ω-run ωa2 {!!} {!!} ≡ ω-run ωa2 {!!} {!!}
+-- record flipProperty : Set where
+--     field
+--        flipP : (n : ℕ) →  ω-run ωa2 {!!} {!!} ≡ ω-run ωa2 {!!} {!!}
 
-lemma2 : Muller ωa2 flip-seq 
-lemma2 = record {
-          next = next1
-       ;  infinite = {!!}
-   }  where
-     next1 : ℕ → ℕ
-     next1 = {!!}
-     infinite' : (n m : ℕ) → n ≥″ m → aend ωa2 {!!} ≡ true → aend ωa2 {!!} ≡ true
-     infinite' = {!!}
-     infinite2 : (n : ℕ) → aend ωa2 {!!} ≡ true
-     infinite2 = {!!}
-
-lemma3 : Buchi ωa1 false-seq  →  ⊥
-lemma3 = {!!}
-
-lemma4 : Muller ωa1 flip-seq  →  ⊥
-lemma4 = {!!}
-
-
+-- lemma2 : Buchi ωa2 flip-seq 
+-- lemma2 = record {
+--           next = next1
+--        ;  infinite = {!!}
+--    }  where
+--      next1 : ℕ → ℕ
+--      next1 = {!!}
+--      infinite' : (n m : ℕ) → n ≥″ m → aend ωa2 {!!} ≡ true → aend ωa2 {!!} ≡ true
+--      infinite' = {!!}
+--      infinite2 : (n : ℕ) → aend ωa2 {!!} ≡ true
+--      infinite2 = {!!}
+-- 
+-- lemma3 : Muller ωa1 false-seq  →  ⊥
+-- lemma3 = {!!}
+-- 
+-- lemma4 : Buchi ωa1 flip-seq  →  ⊥
+-- lemma4 = {!!}
+-- 
+-- 
--- a/automaton-in-agda/src/regular-concat.agda	Wed Nov 29 17:40:55 2023 +0900
+++ b/automaton-in-agda/src/regular-concat.agda	Fri Apr 05 13:38:20 2024 +0900
@@ -82,6 +82,7 @@
        exists finab (λ qn → nq qn /\ Nδ NFA qn h (abmove q h)) ≡ true
     nmove (case1 q) nq nqt h = found finab (case1 q) ( bool-and-tt nqt (lemma-nmove-ab (case1 q)  h) )  
     nmove (case2 q) nq nqt h = found finab (case2 q) ( bool-and-tt nqt (lemma-nmove-ab (case2 q) h) ) 
+
     acceptB : (z : List Σ) → (q : states B) → (nq : states A ∨ states B → Bool ) → (nq (case2 q) ≡ true) → ( accept (automaton B) q z ≡ true ) 
         → Naccept NFA (CNFA-exist A B) nq z  ≡ true
     acceptB [] q nq nqt fb = lemma8 where
--- a/automaton-in-agda/src/regular-language.agda	Wed Nov 29 17:40:55 2023 +0900
+++ b/automaton-in-agda/src/regular-language.agda	Fri Apr 05 13:38:20 2024 +0900
@@ -33,25 +33,6 @@
 Concat : {Σ : Set} → ( A B : language {Σ} ) → language {Σ}
 Concat {Σ} A B = split A B
 
--- {-# TERMINATING #-}
--- Star1 : {Σ : Set} → ( A : language {Σ} ) → language {Σ}
--- Star1 {Σ} A [] = true
--- Star0 {Σ} A (h ∷ t) = split A ( Star1 {Σ} A ) (h ∷ t)
-
--- Terminating version of Star1
---
-
--- regular-langue (P *) ( a ∷ b ∷ c ∷ [] ) =
---   (P []) \/
---   (P (a ∷ []) /\ repeat P (b ∷ c ∷ []) ) \/
---   (P (a ∷ b ∷ []) /\ repeat P (c ∷ []) ) \/
---   (P (a ∷ b ∷ c ∷ [])
---
--- repeat : {Σ : Set} → (x : language {Σ} ) → language {Σ}
--- repeat x [] = true
--- repeat x (h  ∷ t) = (x [] /\ ? (h  ∷ t)) \/
---   repeat (λ t1 → x ( h ∷ t1 ))  t
-
 repeat : {Σ : Set} → (P : List Σ → Bool) → (pre y : List Σ ) → Bool
 repeat P [] [] = true
 repeat P (h ∷ t) [] = P (h ∷ t)
@@ -78,6 +59,11 @@
 
 open import automaton-ex
 
+-- test-AB→star : {Σ : Set} → {A B : List In2 → Bool} → Star1 A ( i1 ∷ i1 ∷ i1 ∷ [] ) ≡ ?
+-- test-AB→star  = ?
+
+test-aaa = Star (accept am1 sr) ( i1 ∷ i1 ∷ i1 ∷ [] ) 
+
 test-AB→split : {Σ : Set} → {A B : List In2 → Bool} → split A B ( i0 ∷ i1 ∷ i0 ∷ [] ) ≡ (
        ( A [] /\ B ( i0 ∷ i1 ∷ i0 ∷ [] ) ) \/
        ( A ( i0 ∷ [] ) /\ B ( i1 ∷ i0 ∷ [] ) ) \/
@@ -243,26 +229,26 @@
 
 open import Data.List.Properties
 
-Star→StarProp : {Σ : Set} → ( A : language {Σ} ) → (x : List Σ) → Star A x ≡ true → StarProp A x
-Star→StarProp {Σ} A x ax = ss00 [] x ax  where
-    ss00 :  (pre x : List Σ) → repeat A pre x ≡ true → StarProp A (pre ++ x )
-    ss00 [] [] eq = record { spn = [] ; spn-concat = refl ; propn = eq }
-    ss00 (h ∷ t) [] eq = record { spn = (h ∷ t) ∷ []  ; spn-concat = refl ; propn = bool-and-tt eq refl }
-    ss00 pre (h ∷ []) eq = record { spn = (pre ++ (h ∷ [])) ∷ []  ; spn-concat = ++-assoc pre _ _ 
-       ; propn = bool-and-tt (trans (sym (ss01 pre (h ∷ []) refl )) eq) refl } where
-        ss01 : (pre x : List Σ) → x ≡ h ∷ [] → repeat A pre x ≡ A (pre ++ (h ∷ [])) 
-        ss01 [] (h ∷ []) refl = refl
-        ss01 (x ∷ pre) (h ∷ []) refl = refl
-    ss00 pre (h ∷ y@(i ∷ t)) eq = ? where
-        ss01 : (pre x : List Σ) → x ≡ y → ( ((A (pre ++ (h ∷ []))) /\ repeat A [] y ) \/ repeat A (pre ++ (h ∷ [])) y ) ≡ repeat A pre (h ∷ y )
-        ss01 = ?
-        ss02 :  StarProp A (pre ++ h ∷ y )
-        ss02 with (A (pre ++ (h ∷ []))) /\ repeat A [] y in eq1
-        ... | true = ?
-        ... | false = ? where
-           ss03 : repeat A (pre ++ (h ∷ [])) y ≡ true
-           ss03 = ?
-
+-- Star→StarProp : {Σ : Set} → ( A : language {Σ} ) → (x : List Σ) → Star A x ≡ true → StarProp A x
+-- Star→StarProp {Σ} A x ax = ss00 [] x ax  where
+--     ss00 :  (pre x : List Σ) → repeat A pre x ≡ true → StarProp A (pre ++ x )
+--     ss00 [] [] eq = record { spn = [] ; spn-concat = refl ; propn = eq }
+--     ss00 (h ∷ t) [] eq = record { spn = (h ∷ t) ∷ []  ; spn-concat = refl ; propn = bool-and-tt eq refl }
+--     ss00 pre (h ∷ []) eq = record { spn = (pre ++ (h ∷ [])) ∷ []  ; spn-concat = ++-assoc pre _ _ 
+--        ; propn = bool-and-tt (trans (sym (ss01 pre (h ∷ []) refl )) eq) refl } where
+--         ss01 : (pre x : List Σ) → x ≡ h ∷ [] → repeat A pre x ≡ A (pre ++ (h ∷ [])) 
+--         ss01 [] (h ∷ []) refl = refl
+--         ss01 (x ∷ pre) (h ∷ []) refl = refl
+--     ss00 pre (h ∷ y@(i ∷ t)) eq = ? where
+--         ss01 : (pre x : List Σ) → x ≡ y → ( ((A (pre ++ (h ∷ []))) /\ repeat A [] y ) \/ repeat A (pre ++ (h ∷ [])) y ) ≡ repeat A pre (h ∷ y )
+--         ss01 = ?
+--         ss02 :  StarProp A (pre ++ h ∷ y )
+--         ss02 with (A (pre ++ (h ∷ []))) /\ repeat A [] y in eq1
+--         ... | true = ?
+--         ... | false = ? where
+--            ss03 : repeat A (pre ++ (h ∷ [])) y ≡ true
+--            ss03 = ?
+-- 
 --
 -- StarProp→Star : {Σ : Set} → ( A : language {Σ} ) → (x : List Σ) → StarProp A x → Star A x ≡ true
 -- StarProp→Star {Σ} A x sp = subst (λ k →  Star A k ≡ true ) (spsx (spn sp) refl) ( sps1 (spn sp) refl ) where