proposition: Lemma inverse_simulation_step L R X : exists (x: State) (b_x: bool) (l r: list Symbol) (b_y: bool), forall L' R' Y, step MN (L, R, X) (L', R', Y) -> exists (y: State) (l' r': list Symbol), (L, R, X) = (encode_Stack l, encode_Stack r, to_nat (x, b_x)) /\ (L', R', Y) = (encode_Stack l', encode_Stack r', to_nat (y, b_y)) /\ match b_x, b_y with | false, false => SMX.step MX (l, r, x) (l', r', y) | false, true => SMX.step MX (l, r, x) (r', l', y) | true, false => SMX.step MX (r, l, x) (l', r', y) | true, true => SMX.step MX (r, l, x) (r', l', y) end.
proof: Proof. Proof using flip_consistent_MX. set x_b_x : State * bool := of_nat X. move Hx_b_x: x_b_x => [x b_x]. subst x_b_x. exists x, b_x, (decode_Stack L), (decode_Stack R). have := Exists_dec (fun '((_, X), _, b) => X = x) MX. move=> /(_ ltac:(move=> [[[? ?] ?] ?]; do 3 (decide equality))). case; first last. { move Hx': (L, R, X) => x' HMX. exists false. move=> L' R' Y HXY. exfalso. apply: HMX. apply /Exists_exists. case: HXY Hx'. move=> >. rewrite /MN in_flat_map. move=> [[[[[? ?] ?] [[? ?] ?]] b]] + [] *. subst. move=> [H2MX HX]. eexists. constructor; first by eassumption. move=> /=. move: b HX {H2MX} => /= [|]. { case. - move=> [] *. subst. move: Hx_b_x. by rewrite enumP => [[]]. - case; last done. move=> [] *. subst. move: Hx_b_x. by rewrite enumP => [[]]. } case. - move=> [] *. subst. move: Hx_b_x. by rewrite enumP => [[]]. - case; last done. move=> [] *. subst. move: Hx_b_x. by rewrite enumP => [[]]. } rewrite Exists_exists. move=> [[[[[? ?] x'] [[? ?] ?]] b'] [H2MX ?]]. subst x'. exists (if b' then negb b_x else b_x). move=> L' R' Y. move Hc: (L, R, X) => c. move Hd: (L', R', Y) => d Hcd. case: Hcd Hc Hd Hx_b_x. move=> v w r1 s1 r2 s2 x' y + [] ? ? ? [] ? ? ?; subst. rewrite /MN in_flat_map. move=> [[[[[? ?] ?] [[? ?] ?]] b]]. move=> + Hx_b_x. rewrite ?encode_decode_Stack -Hx_b_x. case: b. { move=> [HMX] /=. case. - move=> [] *. subst. move: Hx_b_x. rewrite ?enumP. move=> [? ?]. subst. have ? := flip_consistent_MX _ _ _ _ _ _ _ _ _ HMX H2MX. subst b'. rewrite -(@encode_decode_Stack v) -(@encode_decode_Stack w) -?encode_Stack_app. do 3 eexists. constructor; first by reflexivity. constructor; first by reflexivity. move: HMX => /(SMX.transition MX). rewrite ?decode_encode_Stack. by apply. - case; last done. move=> [] *. subst. move: Hx_b_x. rewrite ?enumP. move=> [? ?]. subst. have ? := flip_consistent_MX _ _ _ _ _ _ _ _ _ HMX H2MX. subst b'. rewrite -(@encode_decode_Stack v) -(@encode_decode_Stack w) -?encode_Stack_app. do 3 eexists. constructor; first by reflexivity. constructor; first by reflexivity. move: HMX => /(SMX.transition MX). rewrite ?decode_encode_Stack. by apply. } move=> [HMX] /=. case. - move=> [] *. subst. move: Hx_b_x. rewrite ?enumP. move=> [? ?]. subst. have ? := flip_consistent_MX _ _ _ _ _ _ _ _ _ HMX H2MX. subst b'. rewrite -(@encode_decode_Stack v) -(@encode_decode_Stack w) -?encode_Stack_app. do 3 eexists. constructor; first by reflexivity. constructor; first by reflexivity. move: HMX => /(SMX.transition MX). rewrite ?decode_encode_Stack. by apply. - case; last done. move=> [] *. subst. move: Hx_b_x. rewrite ?enumP. move=> [? ?]. subst. have ? := flip_consistent_MX _ _ _ _ _ _ _ _ _ HMX H2MX. subst b'. rewrite -(@encode_decode_Stack v) -(@encode_decode_Stack w) -?encode_Stack_app. do 3 eexists. constructor; first by reflexivity. constructor; first by reflexivity. move: HMX => /(SMX.transition MX). rewrite ?decode_encode_Stack. apply. Qed.
imports: Relation_Operators Lia PeanoNat List Undecidability.StackMachines.SMN Undecidability.StackMachines.Util(Nat_facts List_facts Enumerable) Undecidability.StackMachines.Reductions.CM1_HALT_to_SMNdl_UB.CM1_to_SMX ssreflect ssrbool ssrfun