--- a/automaton-in-agda/src/logic.agda	Sun Jan 23 11:15:01 2022 +0900
+++ b/automaton-in-agda/src/logic.agda	Tue Jan 25 09:11:01 2022 +0900
@@ -43,6 +43,10 @@
 de-morgan {n} {A} {B} and (case1 ¬A) = ⊥-elim ( ¬A ( _∧_.proj1 and ))
 de-morgan {n} {A} {B} and (case2 ¬B) = ⊥-elim ( ¬B ( _∧_.proj2 and ))
 
+de-morgan∨ : {n  : Level } {A B : Set n} →  A ∨ B  → ¬ ( (¬ A ) ∧ (¬ B ) )
+de-morgan∨ {n} {A} {B} (case1 a) and = ⊥-elim (  _∧_.proj1 and a )
+de-morgan∨ {n} {A} {B} (case2 b) and = ⊥-elim (  _∧_.proj2 and b )
+
 dont-or :　{n m : Level} {A  : Set n} { B : Set m } →  A ∨ B → ¬ A → B
 dont-or {A} {B} (case1 a) ¬A = ⊥-elim ( ¬A a )
 dont-or {A} {B} (case2 b) ¬A = b

--- a/automaton-in-agda/src/nat.agda	Sun Jan 23 11:15:01 2022 +0900
+++ b/automaton-in-agda/src/nat.agda	Tue Jan 25 09:11:01 2022 +0900
@@ -155,6 +155,13 @@
 x≤y+x : {z y : ℕ } → z ≤ y + z
 x≤y+x {z} {y} = subst (λ k → z ≤ k ) (+-comm _ y ) x≤x+y
 
+x≤x+sy : {x y : ℕ} → x < x + suc y
+x≤x+sy {x} {y} = begin
+        suc x ≤⟨ x≤x+y ⟩
+        suc x + y ≡⟨ cong (λ k → k + y) (+-comm 1 x ) ⟩
+        (x + 1) + y ≡⟨ (+-assoc x 1 _) ⟩
+        x + suc y ∎  where open ≤-Reasoning
+
 <-plus : {x y z : ℕ } → x < y → x + z < y + z 
 <-plus {zero} {suc y} {z} (s≤s z≤n) = s≤s (subst (λ k → z ≤ k ) (+-comm z _ ) x≤x+y  )
 <-plus {suc x} {suc y} {z} (s≤s lt) = s≤s (<-plus {x} {y} {z} lt)

--- a/automaton-in-agda/src/omega-automaton.agda	Sun Jan 23 11:15:01 2022 +0900
+++ b/automaton-in-agda/src/omega-automaton.agda	Tue Jan 25 09:11:01 2022 +0900
@@ -16,7 +16,7 @@
 
 ω-run : { Q  Σ : Set } → (Ω : Automaton Q Σ ) → Q →  ( ℕ → Σ )  → ( ℕ → Q )
 ω-run Ω x s zero = x
-ω-run Ω x  s (suc n) = δ Ω (ω-run Ω x s n) ( s n )
+ω-run Ω x s (suc n) = δ Ω (ω-run Ω x s n) ( s n )
 
 --
 -- accept as Buchi automaton
@@ -56,41 +56,59 @@
 open import nat
 open import Data.Nat.Properties
 
-LEMB : { Q  Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) → Q → Buchi Ω S ∨ (¬ ( Buchi Ω S ))
-LEMB = {!!}
+-- 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 = {!!}
 
-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
+ω-run-eq Ω  Ω' q s zero refl =  refl
+ω-run-eq Ω  Ω' q s (suc n) eq = begin
+     ω-run Ω q s (suc n) ≡⟨⟩
+     δ Ω (ω-run Ω q s n) (s n) ≡⟨ cong₂ (λ j k → j k (s n) ) eq (ω-run-eq Ω  Ω' q s n eq) ⟩
+     δ Ω' (ω-run Ω' q s n) (s n) ≡⟨⟩
+     ω-run Ω' q s (suc n) ∎  where open ≡-Reasoning
 
 B→M : { Q  Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) → Q → Buchi Ω S → ¬ ( Muller record { δ = δ Ω ; aend = λ q → not (aend Ω q)} S )
