proposition: Lemma SM_to_SUcsP {x y: state} {a b: symbol} : In (a, x, (y, b)) (SM_to_SUcs M) -> exists x' y', x = (embed ([], [], x')) /\ y = (embed ([], [], y')) /\ equiv ([a], [], x') ([], [b], y').
proof: Proof. rewrite /SM_to_SUcs in_map_iff. move=> [[[[[x' y'] a'] b'] d]]. case: d. - case. case=> <- <- <- <- H. exists x', y'. constructor; first done. constructor; first done. exists ([], [b'], y'). constructor; [apply: rt_step; by apply: step_l | by apply: rt_refl]. - case. case=> <- <- <- <- H. exists y', x'. constructor; first done. constructor; first done. exists ([b'], [], y'). constructor; [by apply: rt_refl | apply: rt_step; by apply: step_r]. Qed.
imports: List PeanoNat Lia Relations.Relation_Operators Relations.Operators_Properties Undecidability.StackMachines(SSM) Undecidability.StackMachines.Util(CSSM_facts) Undecidability.SemiUnification.SemiU Undecidability.SemiUnification.Util(Enumerable) ssreflect ssrfun ssrbool