1: \begin{definition}

2:   Let the predicates $\nbinfcansymb$ and $\binfcansymb$ on

3:   $\olfsfix$ be defined by $\nbinfcansymb:=\nbinfpsymb P$ and

4:   $\binfcansymb:=\binfpsymb P$ for $P:=\exfinsymb\circ\solletter$,

5:   which satisfies the proviso by

6:   Theorem~\ref{thm:decide-fin-inhab}.\ref{thm:decide-fin-inhab.2}. In particular,

7:   $\nbinfcansymb$ and $\binfcansymb$ are decidable.

8: \end{definition}

9: