--- a/agda/omega-automaton.agda	Wed Dec 18 17:34:15 2019 +0900
+++ b/agda/omega-automaton.agda	Sat Mar 14 17:34:54 2020 +0900
@@ -4,23 +4,24 @@
 open import Data.Nat
 open import Data.List
 open import Data.Maybe
-open import Data.Bool using ( Bool ; true ; false ; _∧_ ) renaming ( not to negate )
+-- open import Data.Bool using ( Bool ; true ; false ; _∧_ ) renaming ( not to negate )
 open import  Relation.Binary.PropositionalEquality hiding ( [_] )
-open import Relation.Nullary using (¬_; Dec; yes; no)
+open import Relation.Nullary using (not_; Dec; yes; no)
 open import Data.Empty
 
+open import logic
 open import automaton
 
 open Automaton 
 
-ω-run : { Q  Σ : Set } → (Ω : Automaton Q Σ ) →  ℕ → ( ℕ → Σ )  → Q
-ω-run Ω zero s = astart Ω
-ω-run Ω (suc n) s = δ Ω (ω-run Ω n s) ( s n )
+ω-run : { Q  Σ : Set } → (Ω : Automaton Q Σ ) → (astart : Q )  →  ℕ → ( ℕ → Σ )  → Q
+ω-run Ω x zero s = x
+ω-run Ω x (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
+        stay : (n : ℕ ) → n > from → aend Ω ( ω-run Ω ? n S ) ≡ true
 
 open Buchi
        
@@ -28,9 +29,9 @@
 record Muller { Q  Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) : Set where
     field
         next     : (n : ℕ ) → ℕ 
-        infinite : (n : ℕ ) →  aend Ω ( ω-run Ω (n + (next n)) S ) ≡ true 
+        infinite : (n : ℕ ) →  aend Ω ( ω-run Ω ? (n + (next n)) S ) ≡ true 
 
---                       ¬ p
+--                       not p
 --                   ------------>
 --        [] <> p *                 [] <> p 
 --                   <-----------
@@ -53,7 +54,6 @@
 ωa1 : Automaton States3 Bool
 ωa1 = record {
         δ = transition3
-     ;  astart = ts*
      ;  aend = mark1
   }  
 
@@ -65,24 +65,23 @@
 
 flip-seq :  ℕ → Bool
 flip-seq zero = false
-flip-seq (suc n) = negate ( flip-seq n )
+flip-seq (suc n) = not ( flip-seq n )
 
 lemma1 : Buchi ωa1 true-seq 
 lemma1 = record {
         from = zero
       ; stay = lem1
    } where
-      lem1 : ( n :  ℕ ) → n > zero → aend ωa1 (ω-run ωa1 n true-seq ) ≡ true
+      lem1 : ( n :  ℕ ) → n > zero → aend ωa1 (ω-run ωa1 ? n true-seq ) ≡ true
       lem1 zero ()
-      lem1 (suc n) (s≤s z≤n) with ω-run ωa1 n true-seq 
-      lem1 (suc n) (s≤s z≤n) | ts* = refl
-      lem1 (suc n) (s≤s z≤n) | ts = refl
+      lem1 (suc n) (s≤s z≤n) with ω-run ωa1 ? n true-seq 
+      lem1 (suc n) (s≤s z≤n) | ts* = ?
+      lem1 (suc n) (s≤s z≤n) | ts = ?
 
 ωa2 : Automaton States3 Bool
 ωa2 = record {
         δ = transition3
-     ;  astart = ts*
-     ;  aend = λ x → negate ( mark1 x )
+     ;  aend = λ x → not ( mark1 x )
   }  
 
 flip-dec : (n : ℕ ) →  Dec (  flip-seq n   ≡ true )
@@ -90,17 +89,15 @@
 flip-dec n | false = no  λ () 
 flip-dec n | true = yes refl
 
-flip-dec1 : (n : ℕ ) → flip-seq (suc n)  ≡ negate ( flip-seq n )
+flip-dec1 : (n : ℕ ) → flip-seq (suc n)  ≡ ( not ( flip-seq n ) )
 flip-dec1 n = let open ≡-Reasoning in
           flip-seq (suc n )
        ≡⟨⟩
-          negate ( flip-seq n )
+          ( not ( flip-seq n ) )
        ∎
 
-flip-dec2 : (n : ℕ ) → ¬ flip-seq (suc n)  ≡  flip-seq n 
-flip-dec2 n neq with  flip-seq n
-flip-dec2 n () | false 
-flip-dec2 n () | true 
+flip-dec2 : (n : ℕ ) → not flip-seq (suc n)  ≡  flip-seq n 
+flip-dec2 n = ?
 
 
 record flipProperty : Set where