Sorry, I was incorrect when I said that Idris/Agra produce false negatives, I should have said that given a statement, the result can be undecidable whether it is valid or not.

Yes, the proof process taking too long is what I was getting at. So, you're talking about restricting the input so that the constructed statement considering the prior state and intput should be able to be determined valid or not within a reasonable period of time, correct?  

I'm trying to understand why restricting the possible input so nodes are able to process them all is better than just allowing the nodes to just reject inputs that can't be processed in a reasonable  time period (or in the case of undecidable languages causes the statement to be undecidable). My guess is that each individual node has their own internal state, which means that a scenario could exist where some nodes view an input as valid, others view it as undecidable, (or undecidable given a reasonable amount of processing time), and if that statement was part of a tau block chain it would cause a fork, which wouldn't be easy to reconcile. Is this the reason, or is it something else?

So then you are attempting to build tau with the following properties:

1. Uses a consistent, decidable logic
2. Has input restrictions that prevent a statement that is too complex from being accepted.
3. Has a prover that can take a statement derived by any input that passes the restriction in 2 and any internal state, and test for validity in a reasonable period of time.

Is this correct?

If so, then I'm curious about 3. Is it possible to prove that a prover can do this? If not, won't it be possible for Tau one day to be vulnerable to inputs that pass its restrictions but when combined with the internal state of a node still cause the prover to take too long?