proposition: Fact mma_mm2_terminates P s : (1,P) /A/ s ↓ -> map mma_mm2_instr P /2/ mma_mm2_state s ↓.
proof: Proof. intros (y & H1 & H2). exists (mma_mm2_state y); split. + apply mma_mm2_compute_equiv; auto. + intros z H. rewrite <- (mma_mm2_mma_state z) in H. rewrite <- mma_mm2_step_equiv in H. revert H. apply sss_out_step_stall with (1 := H2). Qed.
imports: List Arith Relations Lia Undecidability.Synthetic.Definitions Undecidability.Shared.Libs.DLW(utils pos vec sss subcode) Undecidability.MinskyMachines(MM2 mma_defs)