proposition: Lemma narrow_dec (X: config) : decidable (narrow X).
proof: Proof. case: (Exists_dec (fun Y => get_right Y = [] /\ equiv X Y) (space X)). - move=> [[A + ] y]. case; first last. { move=> >. right. by move=> [+]. } case: (equiv_dec X (A, [], y)). + move=> ?. by left. + move=> ?. right. by move=> [_]. - move=> + /ltac:(left). rewrite Exists_exists. move=> [[[A B] y] [_]] /= [->] ?. by exists y, A. - move=> + /ltac:(right) => + [y [A HX]]. rewrite Exists_exists. apply. exists (A, [], y). constructor; last done. by apply: space_equivP. Qed.
imports: PeanoNat Lia Relation_Operators Operators_Properties List ssreflect ssrfun ssrbool Undecidability.StackMachines.SSM