Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/omega-automaton.agda @ 330:407684f806e4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 16 Nov 2022 17:43:10 +0900
parents ba0ae5de62d1
children ce4e44cee2d3
comparison
equal deleted inserted replaced
329:ba0ae5de62d1 330:407684f806e4
69 ω-run-eq Ω Ω' q s (suc n) eq = begin 69 ω-run-eq Ω Ω' q s (suc n) eq = begin
70 ω-run Ω q s (suc n) ≡⟨⟩ 70 ω-run Ω q s (suc n) ≡⟨⟩
71 δ Ω (ω-run Ω q s n) (s n) ≡⟨ cong₂ (λ j k → j k (s n) ) eq (ω-run-eq Ω Ω' q s n eq) ⟩ 71 δ Ω (ω-run Ω q s n) (s n) ≡⟨ cong₂ (λ j k → j k (s n) ) eq (ω-run-eq Ω Ω' q s n eq) ⟩
72 δ Ω' (ω-run Ω' q s n) (s n) ≡⟨⟩ 72 δ Ω' (ω-run Ω' q s n) (s n) ≡⟨⟩
73 ω-run Ω' q s (suc n) ∎ where open ≡-Reasoning 73 ω-run Ω' q s (suc n) ∎ where open ≡-Reasoning
74
75 --
76 -- <> [] p → ¬ [] <> ¬ p
77 --
78
74 79
75 B→M : { Q Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) → Q → Buchi Ω S → ¬ ( Muller record { δ = δ Ω ; aend = λ q → not (aend Ω q)} S ) 80 B→M : { Q Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) → Q → Buchi Ω S → ¬ ( Muller record { δ = δ Ω ; aend = λ q → not (aend Ω q)} S )
76 B→M {Q} {Σ} Ω S q b m = ¬-bool bm04 bm02 where 81 B→M {Q} {Σ} Ω S q b m = ¬-bool bm04 bm02 where
77 q1 : Q 82 q1 : Q
78 q1 = ω-run Ω q S (from b + suc (next m (from b))) 83 q1 = ω-run Ω q S (from b + suc (next m (from b)))
88 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) ⟩ 93 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) ⟩
89 not (not (aend Ω (ω-run Ω' q S (from b + suc (next m (from b)))))) ≡⟨⟩ 94 not (not (aend Ω (ω-run Ω' q S (from b + suc (next m (from b)))))) ≡⟨⟩
90 not (aend Ω' (ω-run Ω' q S (from b + (suc (next m (from b)))))) ≡⟨ cong (λ k → not k ) bm03 ⟩ 95 not (aend Ω' (ω-run Ω' q S (from b + (suc (next m (from b)))))) ≡⟨ cong (λ k → not k ) bm03 ⟩
91 false ∎ where open ≡-Reasoning 96 false ∎ where open ≡-Reasoning
92 97
98 --
99 -- [] <> p → ¬ <> [] ¬ p
100 --
93 101
94 M→B : { Q Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) → Q → Muller Ω S → ¬ ( Buchi record { δ = δ Ω ; aend = λ q → not (aend Ω q)} S ) 102 M→B : { Q Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) → Q → Muller Ω S → ¬ ( Buchi record { δ = δ Ω ; aend = λ q → not (aend Ω q)} S )
95 M→B {Q} {Σ} Ω S q m b = ¬-bool bm04 bm02 where 103 M→B {Q} {Σ} Ω S q m b = ¬-bool bm04 bm02 where
96 q1 : Q 104 q1 : Q
97 q1 = ω-run Ω q S (from b + suc (next m (from b))) 105 q1 = ω-run Ω q S (from b + suc (next m (from b)))