I see; thanks for clarifying. I suppose the only thing you’d get “for free” is that the termination of these programs becomes decidable. (Not sure if this is kn

I see; thanks for clarifying. I suppose the only thing you’d get “for free” is that the termination of these programs becomes decidable. (Not sure if this is known for these specific programs. At some point, BB number bounds are necessarily unknowable.)