--- a/agda/omega-automaton.agda	Mon Sep 10 23:45:17 2018 +0900
+++ b/agda/omega-automaton.agda	Mon Sep 17 20:43:59 2018 +0900
@@ -28,8 +28,7 @@
 record Muller { Q  Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) : Set where
     field
         next     : (n : ℕ ) → ℕ 
-        large    : (n : ℕ ) →  next n > n
-        infinite : (n : ℕ ) →  aend Ω ( ω-run Ω (next n) S ) ≡ true 
+        infinite : (n : ℕ ) →  aend Ω ( ω-run Ω (n + (next n)) S ) ≡ true 
 
 --                       ¬ p
 --                   ------------>
@@ -103,37 +102,28 @@
 flip-dec2 n () | false 
 flip-dec2 n () | true 
 
+
+record flipProperty : Set where
+    field
+       flipP : (n : ℕ) →  ω-run ωa2 (suc (suc n)) flip-seq  ≡ ω-run ωa2 n flip-seq
+
 lemma2 : Muller ωa2 flip-seq 
 lemma2 = record {
           next = next
-       ;  large = large
        ;  infinite = infinite
    }  where
      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
-       ∎ 
-
-   
+     next n with ω-run ωa2 n flip-seq | flip-seq n
+     next n | ts | true = 2
+     next n | ts | false = 1
+     next n | ts* | true = 2
+     next n | ts* | false = 1
+     infinite : (n : ℕ) → aend ωa2 (ω-run ωa2 (n + (next n)) flip-seq) ≡ true
+     infinite n with ω-run ωa2 n flip-seq | flip-seq n | 
+     infinite n | ts | true = {!!}
+     infinite n | ts | false = {!!}
+     infinite n | ts* | true = {!!}
+     infinite n | ts* | false = {!!}
 
 lemma3 : Buchi ωa1 false-seq  →  ⊥
 lemma3 = {!!}