proposition: Fact ra_compiler_rec : ra_compiler_spec (ra_rec f g) i p o m.
proof: Proof. Proof using Hf Hg H1 H2 H3. exists Q4; intros v e G2 G3; split. + intros x; simpl ra_rel; intros G1. destruct rec_Q4_progress with (3 := G1) (e := e) as (e' & G4 & G5 & G6); auto. exists e'; split. * intros j; dest j o. * apply sss_progress_compute; auto. + intros G1. apply rec_Q4_compute_rev with (e := e); 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)