We now present some derived inference rules which come in useful when completeness for PITL with finite time is assumed. Recall that any valid implication of the form finite ⊃ f is allowed and that we designate such a step by using PITLF. PITL Theorem BfFinStateEqvBox below illustrates this technique.