\begin{definition}[Definition:Finished Branch of Propositional Tableau]
Let $T$ be a propositional tableau.
Let $\Gamma$ be a branch of $T$.
Then $\Gamma$ is '''finished''' {{iff}}:
:$(1): \quad \Gamma$ is not contradictory
:$(2): \quad$ Every non-basic WFF on $\Gamma$ is used at some node of $\Gamma$.
That is, $\Gamma$ is '''finished''' {{iff}} the set $\Delta$ of WFFs of propositional logic which occur along $\Gamma$ is a finished set.
\end{definition}