Tableaux: definition Induction step if T is a finite tableau, P a path on t, e and entry of T occurring on P TI is obtained from T by adjoining an atomic tableau with root entry e to t at the end of the path P, then Tl is also a tableau o Here the requirement that c be new in Case 7b and Ba means that it is one of the ci that do not appear in any entries on P o In actual practice it is simpler in terms of bookkeeping to choose one not appearing at any nod ot tTableaux: definition Induction step: if τ is a finite tableau, P a path on τ , E and entry of τ occurring on P. τ ′ is obtained from τ by adjoining an atomic tableau with root entry E to τ at the end of the path P, then τ ′ is also a tableau. Here the requirement that c be new in Case 7b and 8a means that it is one of the ci that do not appear in any entries on P. In actual practice it is simpler in terms of bookkeeping to choose one not appearing at any nod of τ . Yi Li (Fudan University) Discrete Mathematics June 5, 2012 10 / 25