proposition: Lemma simulation {c d} : SMX.reachable MX c d -> let '(l, r, x) := c in let '(l', r', y) := d in (reachable MN (encode_Stack r, encode_Stack l, to_nat (x, true)) (encode_Stack r', encode_Stack l', to_nat (y, true)) \/ reachable MN (encode_Stack r, encode_Stack l, to_nat (x, true)) (encode_Stack l', encode_Stack r', to_nat (y, false))) /\ (reachable MN (encode_Stack l, encode_Stack r, to_nat (x, false)) (encode_Stack l', encode_Stack r', to_nat (y, false)) \/ reachable MN (encode_Stack l, encode_Stack r, to_nat (x, false)) (encode_Stack r', encode_Stack l', to_nat (y, true))).
proof: Proof. elim. - move=> [[l r] x] [[l' r'] y] Hxy. constructor. + have [? | ?] := simulation_step_true Hxy; [left | right]; by apply: rt_step. + have [? | ?] := simulation_step_false Hxy; [left | right]; by apply: rt_step. - move=> [[l r] x]. constructor; left; by apply rt_refl. - move=> [[lx rx] x] [[ly ry] y] [[lz rz] z] _ Hxy _ Hyz. constructor. + move: Hxy Hyz => [[Hxy|Hxy] _]. * move=> [[Hyz|Hyz] _]; [left | right]; apply: rt_trans; by eassumption. * move=> [_ [Hyz|Hyz]]; [right | left]; apply: rt_trans; by eassumption. + move: Hxy Hyz => [_ [Hxy|Hxy]]. * move=> [_ [Hyz|Hyz]]; [left | right]; apply: rt_trans; by eassumption. * move=> [[Hyz|Hyz] _]; [right | left] ; apply: rt_trans; by eassumption. 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