fact: Definition ra_compiled n (f : recalg n) i p o m (P : list (mm_instr nat)) := forall v e, (forall i, m <= i -> e⇢i = 0) -> (forall q, e⇢(pos2nat q+p) = vec_pos v q) -> (forall x, ⟦f⟧ v x -> exists e', e' ⋈ e⦃o⇠x⦄ /\ (i,P) // (i,e) ->> (length P + i,e')) /\ ((i,P) // (i,e) ↓ -> exists x, ⟦f⟧ v x).
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)