We start with noting that the sets of all 1-types \({TP}_1\)  and of
all 2-types \({TP}_2\)  can be computed by enumerating all
candidates \(t \subseteq {cl}_i()\) , \(i \in \lbrace 1,2\rbrace \) , and then
checking whether \(t\)  is satisfiable w.r.t. . The latter can be
done in [1]}, which yields
an upper bound of \(2^{2^{O(||)}}\) , sufficient for our purposes.
However, it also seems clear that the standard type elimination
procedure for can be adapted to GF\(_2\)  in a straightforward
way, eliminating 1-types and 2-types simultaneously. This gives a
\(2^{O(||)}\)  upper bound.
