proposition: Fact ra_compiler_zero : ra_compiler_stm ra_zero.
proof: Proof. red; simpl; intros i p o m H1 H2 H3. exists (mm_set o m 0 i); intros v e H4 H5; split. 2: exists 0; cbv; auto. intros x; revert H5. vec split v with a; vec nil v; clear v. intros H5 E; cbv in E; subst x. rewrite mm_set_length. destruct mm_set_progress with (dst := o) (zero := m) (n := 0) (i := i) (e := e) as (e' & G1 & G2); auto; try lia. exists e'; split; 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)