There is a small typo in the above:

Undecidable ≡ Halt<ExpressionFromString<Natural>>[⦅RunOne.[]⦆] is

inferentially undecidable in the theory Actors, that is,

⊬Undecidable and ⊬¬Undecidable where

RunOne.[]≡Eval.[SelectOne.[0]] and ⦅RunOne.[]⦆ is the

expression for the procedure application RunOne.[]