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_start : tc_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 3 (refl …)).
26 definition tc_true : tc_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 3 (refl …)).
27 definition tc_false : tc_states ≝ mk_Sig ?? 2 (leb_true_to_le 3 3 (refl …)).
29 definition test_char ≝
30 λalpha:FinSet.λtest:alpha→bool.
34 [ None ⇒ 〈tc_true, None ?〉
37 [ true ⇒ 〈tc_true,None ?〉
38 | false ⇒ 〈tc_false,None ?〉 ]])
39 tc_start (λx.notb (x == tc_start)).
43 ∀c. current alpha t1 = Some ? c →
44 test c = true ∧ t2 = t1.
46 definition Rtc_false ≝
48 ∀c. current alpha t1 = Some ? c →
49 test c = false ∧ t2 = t1.
52 ∀alpha,test,ls,a0,rs. test a0 = true →
53 step alpha (test_char alpha test)
54 (mk_config ?? tc_start (midtape … ls a0 rs)) =
55 mk_config alpha (states ? (test_char alpha test)) tc_true
57 #alpha #test #ls #a0 #ts #Htest whd in ⊢ (??%?);
58 whd in match (trans … 〈?,?〉); >Htest %
62 ∀alpha,test,ls,a0,rs. test a0 = false →
63 step alpha (test_char alpha test)
64 (mk_config ?? tc_start (midtape … ls a0 rs)) =
65 mk_config alpha (states ? (test_char alpha test)) tc_false
67 #alpha #test #ls #a0 #ts #Htest whd in ⊢ (??%?);
68 whd in match (trans … 〈?,?〉); >Htest %
73 accRealize alpha (test_char alpha test)
74 tc_true (Rtc_true alpha test) (Rtc_false alpha test).
77 @(ex_intro ?? (mk_config ?? tc_true (niltape ?))) %
78 [ % // #_ #c normalize #Hfalse destruct | #_ #c normalize #Hfalse destruct (Hfalse) ]
79 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? tc_true (leftof ? a al)))
80 % [ % // #_ #c normalize #Hfalse destruct | #_ #c normalize #Hfalse destruct (Hfalse) ]
81 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? tc_true (rightof ? a al)))
82 % [ % // #_ #c normalize #Hfalse destruct | #_ #c normalize #Hfalse destruct (Hfalse) ]
83 | #ls #c #rs @(ex_intro ?? 2)
84 cases (true_or_false (test c)) #Htest
85 [ @(ex_intro ?? (mk_config ?? tc_true ?))
88 [ whd in ⊢ (??%?); >tc_q0_q1 //
89 | #_ #c0 #Hc0 % // normalize in Hc0; destruct // ]
90 | * #Hfalse @False_ind @Hfalse % ]
92 | @(ex_intro ?? (mk_config ?? tc_false (midtape ? ls c rs)))
95 [ whd in ⊢ (??%?); >tc_q0_q2 //
96 | whd in ⊢ ((??%%)→?); #Hfalse destruct (Hfalse) ]
97 | #_ #c0 #Hc0 % // normalize in Hc0; destruct (Hc0) //