Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/halt.agda @ 405:af8f630b7e60

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 Sun, 24 Sep 2023 18:02:04 +0900
parents 9120a5872a5b
children c7ad8d2dc157
comparison
equal deleted inserted replaced
404:dfaf230f7b9a 405:af8f630b7e60
1 {-# OPTIONS --cubical-compatible #-}
2
1 module halt where 3 module halt where
2 4
3 open import Level renaming ( zero to Zero ; suc to Suc ) 5 open import Level renaming ( zero to Zero ; suc to Suc )
4 open import Data.Nat 6 open import Data.Nat
5 open import Data.Maybe 7 open import Data.Maybe
90 h-nothing h y refl | false = refl 92 h-nothing h y refl | false = refl
91 h-just : (h : List Bool → Bool) → (y : List Bool) → h y ≡ true → h1 h y ≡ just true 93 h-just : (h : List Bool → Bool) → (y : List Bool) → h y ≡ true → h1 h y ≡ just true
92 h-just h y eq with h y 94 h-just h y eq with h y
93 h-just h y refl | true = refl 95 h-just h y refl | true = refl
94 TN1 : (h : List Bool → Bool) → (y : List Bool ) → Halt.halt halt (UTM.utm utm) (tenc h y) ≡ h y 96 TN1 : (h : List Bool → Bool) → (y : List Bool ) → Halt.halt halt (UTM.utm utm) (tenc h y) ≡ h y
95 TN1 h y with h y | inspect h y 97 TN1 h y with h y in eq1
96 ... | true | record { eq = eq1 } = begin 98 ... | true = begin
97 Halt.halt halt (UTM.utm utm) (tenc h y) ≡⟨ proj2 (is-halt halt (UTM.utm utm) (tenc h y) ) (case1 (sym tm-tenc)) ⟩ 99 Halt.halt halt (UTM.utm utm) (tenc h y) ≡⟨ proj2 (is-halt halt (UTM.utm utm) (tenc h y) ) (case1 (sym tm-tenc)) ⟩
98 true ∎ where 100 true ∎ where
99 tm-tenc : tm (UTM.utm utm) (tenc h y) ≡ just true 101 tm-tenc : tm (UTM.utm utm) (tenc h y) ≡ just true
100 tm-tenc = begin 102 tm-tenc = begin
101 tm (UTM.utm utm) (tenc h y) ≡⟨ is-tm utm _ y ⟩ 103 tm (UTM.utm utm) (tenc h y) ≡⟨ is-tm utm _ y ⟩
102 h1 h y ≡⟨ h-just h y eq1 ⟩ 104 h1 h y ≡⟨ h-just h y eq1 ⟩
103 just true ∎ 105 just true ∎
104 ... | false | record { eq = eq1 } = begin 106 ... | false = begin
105 Halt.halt halt (UTM.utm utm) (tenc h y) ≡⟨ proj2 (is-not-halt halt (UTM.utm utm) (tenc h y) ) (sym tm-tenc) ⟩ 107 Halt.halt halt (UTM.utm utm) (tenc h y) ≡⟨ proj2 (is-not-halt halt (UTM.utm utm) (tenc h y) ) (sym tm-tenc) ⟩
106 false ∎ where 108 false ∎ where
107 tm-tenc : tm (UTM.utm utm) (tenc h y) ≡ nothing 109 tm-tenc : tm (UTM.utm utm) (tenc h y) ≡ nothing
108 tm-tenc = begin 110 tm-tenc = begin
109 tm (UTM.utm utm) (tenc h y) ≡⟨ is-tm utm _ y ⟩ 111 tm (UTM.utm utm) (tenc h y) ≡⟨ is-tm utm _ y ⟩