proposition: Fact mm2_mma_terminates P s : P /2/ s ↓ -> (1,map mm2_mma_instr P) /A/ mm2_mma_state s ↓.
proof: Proof. intros (y & H1 & H2). exists (mm2_mma_state y); split. + apply mm2_mma_compute; auto. + destruct y as (i,(a,b)); simpl fst. red in H2. destruct (in_out_code_dec i (1, map mm2_mma_instr P)) as [ H3 | ] ; auto. destruct in_code_subcode with (1 := H3) as (rho & H4); exfalso; revert H4. rewrite <- (mm2_mma_mm2_instr rho). generalize (mma_mm2_instr rho); clear rho; intros rho. intros H4. destruct (mma_sss_total (mm2_mma_instr rho) (i,a##b##vec_nil)) as (w & Hw). apply mma_mm2_atom in Hw. apply (H2 (mma_mm2_state w)). rewrite mma_mm2_mma_instr in Hw. exists rho; split; auto; simpl. destruct H4 as (l & r & H4 & H5). exists (map mma_mm2_instr l), (map mma_mm2_instr r); split; rew length; try lia. apply f_equal with (f := map mma_mm2_instr) in H4. rewrite map_map, map_app in H4; simpl in H4. rewrite mma_mm2_mma_instr in H4. rewrite <- H4, <- (map_id P) at 1. apply map_ext; intros; rewrite mma_mm2_mma_instr; auto. Qed.
imports: List Arith Relations Lia Undecidability.Synthetic.Definitions Undecidability.Shared.Libs.DLW(utils pos vec sss subcode) Undecidability.MinskyMachines(MM2 mma_defs)