proposition: Theorem ra_compiler n f : @ra_compiler_stm n f.
proof: Proof. induction f as [ c | | | n q | n k f g Hf Hg | | ]. + apply ra_compiler_cst. + apply ra_compiler_zero. + apply ra_compiler_succ. + apply ra_compiler_proj. + apply ra_compiler_comp; trivial. + intros i p o m ? ? ?; apply ra_compiler_rec; auto. + intros i p o m ? ? ?; apply ra_compiler_min; 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)