There is a small typo in the above: Undecidable ≡ Halt<ExpressionFromString<Natural>>[⦅RunOne.[]⦆] is inferentially undecidable in the theory Actors, that is,

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.[]