Require Import List Lia.
Require Import Undecidability.TM.SBTM.
Require Undecidability.StringRewriting.SR.
Require Import Undecidability.StringRewriting.Util.Definitions.
Require Import Undecidability.Synthetic.Definitions.
Require Import Undecidability.Synthetic.ReducibilityFacts.
Require Import Undecidability.StringRewriting.Reductions.HaltSBTMu_to_SRH.
Require Import Undecidability.Shared.ListAutomation.
Import ListNotations.
Set Default Proof Using "Type".
Section FixM.
Variable M : SBTM.
Notation END := 0.
Notation X := 1.
Notation "⦇" := 2.
Notation "⦈" := 3.
Notation tt := 4.
Notation ff := 5.
Notation "!! b" := (if b then tt else ff) (at level 1).
Notation "! p" := (@enc_state M p) (at level 1).
Lemma help_exists1 (P : state M -> tape -> option bool -> move -> Prop) :
(exists c q w m ls rs, P q (ls, c, rs) w m) -> (exists q t w m, P q t w m).
Proof.
intros (c & q & w & m & ls & rs & H). now exists q, (ls, c, rs), w, m.
Qed.
Lemma help_exists2 P Q :
(P /\ exists ls rs, Q ls rs) -> exists ls rs : list bool, P /\ Q ls rs.
Proof using M.
firstorder.
Qed.
Lemma rev_sim_swap t q z :
SR.rew (map SR.swap (R M)) (enc_conf M t q) z -> exists q' t' w m, trans M (q', curr t') = Some (q, w, m) /\ t = mv m (wr w t') /\ z = enc_conf M t' q'.
Proof.
intros H. inversion H as [x y v u Hin HL HR]; subst z.
eapply in_map_iff in Hin as ([? ?] & [= -> ->] & Hin).
destruct t as [[ls o] rs].
eapply in_flat_map in Hin as (q_ & _ & Hq2).
unfold rules in Hq2.
rewrite ! in_app_iff in Hq2.
destruct Hq2 as [ Hq2 | [Hq2 | Hq2]].
all: destruct (trans M (q_, _)) as [ [[q' w] m] | ] eqn:Etrans; try destruct m eqn:Em;
try destruct w as [[] | ] eqn:Ew; cbn -[Nat.add] in Hq2.
all: match type of Etrans with trans _ (_, ?c) = _ => (eapply help_exists1; exists c, q_, w, m) || exfalso end; rewrite ?Em, ?Ew; cbn [curr].
all: repeat match type of Hq2 with _ \/ _ => destruct Hq2 as [Hq2 | Hq2] end; inversion Hq2; subst u v; clear Hq2; cbn -[Nat.add].
all: try eapply help_exists2.
all:
cbn [app] in HL;
match type of HL with
| ?L = ?R => match L with context C [! ?q :: ?c :: ?rs] => let ls := context C [@nil nat] in
replace L with (ls ++ !q ++ [c] ++ rs) in HL; [ | cbn; now simpl_list]
end
end.
all:
match type of HL with _ = enc_conf _ (?ls,?o,?rs) ?q =>
let H1 := fresh "H" in let H2 := fresh "H" in let H3 := fresh "H" in let H4 := fresh "H" in let HH := fresh "H" in
eapply enc_conf_inv in HL as (H1 & -> & H3 & H4); try rewrite H4 in *; destruct o as [ [] | ]; inversion H3; clear H3; cbn in H1;
rewrite ?app_nil_r in H1; subst;
split ; [ eassumption | ]
end.
all: try now (try (destruct rs as [ | [] rs]; cbn in H3; inversion H3; subst);
destruct x; try (now inversion H0); cbn in H0; eapply cons_inj in H0 as [HH H0]; try rewrite HH in *; clear HH; [
destruct ls as [ | ? ls _ ] using rev_ind; cbn in H0; inversion H0;
[ eexists [], _; split; reflexivity |
exfalso; rewrite rev_app_distr in H0; cbn in H0; inversion H0 ] |
destruct ls as [ | [] ls ]; cbn in H0;
destruct x; inversion H0; rewrite map_app in H0;
eapply app_inj_tail in H0 as []; lia ]).
all: try now (
try (destruct rs as [ | [] rs]; cbn in H3; inversion H3; subst);
destruct x; try (now inversion H0); cbn in H0; eapply cons_inj in H0 as [HH H0]; try rewrite HH in *; clear HH;
destruct ls; cbn in H0; try (rewrite map_app in H0; eapply app_inj_tail in H0 as [H0 H1]);
[ destruct x; inversion H0 |
destruct b; inversion H1 ;
now ((eexists _, (_ :: _) + eexists _, []); split; try reflexivity;
subst; cbn -[Nat.add]; now simpl_list)]).
all: try now (try (destruct rs as [ | [] rs]; cbn in H3; inversion H3; subst);
now ((eexists (_ :: ls), rs + eexists _, (_ :: _) + eexists _, [] + eexists _, _ + eexists (_ :: ls), rs); split; try reflexivity; cbn; now simpl_list)).
Qed.
Variable q_halt : state M.
Definition all_symsX {B} f : list B := [f X ; f tt ; f ff].
Definition Del := concat (all_symsX (fun c => all_syms (fun a => ([!q_halt; c ; a], [!q_halt ; c])))) ++
all_syms (fun a => ([a; !q_halt], [!q_halt])) ++
all_symsX (fun c => ( [⦇; !q_halt; c ; ⦈], [END])).
Lemma enc_conf_equiv ls o rs q :
enc_conf M (ls, o, rs) q = ([⦇] ++ map (fun b : bool => !!b) (rev ls)) ++ ([!q] ++ [encode_sym o]) ++ (map (fun b : bool => !!b) rs ++ [⦈]).
Proof.
unfold enc_conf. now simpl_list.
Qed.
Lemma sim_Del t :
SR.rewt Del (enc_conf M t q_halt) [END].
Proof.
destruct t as [[ls o] rs].
transitivity (enc_conf M (ls, o, []) q_halt). {
eapply rewt_subset. 2:{ unfold Del. eapply incl_appl. reflexivity. }
induction rs.
- reflexivity.
- cbn -[Nat.add]. destruct o as [ [] | ], a; (econstructor; [ eapply do_rew; [ | | eapply enc_conf_equiv ] | eapply IHrs]).
do 2 right; now left. reflexivity.
do 3 right; now left. reflexivity.
do 4 right; now left. reflexivity.
do 5 right; now left. reflexivity.
do 0 right; now left. reflexivity.
do 1 right; now left. reflexivity.
}
transitivity (enc_conf M ([], o, []) q_halt). {
eapply rewt_subset. 2:{ unfold Del. eapply incl_appr. eapply incl_appl. reflexivity. }
induction ls.
- reflexivity.
- cbn -[Nat.add]. destruct a; (econstructor; [ eapply do_rew; [ | | ] | eapply IHls]).
all: cbn - [Nat.add].
now left. cbn -[Nat.add]. simpl_list. cbn -[Nat.add]. instantiate (2 := 2 :: map (fun b : bool => !! b) (rev ls)). reflexivity. reflexivity.
right. now left. cbn -[Nat.add]. simpl_list. cbn -[Nat.add]. instantiate (2 := 2 :: map (fun b : bool => !! b) (rev ls)). reflexivity. reflexivity.
}
destruct o as [ [] | ]; (
eapply rewt_subset; [ | do 2 eapply incl_appr; reflexivity ]);
(cbn -[Nat.add]; econstructor; [ eapply do_rew with (x := []) (y := []); simpl_list; try reflexivity; cbn; eauto | reflexivity]).
Qed.
Lemma rev_sim_Del t q z :
SR.rew Del (enc_conf M t q) z -> q = q_halt /\ (z = END \/ exists t', z = enc_conf M t' q_halt).
Proof.
intros H. inversion H as [x y v u Hin HL HR]; subst z.
cbn -[Nat.add] in Hin.
destruct t as [[ls o] rs].
decompose [or] Hin; clear Hin. all: try tauto.
all: try specialize H0 as [= <- <-]. all: try specialize H1 as [= <- <-].
all:
cbn [app] in HL;
match type of HL with
| ?L = ?R => match L with context C [! ?q :: ?rs] => let ls := context C [@nil nat] in
replace L with (ls ++ !q ++ rs) in HL; [ | cbn; now simpl_list]
end
end; eapply enc_conf_inv' in HL as (H1 & <- & H3).
1-6, 9-11: subst; destruct o as [ [] | ]; inversion H3; split; clear H3; try reflexivity.
1-6, 9: destruct rs as [ | [] rs]; inversion H2; subst; rewrite app_nil_r in *.
1-6: destruct x; inversion H1; subst.
1-6: right; (eexists (ls, None, rs) + eexists (ls, Some true, rs) + ( eexists (ls, Some false, rs))) ; cbn -[Nat.add]; now simpl_list.
4,5: subst; split; try reflexivity; right.
4,5: destruct x; inversion H1; subst; clear H1; destruct ls as [ | ? ls ]; [ now destruct x; inversion H3; clear H3 |]; cbn in H3;
rewrite map_app in H3; cbn in H3; eapply app_inj_tail in H3 as [-> H3];
destruct b; inversion H3; exists (ls, o, rs); cbn; now simpl_list.
all: destruct x; inversion H1; subst; clear H1; cbn; eauto.
1,3,5: destruct ls as [ | []]; cbn in H4; [ destruct x; inversion H4 | | ]; rewrite map_app in H4;
eapply app_inj_tail in H4 as [H4 [=]].
1,2: destruct rs as [ | []]; inversion H2; eauto.
Qed.
Lemma enc_conf_END t q : ~ In END (@enc_conf M t q).
Proof.
destruct t as [[ls o] rs].
unfold enc_conf.
rewrite !in_app_iff, !in_map_iff; repeat setoid_rewrite <- in_rev. cbn.
intros H. decompose [or] H; try lia; firstorder; try lia.
all: try (destruct x; lia). destruct o as [[]|]; cbn in *; lia.
Qed.
Lemma rev_sim_Del_swap t q z :
SR.rew (map SR.swap Del) (enc_conf M t q) z -> q = q_halt /\ exists t', z = enc_conf M t' q_halt.
Proof.
intros H. inversion H as [x y v u Hin HL HR]; subst z.
cbn -[Nat.add] in Hin.
destruct t as [[ls o] rs].
decompose [or] Hin; clear Hin. all: try tauto.
all: try specialize H0 as [= <- <-]. all: try specialize H1 as [= <- <-].
1-8:
cbn [app] in HL;
match type of HL with
| ?L = ?R => match L with context C [! ?q :: ?rs] => let ls := context C [@nil nat] in
replace L with (ls ++ !q ++ rs) in HL; [ | cbn; now simpl_list]
end
end; eapply enc_conf_inv' in HL as (H1 & <- & H3).
1-6:destruct o as [ [] | ]; inversion H3; split; subst; try clear H3; try reflexivity.
all: rewrite ?app_nil_r in *; subst.
7,8: split; [ reflexivity | ].
1: exists (ls, None, true :: rs).
2: exists (ls, None, false :: rs).
3: exists (ls, Some true, true :: rs).
4: exists (ls, Some true, false :: rs).
5: exists (ls, Some false, true :: rs).
6: exists (ls, Some false, false :: rs).
1-6: cbn -[Nat.add]; now simpl_list.
1: exists (true :: ls, o, rs); cbn; now simpl_list.
1: exists (false :: ls, o, rs); cbn; now simpl_list.
all: edestruct enc_conf_END; rewrite <- HL; eauto.
Qed.
End FixM.
Lemma backwards M t q1 q:
(forall c, trans M (q,c) = None /\ (forall q', trans M (q', c) = None -> q' = q)) ->
SR.rewt ((R M ++ Del M q) ++ map SR.swap (R M ++ Del M q)) (enc_conf M t q1) [0] -> exists t', eval M q1 t q t'.
Proof.
intros Hq H. revert Hq. remember [0] as x. remember (enc_conf M t q1) as y.
induction H in q1, Heqy, Heqx, t |- *; subst; intros Hq.
+ edestruct enc_conf_END. rewrite <- Heqy. eauto.
+ rewrite map_app in H. rewrite !rew_app_inv in H. destruct H as [[H | H] | [H | H]].
* eapply rev_sim in H as (q' & w & m & H1 & H3). subst.
edestruct IHrewt as (H4 & H5); [reflexivity | eauto | eauto |].
eexists. econstructor. all: eassumption.
* eapply rev_sim_Del in H as [-> [H | (t' & ->)]].
-- do 2 econstructor. eapply Hq.
-- econstructor. econstructor. eapply Hq.
* eapply rev_sim_swap in H as (q' & w & m & t' & H1 & H3 & H4). subst.
edestruct IHrewt as (H4 & H5); [reflexivity | eauto | eauto |].
inversion H5; subst; clear H5; try congruence.
rewrite H in H1. inversion H1; subst; clear H1.
eexists. eassumption.
* eapply rev_sim_Del_swap in H as [ -> (t' & ->)].
do 2 econstructor. eapply Hq.
Qed.
Lemma reduction :
HaltSBTMu ⪯ SR.TSR.
Proof.
unshelve eexists. { intros [(M & q & H) t]. exact (R M ++ (Del M q), @enc_conf M t Fin.F1, [0]). }
intros [(M & q & Hq) t]. split.
- cbn -[Del R enc_state]. intros (t' & H).
etransitivity.
+ eapply rewt_subset. eapply simulation. eassumption. eauto.
+ eapply rewt_subset. eapply sim_Del. eauto.
- cbn -[Del R Nat.add]. intros H1. now eapply backwards.
Qed.
Require Import Undecidability.TM.SBTM.
Require Undecidability.StringRewriting.SR.
Require Import Undecidability.StringRewriting.Util.Definitions.
Require Import Undecidability.Synthetic.Definitions.
Require Import Undecidability.Synthetic.ReducibilityFacts.
Require Import Undecidability.StringRewriting.Reductions.HaltSBTMu_to_SRH.
Require Import Undecidability.Shared.ListAutomation.
Import ListNotations.
Set Default Proof Using "Type".
Section FixM.
Variable M : SBTM.
Notation END := 0.
Notation X := 1.
Notation "⦇" := 2.
Notation "⦈" := 3.
Notation tt := 4.
Notation ff := 5.
Notation "!! b" := (if b then tt else ff) (at level 1).
Notation "! p" := (@enc_state M p) (at level 1).
Lemma help_exists1 (P : state M -> tape -> option bool -> move -> Prop) :
(exists c q w m ls rs, P q (ls, c, rs) w m) -> (exists q t w m, P q t w m).
Proof.
intros (c & q & w & m & ls & rs & H). now exists q, (ls, c, rs), w, m.
Qed.
Lemma help_exists2 P Q :
(P /\ exists ls rs, Q ls rs) -> exists ls rs : list bool, P /\ Q ls rs.
Proof using M.
firstorder.
Qed.
Lemma rev_sim_swap t q z :
SR.rew (map SR.swap (R M)) (enc_conf M t q) z -> exists q' t' w m, trans M (q', curr t') = Some (q, w, m) /\ t = mv m (wr w t') /\ z = enc_conf M t' q'.
Proof.
intros H. inversion H as [x y v u Hin HL HR]; subst z.
eapply in_map_iff in Hin as ([? ?] & [= -> ->] & Hin).
destruct t as [[ls o] rs].
eapply in_flat_map in Hin as (q_ & _ & Hq2).
unfold rules in Hq2.
rewrite ! in_app_iff in Hq2.
destruct Hq2 as [ Hq2 | [Hq2 | Hq2]].
all: destruct (trans M (q_, _)) as [ [[q' w] m] | ] eqn:Etrans; try destruct m eqn:Em;
try destruct w as [[] | ] eqn:Ew; cbn -[Nat.add] in Hq2.
all: match type of Etrans with trans _ (_, ?c) = _ => (eapply help_exists1; exists c, q_, w, m) || exfalso end; rewrite ?Em, ?Ew; cbn [curr].
all: repeat match type of Hq2 with _ \/ _ => destruct Hq2 as [Hq2 | Hq2] end; inversion Hq2; subst u v; clear Hq2; cbn -[Nat.add].
all: try eapply help_exists2.
all:
cbn [app] in HL;
match type of HL with
| ?L = ?R => match L with context C [! ?q :: ?c :: ?rs] => let ls := context C [@nil nat] in
replace L with (ls ++ !q ++ [c] ++ rs) in HL; [ | cbn; now simpl_list]
end
end.
all:
match type of HL with _ = enc_conf _ (?ls,?o,?rs) ?q =>
let H1 := fresh "H" in let H2 := fresh "H" in let H3 := fresh "H" in let H4 := fresh "H" in let HH := fresh "H" in
eapply enc_conf_inv in HL as (H1 & -> & H3 & H4); try rewrite H4 in *; destruct o as [ [] | ]; inversion H3; clear H3; cbn in H1;
rewrite ?app_nil_r in H1; subst;
split ; [ eassumption | ]
end.
all: try now (try (destruct rs as [ | [] rs]; cbn in H3; inversion H3; subst);
destruct x; try (now inversion H0); cbn in H0; eapply cons_inj in H0 as [HH H0]; try rewrite HH in *; clear HH; [
destruct ls as [ | ? ls _ ] using rev_ind; cbn in H0; inversion H0;
[ eexists [], _; split; reflexivity |
exfalso; rewrite rev_app_distr in H0; cbn in H0; inversion H0 ] |
destruct ls as [ | [] ls ]; cbn in H0;
destruct x; inversion H0; rewrite map_app in H0;
eapply app_inj_tail in H0 as []; lia ]).
all: try now (
try (destruct rs as [ | [] rs]; cbn in H3; inversion H3; subst);
destruct x; try (now inversion H0); cbn in H0; eapply cons_inj in H0 as [HH H0]; try rewrite HH in *; clear HH;
destruct ls; cbn in H0; try (rewrite map_app in H0; eapply app_inj_tail in H0 as [H0 H1]);
[ destruct x; inversion H0 |
destruct b; inversion H1 ;
now ((eexists _, (_ :: _) + eexists _, []); split; try reflexivity;
subst; cbn -[Nat.add]; now simpl_list)]).
all: try now (try (destruct rs as [ | [] rs]; cbn in H3; inversion H3; subst);
now ((eexists (_ :: ls), rs + eexists _, (_ :: _) + eexists _, [] + eexists _, _ + eexists (_ :: ls), rs); split; try reflexivity; cbn; now simpl_list)).
Qed.
Variable q_halt : state M.
Definition all_symsX {B} f : list B := [f X ; f tt ; f ff].
Definition Del := concat (all_symsX (fun c => all_syms (fun a => ([!q_halt; c ; a], [!q_halt ; c])))) ++
all_syms (fun a => ([a; !q_halt], [!q_halt])) ++
all_symsX (fun c => ( [⦇; !q_halt; c ; ⦈], [END])).
Lemma enc_conf_equiv ls o rs q :
enc_conf M (ls, o, rs) q = ([⦇] ++ map (fun b : bool => !!b) (rev ls)) ++ ([!q] ++ [encode_sym o]) ++ (map (fun b : bool => !!b) rs ++ [⦈]).
Proof.
unfold enc_conf. now simpl_list.
Qed.
Lemma sim_Del t :
SR.rewt Del (enc_conf M t q_halt) [END].
Proof.
destruct t as [[ls o] rs].
transitivity (enc_conf M (ls, o, []) q_halt). {
eapply rewt_subset. 2:{ unfold Del. eapply incl_appl. reflexivity. }
induction rs.
- reflexivity.
- cbn -[Nat.add]. destruct o as [ [] | ], a; (econstructor; [ eapply do_rew; [ | | eapply enc_conf_equiv ] | eapply IHrs]).
do 2 right; now left. reflexivity.
do 3 right; now left. reflexivity.
do 4 right; now left. reflexivity.
do 5 right; now left. reflexivity.
do 0 right; now left. reflexivity.
do 1 right; now left. reflexivity.
}
transitivity (enc_conf M ([], o, []) q_halt). {
eapply rewt_subset. 2:{ unfold Del. eapply incl_appr. eapply incl_appl. reflexivity. }
induction ls.
- reflexivity.
- cbn -[Nat.add]. destruct a; (econstructor; [ eapply do_rew; [ | | ] | eapply IHls]).
all: cbn - [Nat.add].
now left. cbn -[Nat.add]. simpl_list. cbn -[Nat.add]. instantiate (2 := 2 :: map (fun b : bool => !! b) (rev ls)). reflexivity. reflexivity.
right. now left. cbn -[Nat.add]. simpl_list. cbn -[Nat.add]. instantiate (2 := 2 :: map (fun b : bool => !! b) (rev ls)). reflexivity. reflexivity.
}
destruct o as [ [] | ]; (
eapply rewt_subset; [ | do 2 eapply incl_appr; reflexivity ]);
(cbn -[Nat.add]; econstructor; [ eapply do_rew with (x := []) (y := []); simpl_list; try reflexivity; cbn; eauto | reflexivity]).
Qed.
Lemma rev_sim_Del t q z :
SR.rew Del (enc_conf M t q) z -> q = q_halt /\ (z = END \/ exists t', z = enc_conf M t' q_halt).
Proof.
intros H. inversion H as [x y v u Hin HL HR]; subst z.
cbn -[Nat.add] in Hin.
destruct t as [[ls o] rs].
decompose [or] Hin; clear Hin. all: try tauto.
all: try specialize H0 as [= <- <-]. all: try specialize H1 as [= <- <-].
all:
cbn [app] in HL;
match type of HL with
| ?L = ?R => match L with context C [! ?q :: ?rs] => let ls := context C [@nil nat] in
replace L with (ls ++ !q ++ rs) in HL; [ | cbn; now simpl_list]
end
end; eapply enc_conf_inv' in HL as (H1 & <- & H3).
1-6, 9-11: subst; destruct o as [ [] | ]; inversion H3; split; clear H3; try reflexivity.
1-6, 9: destruct rs as [ | [] rs]; inversion H2; subst; rewrite app_nil_r in *.
1-6: destruct x; inversion H1; subst.
1-6: right; (eexists (ls, None, rs) + eexists (ls, Some true, rs) + ( eexists (ls, Some false, rs))) ; cbn -[Nat.add]; now simpl_list.
4,5: subst; split; try reflexivity; right.
4,5: destruct x; inversion H1; subst; clear H1; destruct ls as [ | ? ls ]; [ now destruct x; inversion H3; clear H3 |]; cbn in H3;
rewrite map_app in H3; cbn in H3; eapply app_inj_tail in H3 as [-> H3];
destruct b; inversion H3; exists (ls, o, rs); cbn; now simpl_list.
all: destruct x; inversion H1; subst; clear H1; cbn; eauto.
1,3,5: destruct ls as [ | []]; cbn in H4; [ destruct x; inversion H4 | | ]; rewrite map_app in H4;
eapply app_inj_tail in H4 as [H4 [=]].
1,2: destruct rs as [ | []]; inversion H2; eauto.
Qed.
Lemma enc_conf_END t q : ~ In END (@enc_conf M t q).
Proof.
destruct t as [[ls o] rs].
unfold enc_conf.
rewrite !in_app_iff, !in_map_iff; repeat setoid_rewrite <- in_rev. cbn.
intros H. decompose [or] H; try lia; firstorder; try lia.
all: try (destruct x; lia). destruct o as [[]|]; cbn in *; lia.
Qed.
Lemma rev_sim_Del_swap t q z :
SR.rew (map SR.swap Del) (enc_conf M t q) z -> q = q_halt /\ exists t', z = enc_conf M t' q_halt.
Proof.
intros H. inversion H as [x y v u Hin HL HR]; subst z.
cbn -[Nat.add] in Hin.
destruct t as [[ls o] rs].
decompose [or] Hin; clear Hin. all: try tauto.
all: try specialize H0 as [= <- <-]. all: try specialize H1 as [= <- <-].
1-8:
cbn [app] in HL;
match type of HL with
| ?L = ?R => match L with context C [! ?q :: ?rs] => let ls := context C [@nil nat] in
replace L with (ls ++ !q ++ rs) in HL; [ | cbn; now simpl_list]
end
end; eapply enc_conf_inv' in HL as (H1 & <- & H3).
1-6:destruct o as [ [] | ]; inversion H3; split; subst; try clear H3; try reflexivity.
all: rewrite ?app_nil_r in *; subst.
7,8: split; [ reflexivity | ].
1: exists (ls, None, true :: rs).
2: exists (ls, None, false :: rs).
3: exists (ls, Some true, true :: rs).
4: exists (ls, Some true, false :: rs).
5: exists (ls, Some false, true :: rs).
6: exists (ls, Some false, false :: rs).
1-6: cbn -[Nat.add]; now simpl_list.
1: exists (true :: ls, o, rs); cbn; now simpl_list.
1: exists (false :: ls, o, rs); cbn; now simpl_list.
all: edestruct enc_conf_END; rewrite <- HL; eauto.
Qed.
End FixM.
Lemma backwards M t q1 q:
(forall c, trans M (q,c) = None /\ (forall q', trans M (q', c) = None -> q' = q)) ->
SR.rewt ((R M ++ Del M q) ++ map SR.swap (R M ++ Del M q)) (enc_conf M t q1) [0] -> exists t', eval M q1 t q t'.
Proof.
intros Hq H. revert Hq. remember [0] as x. remember (enc_conf M t q1) as y.
induction H in q1, Heqy, Heqx, t |- *; subst; intros Hq.
+ edestruct enc_conf_END. rewrite <- Heqy. eauto.
+ rewrite map_app in H. rewrite !rew_app_inv in H. destruct H as [[H | H] | [H | H]].
* eapply rev_sim in H as (q' & w & m & H1 & H3). subst.
edestruct IHrewt as (H4 & H5); [reflexivity | eauto | eauto |].
eexists. econstructor. all: eassumption.
* eapply rev_sim_Del in H as [-> [H | (t' & ->)]].
-- do 2 econstructor. eapply Hq.
-- econstructor. econstructor. eapply Hq.
* eapply rev_sim_swap in H as (q' & w & m & t' & H1 & H3 & H4). subst.
edestruct IHrewt as (H4 & H5); [reflexivity | eauto | eauto |].
inversion H5; subst; clear H5; try congruence.
rewrite H in H1. inversion H1; subst; clear H1.
eexists. eassumption.
* eapply rev_sim_Del_swap in H as [ -> (t' & ->)].
do 2 econstructor. eapply Hq.
Qed.
Lemma reduction :
HaltSBTMu ⪯ SR.TSR.
Proof.
unshelve eexists. { intros [(M & q & H) t]. exact (R M ++ (Del M q), @enc_conf M t Fin.F1, [0]). }
intros [(M & q & Hq) t]. split.
- cbn -[Del R enc_state]. intros (t' & H).
etransitivity.
+ eapply rewt_subset. eapply simulation. eassumption. eauto.
+ eapply rewt_subset. eapply sim_Del. eauto.
- cbn -[Del R Nat.add]. intros H1. now eapply backwards.
Qed.