-B→M {Q} {Σ} Ω S q b m = ¬t=f (aend Ω ( ω-run Ω bm00 S (from b + suc ( next m (from b ) ))))  {!!} where
-   bm00 : Q
-   bm00 = ω-run Ω q S (from b + suc (Muller.next m (from b)))
-   bm02 :  aend Ω (ω-run Ω bm00 S (from b + suc (next m (from b) ))) ≡ true
-   bm02 = stay b bm00 (from b + suc (next m (from b) )) {!!}
-   Ω' : Automaton Q Σ
-   Ω' = record { δ = δ Ω ; aend = λ q → not (aend Ω q) }
-   bm03 : aend  Ω' (ω-run  Ω' bm00 S (from b + suc (next m (from b) ))) ≡ true
-   bm03 = infinite m bm00  (from b)
-   bm05 : (q : Q) → (n : ℕ) → ω-run  Ω' q S n ≡ ω-run  Ω q S n
-   bm05 q zero = refl
-   bm05 q (suc n) = begin
-    ω-run  Ω' q S (suc n) ≡⟨⟩
-    δ Ω (ω-run Ω' q S n) (S n) ≡⟨ cong (λ k → δ Ω  k (S n) ) (bm05 q n) ⟩
-    δ Ω (ω-run Ω q S n) (S n) ≡⟨⟩
-    ω-run Ω q S (suc n) ∎ where open ≡-Reasoning
-   bm04 : (q : Q) → (n : ℕ) → aend  Ω' (ω-run  Ω' q S n) ≡ not aend  Ω (ω-run  Ω q S n) 
-   bm04 q zero = refl
-   bm04 q (suc n) = begin
-     aend Ω' (ω-run Ω' q S (suc n)) ≡⟨⟩
-     not aend Ω (δ Ω (ω-run Ω' q S n) (S n)) ≡⟨ cong (λ k → not aend Ω ( δ Ω k (S n))) (bm05 q n) ⟩
-     not aend Ω (δ Ω (ω-run Ω q S n) (S n)) ≡⟨⟩
-     not aend Ω (ω-run Ω q S (suc n)) ∎ where open ≡-Reasoning
-   bm01 :  (not aend Ω (ω-run Ω bm00 S (Muller.next m (from b) + from b))) ≡ aend Ω (ω-run Ω bm00 S (Muller.next m (from b) + from b))
-   bm01 = {!!}
+B→M {Q} {Σ} Ω S q b m = ¬-bool bm04 bm02 where
+   q1 : Q
+   q1 = ω-run Ω q S (from b + suc (next m (from b)))
+   bm02 : aend Ω q1 ≡ true
+   bm02 = stay b q (from b + suc (next m (from b) )) x≤x+sy 
+   Ω' : Automaton  Q Σ
+   Ω' = record {  δ = δ Ω ; aend = λ q → not (aend Ω q) }
+   bm03 : aend Ω' (ω-run Ω' q S (from b + (suc (next m (from b))))) ≡ true
+   bm03 = infinite m q (from b)
+   bm04 : aend Ω q1 ≡ false
+   bm04 = begin
+     aend Ω (ω-run Ω q S (from b + suc (next m (from b)))) ≡⟨ sym not-not-bool ⟩
+     not (not (aend Ω (ω-run Ω q S (from b + suc (next m (from b)))))) ≡⟨ cong (λ k → not (not (aend  Ω k))) (ω-run-eq Ω Ω' q S (from b + suc (next m (from b))) refl) ⟩
+     not (not (aend Ω (ω-run Ω' q S (from b + suc (next m (from b)))))) ≡⟨⟩
+     not (aend Ω' (ω-run Ω' q S (from b + (suc (next m (from b)))))) ≡⟨ cong (λ k → not k ) bm03  ⟩
+     false ∎  where open ≡-Reasoning
+
 
-M→B : { Q  Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) → Muller Ω S → ¬ ( Buchi record { δ = δ Ω ; aend = λ q → not (aend Ω q)} S )
-M→B = {!!}
+M→B : { Q  Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) → Q → Muller Ω S → ¬ ( Buchi 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)))
+   bm02 : aend Ω q1 ≡ true
+   bm02 = infinite m q (from b)
+   Ω' : Automaton  Q Σ
+   Ω' = record {  δ = δ Ω ; aend = λ q → not (aend Ω q) }
+   bm03 : aend Ω' (ω-run Ω' q S (from b + (suc (next m (from b))))) ≡ true
+   bm03 = stay b q (from b + suc (next m (from b) )) x≤x+sy 
+   bm04 : aend Ω q1 ≡ false
+   bm04 = begin
+     aend Ω (ω-run Ω q S (from b + suc (next m (from b)))) ≡⟨ sym not-not-bool ⟩
+     not (not (aend Ω (ω-run Ω q S (from b + suc (next m (from b)))))) ≡⟨ cong (λ k → not (not (aend  Ω k))) (ω-run-eq Ω Ω' q S (from b + suc (next m (from b))) refl) ⟩
+     not (not (aend Ω (ω-run Ω' q S (from b + suc (next m (from b)))))) ≡⟨⟩
+     not (aend Ω' (ω-run Ω' q S (from b + (suc (next m (from b)))))) ≡⟨ cong (λ k → not k ) bm03 ⟩
+     false ∎  where open ≡-Reasoning
+
 
 
 data  States3   : Set  where