>(eq_pair_fst_snd … (trans sig M ?)) whd in ⊢ (??%?→?); #H
>(inject_trans_def sig n i lein M … (eq_pair_fst_snd … ))
whd in ⊢ (??%?); @eq_f2 [destruct (H) // ]
-@(eq_vec … (niltape ?)) #i0 #lei0n
->nth_change_vec_neq >nth_change_vec_neq
- … (tr
-// qed.
-
+@(eq_vec … (niltape ?)) #i0 #lei0n
+cases (decidable_eq_nat … i i0) #Hii0
+[ >Hii0 >nth_change_vec // >pmap_change >nth_change_vec // destruct (H) //
+| >nth_change_vec_neq // >pmap_change >nth_change_vec_neq
+ >tape_move_null_action //
+]
+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
#A #a #b #H destruct //
qed.
-lemma loop_inject: ∀sig,n,M,i,k,ins,int,outs,outt,vt.
+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(11) 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 normalize in ⊢ (%→?); #H destruct
- |#k #Hind #ins #int #outs #outt #vt whd in ⊢ (??%?→??%?);
+ [#ins #int #outs #outt #vt #Hin normalize in ⊢ (%→?); #H destruct
+ |#k #Hind #ins #int #outs #outt #vt #Hin whd in ⊢ (??%?→??%?);
>halt_inject whd in match (cstate ????);
cases (true_or_false (halt sig M ins)) #Hhalt >Hhalt
whd in ⊢ (??%?→??%?);
|destruct (H) //
]
]
- |>(config_expand … (step ???)) #H <(Hind … H)
- >loopM_unfold @eq_f >(mconfig_expand … (step ????))
- @eq_f2 [ normalize in ⊢ (???%);
- |%[>nth_change_vec // @le_S_S //
- |#j #i >nth_change_vec_neq //
+ |>(config_expand … (step ???)) #H <(Hind … H) //
+ >loopM_unfold @eq_f >inject_step //
]
]
+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)).
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 ?)))
#k * * #outs #outt * #Hloop #HRout @(ex_intro ?? k)
-@(ex_intro ?? (mk_mconfig ?? n outs (change_vec ? (S n) vt outt i))) %
- [elim k in Hloop;
- [normalize in ⊢ (%\to ?); #H destruct
- |#k0 #Hind whd in ⊢ (??%?→??%?);
- >halt_inject whd in match (cstate ????);
- whd in match (cstate sig (states sig M)
- (initc sig M (nth i (tape sig) vt (niltape sig))));
- cases (true_or_false (halt sig M (start sig M))) #Hhalt >Hhalt
- whd in ⊢ (??%?→??%?);
- [#H @eq_f whd in ⊢ (??%?); lapply (de_option ??? H) -H
- whd in ⊢ (??%?→?); #H @eq_f2
- [whd in ⊢ (??%?); destruct (H) //
- |@(eq_vec … (niltape ?)) #j #lejn
- cases (true_or_false (eqb i j)) #eqij
- [>(eqb_true_to_eq … eqij) >nth_change_vec //
- <(eqb_true_to_eq … eqij) destruct (H) //
- |>nth_change_vec_neq // @(eqb_false_to_not_eq … eqij)
- ]
- ]
- |#H <Hind //
+@(ex_intro ?? (mk_mconfig ?? n outs (change_vec ? (S n) vt outt i))) %
+ [whd in ⊢ (??(?????%)?); <(change_vec_same ?? vt i (niltape ?)) in ⊢ (??%?);
+ @loop_inject /2 by refl, trans_eq, le_S_S/
|%[>nth_change_vec // @le_S_S //
|#j #i >nth_change_vec_neq //
]
]
-
-
-
-
-
-
+qed.
+theorem acc_sem_inject: ∀sig.∀M:TM sig.∀Rtrue,Rfalse,acc.∀n,i.
+ i≤n → M ⊨ [ acc : Rtrue, Rfalse ] →
+ inject_TM sig M n i ⊨ [ acc : inject_R sig Rtrue n i, inject_R sig Rfalse n i ].
+#sig #M #Rtrue #Rfalse #acc #n #i #lein #HR #vt cases (HR (nth i ? vt (niltape ?)))
+#k * * #outs #outt * * #Hloop #HRtrue #HRfalse @(ex_intro ?? k)
+@(ex_intro ?? (mk_mconfig ?? n outs (change_vec ? (S n) vt outt i))) % [ %
+ [whd in ⊢ (??(?????%)?); <(change_vec_same ?? vt i (niltape ?)) in ⊢ (??%?);
+ @loop_inject /2 by refl, trans_eq, le_S_S/
+ |#Hqtrue %
+ [>nth_change_vec /2 by le_S_S/
+ |#j #Hneq >nth_change_vec_neq //
+ ] ]
+ |#Hqfalse %
+ [>nth_change_vec /2 by le_S_S/ @HRfalse @Hqfalse
+ |#j #Hneq >nth_change_vec_neq //
+ ] ]
+qed.
\ No newline at end of file