proposition: Fact ra_compiler_proj n q : ra_compiler_stm (@ra_proj n q).
proof: Proof. red; simpl; intros i p o m H1 H2 H3. exists (mm_copy (pos2nat q+p) o m (m+1) i); intros v e H4 H5; split. 2: exists (vec_pos v q); cbv; auto. intros x E; simpl in E; subst x. destruct mm_copy_progress with (src := pos2nat q+p) (dst := o) (tmp := m) (zero := m+1) (i := i) (e := e) as (e' & H7 & H8); try lia; try (apply H4; lia); try (generalize (pos2nat_prop q); lia). exists e'; split. * intros j; rewrite H7; dest j o. * rew length; apply sss_progress_compute; auto. 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)