2is unabashedly intractable-given a sequence f , it involves consideration of an exponential (in |f |) number of tag sequences and an infinite number of lemmata sequences.
we will fall back on an approximation scheme (see §5).