proposition: Lemma step_dec (X Y: config) : decidable (step M X Y).
proof: Proof. case: (Exists_dec (fun '(x, y, a, b, d) => (get_state X, get_state Y, if d then get_left X else b :: get_left X, if d then b :: get_right X else get_right X) = (x, y, if d then a :: get_left Y else get_left Y, if d then get_right Y else a :: get_right Y)) M). - move=> [[[[x y] a] b] d]. do 4 (decide equality). - move=> H. left. move: H. rewrite Exists_exists. move=> [[[[[x y] a] b] d]]. case: d. + move=> [?]. move: X Y => [[A ?] ?] [[? B] ?] /=. case: A; case: B=> //=. move=> >. case=> *. subst. by apply: step_l. + move=> [?]. move: X Y => [[? B] ?] [[A ?] ?] /=. case: A; case: B=> //=. move=> >. case=> *. subst. by apply: step_r. - move=> H. right. move=> HXY. apply: H. rewrite Exists_exists. case: HXY. + move=> x y a b A B H. exists (x, y, a, b, true) => /=. by constructor. + move=> x y a b A B H. exists (x, y, b, a, false) => /=. by constructor. Qed.
imports: PeanoNat Lia Relation_Operators Operators_Properties List ssreflect ssrfun ssrbool Undecidability.StackMachines.SSM