proposition: Theorem decision : (mm2_reversible M) + (not (mm2_reversible M)).
proof: Proof. pose t := list_prod (seq 1 l) (list_prod [0;1;2] [0;1;2]). pose P := fun '(x, y) => forall z, step x z -> step y z -> x = y. have: forall xy, {P xy} + {~ P xy}. { move=> [x y]. subst P. have [<-|?] := mm2_state_eq_dec x y. { left. tauto. } have [[z1 Hxz1]|Hx] := mm2_sig_step_dec M x. - have [[z2 Hyz2]|Hy] := mm2_sig_step_dec M y. + have [?|?] := mm2_state_eq_dec z2 z1. * right. subst z2. by move=> /(_ z1 Hxz1 Hyz2). * left => ?. move: Hxz1 => /mm2_step_det /[apply] <-. by move: Hyz2 => /mm2_step_det /[apply]. + by left => ?? /Hy. - by left => ? /Hx. } move=> /(Forall_Exists_dec P) /(_ (list_prod t t)). case. { move=> /finite_characterization ?. by left. } move=> H. right. move: H => /Exists_exists [[x y]] [H'xy] Hxy HM. apply: Hxy. by apply: HM. Qed.
imports: List ListDec PeanoNat Lia Operators_Properties Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun