proposition: Lemma pointwise_decision x : {mortal K x} + {not (mortal K x)}.
proof: Proof. case H'Kx: (steps (S K) x) => [y|]. - right => /mortal_steps_iff. by rewrite H'Kx. - left. by apply /mortal_steps_iff. Qed.
imports: List PeanoNat Lia Relation_Operators Operators_Properties ConstructiveEpsilon Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Deciders.MM2_UBOUNDED_dec Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun