\[\renewcommand\arraystretch{1.3}
  \begin{array}[t]{rc|ll}
  \multicolumn2{l|}{\hbox{Boolean formula $f$}} &&
  \hbox{Representing OBDD $B_f$} \\\hline
  0           &&& B_0\hbox{ (Fig.~\ref{fig:bdd03})} \\
  1           &&& B_1\hbox{ (Fig.~\ref{fig:bdd03})} \\
  x           &&& B_x\hbox{ (Fig.~\ref{fig:bdd03})} \\
  \bar f      &&& \hbox{swap the $0$- and $1$-nodes in }B_f  \\
  f+g         &&& \apply\;(+,B_f,B_g) \\
  f\cdot g    &&& \apply\;(\cdot\,,B_f,B_g) \\
  f\oplus g   &&& \apply\;(\oplus,B_f,B_g) \\
  f[1/x]      &&& \restrict\;(1,x,B_f) \\ \qquad
  f[0/x]      &&& \restrict\;(0,x,B_f) \\
  \exists x.f &&& \apply\;(+,B_{f[0/x]},B_{f[1/x]}) \\
  \forall x.f &&& \apply\;(\cdot\,,B_{f[0/x]},B_{f[1/x]}) \\
  \end{array}\]