Mercurial > hg > Members > kono > Proof > automaton

comparison agda/utm.agda @ 141:b3f05cd08d24

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
clean up
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 27 Dec 2020 13:26:44 +0900
parents 4c3fbfde1bc2
children
comparison
equal deleted inserted replaced
140:4c3fbfde1bc2 141:b3f05cd08d24
168 utmδ tidy0 $ = tidy1 , write $ , left 168 utmδ tidy0 $ = tidy1 , write $ , left
169 utmδ tidy0 x = tidy0 , write x , left 169 utmδ tidy0 x = tidy0 , write x , left
170 utmδ tidy1 X = tidy1 , write ０ , left 170 utmδ tidy1 X = tidy1 , write ０ , left
171 utmδ tidy1 Y = tidy1 , write １ , left 171 utmδ tidy1 Y = tidy1 , write １ , left
172 utmδ tidy1 Z = tidy1 , write B , left 172 utmδ tidy1 Z = tidy1 , write B , left
173 utmδ tidy1 $ = read0 , write $ , right 173 utmδ tidy1 $ = reads , write $ , right
174 utmδ tidy1 x = tidy1 , write x , left 174 utmδ tidy1 x = tidy1 , write x , left
175 utmδ _ x = halt , write x , mnone 175 utmδ _ x = halt , write x , mnone
176 176
177 U-TM : Turing utmStates utmΣ 177 U-TM : Turing utmStates utmΣ
178 U-TM = record { 178 U-TM = record {
244 ... | nq , nL , nR | _ = loop (suc n) nq nL nR 244 ... | nq , nL , nR | _ = loop (suc n) nq nL nR
245 245
246 t1 = utm-test2 20 short-input 246 t1 = utm-test2 20 short-input
247 247
248 t : (n : ℕ) → utmStates × ( List utmΣ ) × ( List utmΣ ) 248 t : (n : ℕ) → utmStates × ( List utmΣ ) × ( List utmΣ )
249 t n = utm-test2 n short-input 249 -- t n = utm-test2 n input+Copyδ
250 t n = utm-test2 n short-input