#### 8.8 Some Properties Involving a Reduction to PITL with Finite
Time

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