we should still maintain order (like today), so 5,4 can’t be played after 6.
I think that’s what you meant by “max”, but it’s not instead, it’s in addition to the last nonces.
In other words, the suggestion is to add a predicate to today’s logic (which asserts that the executed nonces are monotonically increasing).
Only today it’s simply looking at a single number (i.e. T = 1). And with this we’ll have some history.
So the logic can be - accept only if transaction.nonce > min(LastNonces) and transaction.nonce is not in LastNonces.
Maybe another way to look at it is that each contract has T “available slots” to allow for transactions to execute, and while a transaction is not included, it’s “holding” a slot, and when included in a block (by some definition of finality), the slot is “freed”.