proposition: Lemma remove_rendundant_suffixR {x: state} {A B: stack} {b: symbol} {Y: config} : reachable M (A, B++[b], x) Y -> (exists (x': state) (A': stack), reachable M (A, B++[b], x) (A', [], x')) \/ (exists (D: stack), get_right Y = D ++ [b] /\ reachable M (A, B, x) (get_left Y, D, get_state Y)).
proof: Proof. move HX: (A, B ++ [b], x) => X H. elim: H x A B b HX. - move=> ? ?. case. + move=> > ? >. case=> -> <- ->. right. eexists. constructor. * rewrite app_comm_cons. by reflexivity. * apply: rt_step. by apply: step_l. + move=> x y a b A. case. * move=> ? > _. left. exists y, (a::A). apply: rt_step. by apply: step_r. * move=> b' B ? >. have [B'' [b'' ->]] := (@exists_last _ (b' :: B) ltac:(done)). case=> ?. rewrite app_comm_cons. move /(@app_inj_tail symbol). case=> ? ? ?. subst. right. exists B''. constructor; first done. apply: rt_step. by apply: step_r. - move=> > <-. right. eexists. constructor; first by reflexivity. by apply: rt_refl. - move=> {}X {}[[A' B'] x'] Z. move=> _ IH1 _ IH2 x A B b ?. subst. case: (IH1 x A B b ltac:(done)). { move=> ?. by left. } move=> /= [D' [? Hxx']]. subst. case: (IH2 x' A' D' b ltac:(done)). + move=> [x'' [A'' ?]]. left. exists x'', A''. apply: rt_trans; last by eassumption. have -> : (A = A ++ []) by rewrite app_nil_r. have -> : (A' = A' ++ []) by rewrite app_nil_r. by apply: reachable_app. + move=> [D'' [? ?]]. right. exists D''. constructor; first done. apply: rt_trans; by eassumption. Qed.
imports: PeanoNat Lia Relation_Operators Operators_Properties List ssreflect ssrfun ssrbool Undecidability.StackMachines.SSM