proposition: Fact mma_mm2_step_equiv P s1 s2 : (1,P) /A/ s1 → s2 <-> map mma_mm2_instr P /2/ mma_mm2_state s1 → mma_mm2_state s2.
proof: Proof. split. + apply mma_mm2_step. + intros H; apply mm2_mma_step in H. rewrite map_map in H. do 2 rewrite mm2_mma_mm2_state in H. eq goal H; do 2 f_equal. rewrite <- (map_id P) at 2. apply map_ext, mm2_mma_mm2_instr. Qed.
imports: List Arith Relations Lia Undecidability.Synthetic.Definitions Undecidability.Shared.Libs.DLW(utils pos vec sss subcode) Undecidability.MinskyMachines(MM2 mma_defs)