I noticed my post missed the point a bit... I was thinking about functions that check properties of bit sequences, not functions that check properties of predic

I noticed my post missed the point a bit... I was thinking about functions that check properties of bit sequences, not functions that check properties of predicates on bit sequences. I get how it works now, thanks. Wish I could edit/delete my old post :-/. Just to check my understanding: a terminating program that decides bit sequences will have - a maximum number of bit checks it will make regardless of input, and - a maximum bit index it will access regardless of input, and even - a maximum running time (measured however).