2 include "turing/multi_to_mono/step.ma".
4 definition stop ≝ λsig,n.λM:mTM sig n.λc.
5 notb (halt sig n M (get_state (states sig n M) sig (S n) c (start sig n M))).
7 definition mtm_body ≝ λsig,n.λM:mTM sig n.
8 ifTM ? (test_char … (stop sig n M))
9 (single_finalTM ? (stepM (states sig n M) sig n (trans sig n M)))
12 definition acc_mtm : ∀sig,n,M.states ? (mtm_body sig n M) ≝
13 λsig,n,M. (inr … (inl … (inr … start_nop))).
15 definition mtm_R_true ≝ λsig,n.λM:mTM sig n.λt1,t2.
16 ∀a:multi_sig (TA (HC (states sig n M) (S n)) sig) (S (S n)).
18 t1 = midtape ? ls a rs →
19 let cin ≝ readback_config ? sig n (start … M) ls a rs in
20 halt sig n M (cstate … cin) = false ∧
21 R_stepM sig n M t1 t2.
23 definition mtm_R_false ≝ λsig,n.λM:mTM sig n.λt1,t2.
24 ∀a:multi_sig (TA (HC (states sig n M) (S n)) sig) (S (S n)).
26 t1 = midtape ? ls a rs →
27 let cin ≝ readback_config ? sig n (start … M) ls a rs in
28 halt sig n M (cstate … cin) = true ∧ t1 = t2.
30 lemma sem_mtm_body: ∀sig,n,M.
31 mtm_body sig n M ⊨ [acc_mtm sig n M: mtm_R_true sig n M,
34 @(acc_sem_if_app ??????????? (sem_test_char … (stop sig n M))
37 [#tin #tout #t1 * * #c * #Hc #Hstop #Ht1 >Ht1 #Hstep
38 #a #ls #rs #Htin % [2:@Hstep] >Htin in Hc; whd in ⊢ (??%?→?);
39 #H destruct (H) >state_readback @injective_notb @Hstop
40 |#tin #tout #t1 * #Hc #Ht1 #Htout #a #ls #rs #Htin % //
41 >Htin in Hc; #Hc lapply (Hc … (refl ??)) #H @injective_notb @H
45 definition multi_to_monoTM ≝ λsig,n,M.
46 whileTM ? (mtm_body sig n M) (acc_mtm sig n M).
48 definition multi_to_mono_R ≝ λsig,n.λM:mTM sig n.λt1,t2.
49 ∀a:multi_sig (TA (HC (states sig n M) (S n)) sig) (S (S n)).
51 t1 = midtape ? ls a rs →
52 (∀i.regular_trace (TA (HC (states … M) (S n)) sig) (S(S n)) a ls rs i) →
53 is_head ?? (nth (S n) ? (vec … a) (blank ?)) = true →
56 let cin ≝ readback_config ? sig n (start … M) ls a rs in
57 ∃a1:multi_sig (TA (HC (states sig n M) (S n)) sig) (S (S n)).
59 t2 = midtape ? ls1 a1 rs1 ∧
60 let cout ≝ readback_config ? sig n (start … M) ls1 a1 rs1 in
61 loopM sig n M i cin = Some ? cout.
63 theorem sem_universal: ∀sig,n,M.
64 multi_to_monoTM sig n M ⊫ multi_to_mono_R sig n M.
65 #sig #n #M #intape #i #outc #Hloop
66 lapply (sem_while ?????? (sem_mtm_body sig n M) intape i outc Hloop) [%] -Hloop
67 * #tin * #Hstar #Hfalse @(star_ind_l ??????? Hstar) -Hstar
68 [#a #ls #rs #Htin #_ #_ #_ #_ lapply (Hfalse … Htin) * #Hhalt #Houtc
69 %{a} %{ls} %{rs} %{1} % [<Houtc @Htin |@loop_S_true @Hhalt]
70 |#ta #tb #Hab #Hstar #Hind #a #ls #rs #Ha #H1 #H2 #H3 #H4 lapply (Hab … Ha)
71 * #Hfalseb -Hab #Hab lapply (Hab … Ha H1 H2 H3 H4) -H1 -H2 -H3 -H4
72 * #ls1 * #a1 * #rs1 * * #Htb #Hregb #Hrb_b
73 lapply (Hind … Htb Hregb ???) [@daemon | @daemon |@daemon]
74 * #a2 * #ls2 * #rs2 * #i * #Hc #Hloop
75 %{a2} %{ls2} %{rs2} %{(S i)} % [@Hc] whd
76 whd in match (loopM ?????); >Hfalseb whd in ⊢ (??%?); <Hrb_b @Hloop