proposition: Lemma inverse_simulation {x y} : reachable MN x y -> x = y \/ let '(L, R, X) := x in let '(L', R', Y) := y in exists (x y: State) (b_x b_y: bool) (l r 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.reachable MX (l, r, x) (l', r', y) | false, true => SMX.reachable MX (l, r, x) (r', l', y) | true, false => SMX.reachable MX (r, l, x) (l', r', y) | true, true => SMX.reachable MX (r, l, x) (r', l', y) end.
proof: Proof. Proof using flip_consistent_MX. elim. - move=> [[L R] X]. have [{}x [b_x [l [r [b_y Hx]]]]] := inverse_simulation_step L R X. move=> [[? ?] ?] /Hx{Hx} => [[{}y]] [l'] [r'] [->] [->] Hxy. right. do 8 eexists. constructor; first by reflexivity. constructor; first by reflexivity. move: b_x b_y Hxy => [|] [|] Hxy; by apply: rt_step. - move=> ?. by left. - move=> [[L1 R1] X1] [[L2 R2] X2] [[L3 R3] X3]. move=> _ [[] ? ? ?|IH1]; first by subst. move=> _ [[] ? ? ?|IH2]; first by (subst; right). move: IH1 => [x1] [y1] [b_x1] [b_y1] [l1] [r1] [l'1] [r'1] [[]] ? ? ? [[]] ? ? ? Hx1y1. move: IH2 => [x2] [y2] [b_x2] [b_y2] [l2] [r2] [l'2] [r'2] [[]] ? ? ? [[]] ? ? ? Hx2y2. subst. right. exists x1, y2, b_x1, b_y2, l1, r1, l'2, r'2. constructor; first done. constructor; first done. have [? ?]: (y1, b_y1) = (x2, b_x2) by apply /to_nat_inj. have ?: l'1 = l2 by (apply: encode_Stack_inj; congruence). have ?: r'1 = r2 by (apply: encode_Stack_inj; congruence). subst. move: Hx1y1 Hx2y2. clear. move: b_x1 b_x2 b_y2 => [|] [|] [|]; by apply: rt_trans. 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