proposition: Lemma dec_stepI {x y} : step x y -> index y = 1 -> (value1 y < value1 x -> In (mm2_dec_a 1) M) /\ (value2 y < value2 x -> In (mm2_dec_b 1) M).
proof: Proof. move=> [i] [+ Hxy]. case: Hxy => > /=; [lia|lia| | |lia|lia]. - move=> /[dup] /mm2_instr_at_pos -> /nth_error_Some_mm2_instr_at_iff /nth_error_In *. subst. by split; [|lia]. - move=> /[dup] /mm2_instr_at_pos -> /nth_error_Some_mm2_instr_at_iff /nth_error_In *. subst. by split; [lia|]. Qed.
imports: List PeanoNat Lia Relation_Operators Operators_Properties Transitive_Closure Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun