2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department of the University of Bologna, Italy.
8 \ / This file is distributed under the terms of the
9 \ / GNU General Public License Version 2
10 V_____________________________________________________________*)
12 include "turing/if_machine.ma".
16 stato finale diverso a seconda che il carattere
17 corrente soddisfi un test booleano oppure no
19 q1 = true or no current char
23 definition tc_states ≝ initN 3.
25 definition tc_true ≝ 1.
27 definition test_char ≝
28 λalpha:FinSet.λtest:alpha→bool.
36 | false ⇒ 〈2,None ?〉 ]])
41 ∀c. current alpha t1 = Some ? c →
42 test c = true ∧ t2 = t1.
44 definition Rtc_false ≝
46 ∀c. current alpha t1 = Some ? c →
47 test c = false ∧ t2 = t1.
50 ∀alpha,test,ls,a0,rs. test a0 = true →
51 step alpha (test_char alpha test)
52 (mk_config ?? 0 (midtape … ls a0 rs)) =
53 mk_config alpha (states ? (test_char alpha test)) 1
55 #alpha #test #ls #a0 #ts #Htest normalize >Htest %
59 ∀alpha,test,ls,a0,rs. test a0 = false →
60 step alpha (test_char alpha test)
61 (mk_config ?? 0 (midtape … ls a0 rs)) =
62 mk_config alpha (states ? (test_char alpha test)) 2
64 #alpha #test #ls #a0 #ts #Htest normalize >Htest %
69 accRealize alpha (test_char alpha test)
70 1 (Rtc_true alpha test) (Rtc_false alpha test).
73 @(ex_intro ?? (mk_config ?? 1 (niltape ?))) %
74 [ % // #_ #c normalize #Hfalse destruct | #_ #c normalize #Hfalse destruct (Hfalse) ]
75 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? 1 (leftof ? a al)))
76 % [ % // #_ #c normalize #Hfalse destruct | #_ #c normalize #Hfalse destruct (Hfalse) ]
77 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? 1 (rightof ? a al)))
78 % [ % // #_ #c normalize #Hfalse destruct | #_ #c normalize #Hfalse destruct (Hfalse) ]
79 | #ls #c #rs @(ex_intro ?? 2)
80 cases (true_or_false (test c)) #Htest
81 [ @(ex_intro ?? (mk_config ?? 1 ?))
84 [ whd in ⊢ (??%?); >tc_q0_q1 //
85 | #_ #c0 #Hc0 % // normalize in Hc0; destruct // ]
86 | * #Hfalse @False_ind @Hfalse % ]
88 | @(ex_intro ?? (mk_config ?? 2 (midtape ? ls c rs)))
91 [ whd in ⊢ (??%?); >tc_q0_q2 //
92 | #Hfalse destruct (Hfalse) ]
93 | #_ #c0 #Hc0 % // normalize in Hc0; destruct (Hc0) //