proposition: Lemma bounded_MN : bounded MN (1 + 4*NMX).
proof: Proof. Proof using flip_consistent_MX bounded_MX. rewrite /bounded. move=> [[L R] X]. set x_b_x : State * bool := of_nat X. move Hx: x_b_x => [x b_x]. have [T1 [H1T1 H2T1]] := bounded_MX (decode_Stack L, decode_Stack R, x). have [T2 [H1T2 H2T2]] := bounded_MX (decode_Stack R, decode_Stack L, x). exists ([(L, R, X)] ++ flat_map (fun '(l, r, x) => [(encode_Stack l, encode_Stack r, to_nat (x, b_x)); (encode_Stack r, encode_Stack l, to_nat (x, negb b_x))]) T1 ++ flat_map (fun '(l, r, x) => [(encode_Stack l, encode_Stack r, to_nat (x, negb b_x)); (encode_Stack r, encode_Stack l, to_nat (x, b_x))]) T2). constructor. { move=> [[L' R'] Y] /inverse_simulation. case. { move=> <-. by left. } move=> [x'] [y'] [b_x'] [b_y'] [l] [r] [l'] [r']. move=> [[]] ? ? ? [[]] ? ? ?. subst. have [? ?] : (x, b_x) = (x', b_x') by rewrite -Hx /x_b_x enumP. subst. move Hb_x: (b_x') => b_x. move Hb_y: (b_y') => b_y. rewrite ?decode_encode_Stack in H1T1. rewrite ?decode_encode_Stack in H1T2. move: b_x b_y Hb_x Hb_y => [|] [|] ? ?; subst; rewrite ?in_app_iff ?in_flat_map. - move /H1T2 => ?. right. right. eexists. constructor; first by eassumption. move=> /=. by firstorder done. - move /H1T2 => ?. right. right. eexists. constructor; first by eassumption. move=> /=. by firstorder done. - move /H1T1 => ?. right. left. eexists. constructor; first by eassumption. move=> /=. by firstorder done. - move /H1T1 => ?. right. left. eexists. constructor; first by eassumption. move=> /=. by firstorder done. } rewrite ?app_length. set f1 := (f in (flat_map f T1)). set f2 := (f in (flat_map f T2)). have /(legnth_flat_map (l := T1)): (forall a, length (f1 a) <= 2). { move=> [[? ?] ?]. rewrite /f1 /length. by lia. } have /(legnth_flat_map (l := T2)): (forall a, length (f2 a) <= 2). { move=> [[? ?] ?]. rewrite /f2 /length. by lia. } rewrite /length -?/(length _). move: H2T1 H2T2. move: (length _) (length _). by lia. 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