Finished tableaux

There are two cases in which a tableau may be regarded as finished. It may be regarded as finished if all its branches have closed. (Indeed there is now nothing that can be added to it.) It may also be regarded as finished if every formula in an unclosed branch either (a) has been ticked (for one of the reasons given above), or (b) is a formula beginning """, and nothing new would result if one applied the "xj rule to it again, or (c) is a formula to which no rule may be applied. Here is a simple example:

However, whereas  propositional tableaux are bound to finish, some predicate tableaux can never be regarded as finished. Here is a simple example: