proposition: Lemma pointwise_decision K x : {bounded K x} + {not (bounded K x)}.
proof: Proof. case HK: (steps K x) => [y|]. - have [Hy|Hy] := In_dec option_mm2_state_eq_dec (Some y) (path K x). + left. apply: loop_bounded. by rewrite HK. + right. apply: (NoDup_not_bounded HK). apply: path_noloopI. by rewrite HK. - left. by apply: mortal_bounded. Qed.
imports: List ListDec PeanoNat Lia Relation_Operators Operators_Properties Permutation Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun