V_____________________________________________________________*)
include "turing/turing.ma".
+(* include "turing/basic_machines.ma". *)
(******************* inject a mono machine into a multi tape one **********************)
+
definition inject_trans ≝ λsig,states:FinSet.λn,i:nat.
λtrans:states × (option sig) → states × (option sig × move).
λp:states × (Vector (option sig) (S n)).
lemma inject_trans_def :∀sig:FinSet.∀n,i:nat.i < S n →
∀M,v,s,a,sn,an,mn.
trans sig M 〈s,a〉 = 〈sn,an,mn〉 →
- cic:/matita/turing/turing/trans.fix(0,2,9) sig n (inject_TM sig M n i) 〈s,change_vec ? (S n) v a i〉 =
+ cic:/matita/turing/turing/trans#fix:0:2:9 sig n (inject_TM sig M n i) 〈s,change_vec ? (S n) v a i〉 =
〈sn,change_vec ? (S n) (null_action ? n) 〈an,mn〉 i〉.
#sig #n #i #Hlt #M #v #s #a #sn #an #mn #Htrans
whd in ⊢ (??%?); >nth_change_vec // >Htrans //
lemma inject_step : ∀sig,n,M,i,q,t,nq,nt,v. i < S n →
step sig M (mk_config ?? q t) = mk_config ?? nq nt →
- cic:/matita/turing/turing/step.def(12) sig n (inject_TM sig M n i)
+ cic:/matita/turing/turing/step#def:12 sig n (inject_TM sig M n i)
(mk_mconfig ?? n q (change_vec ? (S n) v t i))
= mk_mconfig ?? n nq (change_vec ? (S n) v nt i).
#sig #n #M #i #q #t #nq #nt #v #lein whd in ⊢ (??%?→?);
qed.
lemma halt_inject: ∀sig,n,M,i,x.
- cic:/matita/turing/turing/halt.fix(0,2,9) sig n (inject_TM sig M n i) x
+ cic:/matita/turing/turing/halt#fix:0:2:9 sig n (inject_TM sig M n i) x
= halt sig M x.
// qed.
lemma loop_inject: ∀sig,n,M,i,k,ins,int,outs,outt,vt.i < S n →
loopM sig M k (mk_config ?? ins int) = Some ? (mk_config ?? outs outt) →
- cic:/matita/turing/turing/loopM.def(13) sig n (inject_TM sig M n i) k (mk_mconfig ?? n ins (change_vec ?? vt int i))
+ cic:/matita/turing/turing/loopM#def:13 sig n (inject_TM sig M n i) k (mk_mconfig ?? n ins (change_vec ?? vt int i))
=Some ? (mk_mconfig sig ? n outs (change_vec ?? vt outt i)).
#sig #n #M #i #k elim k -k
[#ins #int #outs #outt #vt #Hin normalize in ⊢ (%→?); #H destruct
]
qed.
-(*
-lemma cstate_inject: ∀sig,n,M,i,x. *)
-
definition inject_R ≝ λsig.λR:relation (tape sig).λn,i:nat.
λv1,v2: (Vector (tape sig) (S n)).
R (nth i ? v1 (niltape ?)) (nth i ? v2 (niltape ?)) ∧
∀j. i ≠ j → nth j ? v1 (niltape ?) = nth j ? v2 (niltape ?).
-(*
-lemma nth_make : ∀A,i,n,j,a,d. i < n → nth i ? (make_veci A a n j) d = a (j+i).
-#A #i elim i
- [#n #j #a #d #ltOn @(lt_O_n_elim … ltOn) <plus_n_O //
- |#m #Hind #n #j #a #d #Hlt lapply Hlt @(lt_O_n_elim … (ltn_to_ltO … Hlt))
- #p <plus_n_Sm #ltmp @Hind @le_S_S_to_le //
- ]
-qed. *)
-
-(*
-lemma mk_config_eq_s: ∀S,sig,s1,s2,t1,t2.
- mk_config S sig s1 t1 = mk_config S sig s2 t2 → s1=s2.
-#S #sig #s1 #s2 #t1 #t2 #H destruct //
-qed.
-
-lemma mk_config_eq_t: ∀S,sig,s1,s2,t1,t2.
- mk_config S sig s1 t1 = mk_config S sig s2 t2 → s1=s2.
-#S #sig #s1 #s2 #t1 #t2 #H destruct //
-qed.
-*)
-
theorem sem_inject: ∀sig.∀M:TM sig.∀R.∀n,i.
i≤n → M ⊨ R → inject_TM sig M n i ⊨ inject_R sig R n i.
#sig #M #R #n #i #lein #HR #vt cases (HR (nth i ? vt (niltape ?)))