proposition: Corollary ra_mm_env_simulator n (f : recalg n) : { P | forall v e, (forall p, e⇢(pos2nat p) = vec_pos v p) -> (forall j, n < j -> e⇢j = 0) -> (forall x, ⟦f⟧ v x -> exists e', e' ⋈ e⦃n⇠x⦄ /\ (1,P) // (1,e) ->> (1+length P,e')) /\ ((1,P) // (1,e) ↓ -> ex (⟦f⟧ v)) }.
proof: Proof. destruct (ra_compiler f) with (i := 1) (p := 0) (o := n) (m := S n) as (P & HP); try lia. exists P; intros v e H4 H5; split. + intros x H3. rewrite Nat.add_comm; apply HP with (v := v); auto. intros; rewrite Nat.add_comm; simpl; auto. + intros H3. apply (HP v e); auto. intros; rewrite Nat.add_comm; simpl; 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)