Require Import Undecidability.Synthetic.Definitions Undecidability.Synthetic.ReducibilityFacts.
Require Import Undecidability.TM.TM.
Require Import Undecidability.TM.SBTM.
Require Import Undecidability.StringRewriting.SR.
Require Undecidability.TM.Reductions.HaltTM_1_to_HaltSBTM Undecidability.TM.Reductions.HaltSBTM_to_HaltSBTMu.
From Undecidability.StringRewriting.Reductions Require HaltSBTMu_to_SRH SRH_to_SR.
Theorem reduction : HaltTM 1 ⪯ SR.
Proof.
apply (reduces_transitive HaltTM_1_to_HaltSBTM.reduction).
apply (reduces_transitive HaltSBTM_to_HaltSBTMu.reduction).
apply (reduces_transitive HaltSBTMu_to_SRH.reduction).
exact SRH_to_SR.reduction.
Qed.
Require Import Undecidability.TM.TM.
Require Import Undecidability.TM.SBTM.
Require Import Undecidability.StringRewriting.SR.
Require Undecidability.TM.Reductions.HaltTM_1_to_HaltSBTM Undecidability.TM.Reductions.HaltSBTM_to_HaltSBTMu.
From Undecidability.StringRewriting.Reductions Require HaltSBTMu_to_SRH SRH_to_SR.
Theorem reduction : HaltTM 1 ⪯ SR.
Proof.
apply (reduces_transitive HaltTM_1_to_HaltSBTM.reduction).
apply (reduces_transitive HaltSBTM_to_HaltSBTMu.reduction).
apply (reduces_transitive HaltSBTMu_to_SRH.reduction).
exact SRH_to_SR.reduction.
Qed.