Require Import List Relation_Operators Operators_Properties Lia.
Import ListNotations.
Require Import Undecidability.StringRewriting.Reductions.CM2_HALT_to_SSTS01.SR2ab.
Require Import ssreflect.
Set Default Goal Selector "!".
Lemma sym_eq_dec (x y: Symbol) : {x = y} + {x <> y}.
Proof. by do 3 (decide equality). Qed.
Lemma stepI {srs u v a b c d s t} :
s = (u ++ a :: b :: v) -> t = (u ++ c :: d :: v) -> In ((a, b), (c, d)) srs ->
step srs s t.
Proof. move=> -> ->. by constructor. Qed.
Lemma multi_step_appI {srs u v s t} : multi_step srs s t -> multi_step srs (u ++ s ++ v) (u ++ t ++ v).
Proof.
elim; [| move=> *; by apply: rt_refl | move=> *; apply: rt_trans; by eassumption ].
move=> {}s {}t [] u' v' > ?.
apply /rt_step /(stepI (u := u ++ u') (v := v' ++ v)); last by eassumption.
all: by rewrite -?app_assoc.
Qed.
Lemma multi_step_applI {srs u s t} : multi_step srs s t -> multi_step srs (u ++ s) (u ++ t).
Proof. move=> /multi_step_appI => /(_ u []). by rewrite ?app_nil_r. Qed.
Lemma multi_step_apprI {srs v s t} : multi_step srs s t -> multi_step srs (s ++ v) (t ++ v).
Proof. by move=> /multi_step_appI => /(_ [] v). Qed.
Import ListNotations.
Require Import Undecidability.StringRewriting.Reductions.CM2_HALT_to_SSTS01.SR2ab.
Require Import ssreflect.
Set Default Goal Selector "!".
Lemma sym_eq_dec (x y: Symbol) : {x = y} + {x <> y}.
Proof. by do 3 (decide equality). Qed.
Lemma stepI {srs u v a b c d s t} :
s = (u ++ a :: b :: v) -> t = (u ++ c :: d :: v) -> In ((a, b), (c, d)) srs ->
step srs s t.
Proof. move=> -> ->. by constructor. Qed.
Lemma multi_step_appI {srs u v s t} : multi_step srs s t -> multi_step srs (u ++ s ++ v) (u ++ t ++ v).
Proof.
elim; [| move=> *; by apply: rt_refl | move=> *; apply: rt_trans; by eassumption ].
move=> {}s {}t [] u' v' > ?.
apply /rt_step /(stepI (u := u ++ u') (v := v' ++ v)); last by eassumption.
all: by rewrite -?app_assoc.
Qed.
Lemma multi_step_applI {srs u s t} : multi_step srs s t -> multi_step srs (u ++ s) (u ++ t).
Proof. move=> /multi_step_appI => /(_ u []). by rewrite ?app_nil_r. Qed.
Lemma multi_step_apprI {srs v s t} : multi_step srs s t -> multi_step srs (s ++ v) (t ++ v).
Proof. by move=> /multi_step_appI => /(_ [] v). Qed.