proposition: Theorem mma_mma2_zero_reduction P s : (1,P) /A/ s ~~> (0,vec_zero) <-> map mma_mm2_instr P /2/ mma_mm2_state s ↠ (0,(0,0)).
proof: Proof. rewrite <- mma_mm2_terminates_zero_equiv; split. + intros []; auto. + intros H; split; auto; simpl; lia. Qed.
imports: List Arith Relations Lia Undecidability.Synthetic.Definitions Undecidability.Shared.Libs.DLW(utils pos vec sss subcode) Undecidability.MinskyMachines(MM2 mma_defs)