--- a/agda/omega-automaton.agda	Thu Aug 30 17:31:57 2018 +0900
+++ b/agda/omega-automaton.agda	Mon Sep 10 23:45:17 2018 +0900
@@ -4,7 +4,7 @@
 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 Data.Empty
@@ -13,18 +13,11 @@
 
 open Automaton 
 
-record Seq ( Σ : Set  )
-       : Set  where
-    field
-        value :  ℕ → Σ
+ω-run : { Q  Σ : Set } → (Ω : Automaton Q Σ ) →  ℕ → ( ℕ → Σ )  → Q
+ω-run Ω zero s = astart Ω
+ω-run Ω (suc n) s = δ Ω (ω-run Ω n s) ( s n )
 
-open Seq
-
-ω-run : { Q  Σ : Set } → (Ω : Automaton Q Σ ) →  ℕ → Seq Σ  → Q
-ω-run Ω zero s = astart Ω
-ω-run Ω (suc n) s = δ Ω (ω-run Ω n s) ( value s n )
-
-record Buchi { Q  Σ : Set } (Ω : Automaton Q Σ ) ( S : Seq  Σ ) : Set where
+record Buchi { Q  Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) : Set where
     field
         from : ℕ
         stay : (n : ℕ ) → n > from → aend Ω ( ω-run Ω n S ) ≡ true
@@ -32,12 +25,11 @@
 open Buchi
        
     
-record Muller { Q  Σ : Set } (Ω : Automaton Q Σ ) ( S : Seq  Σ ) : Set where
+record Muller { Q  Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) : Set where
     field
-        first : ℕ 
-        first-hit : aend Ω ( ω-run Ω first S ) ≡ true
-        next : (n : ℕ ) →  ℕ 
-        next-hit : {n : ℕ } → aend Ω ( ω-run Ω n S ) ≡ true → aend Ω ( ω-run Ω (n + next n) S ) ≡ true
+        next     : (n : ℕ ) → ℕ 
+        large    : (n : ℕ ) →  next n > n
+        infinite : (n : ℕ ) →  aend Ω ( ω-run Ω (next n) S ) ≡ true 
 
 --                       ¬ p
 --                   ------------>
@@ -76,14 +68,14 @@
 flip-seq zero = false
 flip-seq (suc n) = negate ( flip-seq n )
 
-lemma1 : Buchi ωa1 ( record { value = true-seq } )
+lemma1 : Buchi ωa1 true-seq 
 lemma1 = record {
         from = zero
       ; stay = lem1
    } where
-      lem1 : ( n :  ℕ ) → n > zero → aend ωa1 (ω-run ωa1 n (record { value = 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 (record { value = true-seq })
+      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
 
@@ -94,22 +86,59 @@
      ;  aend = λ x → negate ( mark1 x )
   }  
 
-lemma2 : Muller ωa2 ( record { value = flip-seq } )
+flip-dec : (n : ℕ ) →  Dec (  flip-seq n   ≡ true )
+flip-dec n with flip-seq n
+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 = let open ≡-Reasoning in
+          flip-seq (suc n )
+       ≡⟨⟩
+          negate ( 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 
+
+lemma2 : Muller ωa2 flip-seq 
 lemma2 = record {
-        first = 1
-     ;  first-hit =  refl
-     ;  next = λ x → 2
-     ;  next-hit = {!!}
+          next = next
+       ;  large = large
+       ;  infinite = infinite
    }  where
-    lemma : {n : ℕ} → aend ωa2 (ω-run ωa2 n (record { value = false-seq })) ≡ true
-      → aend ωa2 (ω-run ωa2 (n + 2) (record { value = false-seq })) ≡ true
-    lemma {n} prev = {!!}
+     next : ℕ → ℕ
+     next 0 = 1
+     next 1 = 3
+     next (suc (suc n))  = suc (suc (next n ))
+     large :  (n : ℕ) → next n > n
+     large 0 =  s≤s ( z≤n )
+     large 1 =  s≤s  ( s≤s ( z≤n ) )
+     large (suc (suc n))  = s≤s ( s≤s (large n))
+     lem2 :  (n : ℕ) →  ω-run ωa2 (suc (suc n)) flip-seq  ≡ ω-run ωa2 n flip-seq
+     lem2 zero = refl
+     lem2 (suc n) = {!!}
+     infinite : (n : ℕ) → aend ωa2 (ω-run ωa2 (next n) flip-seq) ≡ true
+     infinite 0 = refl
+     infinite 1 = refl
+     infinite (suc (suc n)) = let open ≡-Reasoning in
+          aend ωa2 (ω-run ωa2 (next (suc (suc n))) flip-seq)
+       ≡⟨⟩
+          aend ωa2 (ω-run ωa2 (suc (suc (next n))) flip-seq)
+       ≡⟨ cong ( λ x -> aend  ωa2 x ) (lem2 (next n) ) ⟩
+          aend ωa2 (ω-run ωa2 (next n) flip-seq)
+       ≡⟨ infinite n ⟩
+          true
+       ∎ 
+
    
 
-lemma3 : Buchi ωa1 ( record { value = false-seq } ) →  ⊥
+lemma3 : Buchi ωa1 false-seq  →  ⊥
 lemma3 = {!!}
 
-lemma4 : Muller ωa1 ( record { value = flip-seq } ) →  ⊥
+lemma4 : Muller ωa1 flip-seq  →  ⊥
 lemma4 = {!!}