proposition: Fact ra_compiler_succ : ra_compiler_stm ra_succ.
proof: Proof. red; simpl; intros i p o m H1 H2 H3. exists (mm_copy p o m (m+1) i ++ INC o :: nil); intros v e H4 H5; split. 2: exists (S (vec_head v)); cbv; auto. intros x; revert H5; vec split v with a; vec nil v; clear v. intros H5 H; simpl in H; subst x. specialize (H5 pos0); rewrite pos2nat_fst in H5; simpl in H5. destruct mm_copy_progress with (src := p) (dst := o) (tmp := m) (zero := m+1) (i := i) (e := e) as (e' & H7 & H8); try lia; try (apply H4; lia). exists (e'⦃o⇠S a⦄); split. * intros j; dest j o; rewrite H7; rew env. * rew length. apply sss_compute_trans with (9+i, e'). - apply sss_progress_compute. revert H8; apply subcode_sss_progress; auto. - mm env INC with o. mm env stop. rewrite H7, H5; rew env. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils finite pos vec subcode sss) Undecidability.MinskyMachines(env mme_defs mme_utils) Undecidability.MuRec.Util(recalg)