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