proposition: Theorem ra_mm_simulator n (f : recalg n) : { m & { P : list (mm_instr (pos (n+S m))) | forall v, ex (⟦f⟧ v) <-> (1,P) // (1,vec_app v vec_zero) ↓ } }.
proof: Proof. destruct (ra_mm_compiler f) as (m & P & H1 & H2). exists m, P; split. + intros (x & Hx). exists (1+length P,vec_app v (x##vec_zero)); split; auto. simpl; lia. + intros H; apply H2; eq goal H; do 2 f_equal. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils_tac utils_nat pos vec sss) Undecidability.MinskyMachines(mm_defs) Undecidability.MuRec.Util(recalg ra_mm)