Clean up CC-Lemmmas, especially ArrayLemmas

Lots of duplicated code removed.  WeakSubPaths are SubPaths.
The subpaths are now explicitly collected in an array of all paths.
The subpaths are ordered correctly.
The subpath annotation no longer remembers the literals (they are in
the clause anyway).
Cache produced smt terms.

This is necessary for proof production.
FIXME: I would rather like to have this in an extra hash table that is
given as parameter to toSMTTerm.  This way we would save a pointer for each
CCAppTerm.
Added ProofChecker and option proof-check-mode.
Bug fix for CC annotation patch

Let it compile with Java-1.5 again.
Checkstyle issues
Exponential grow in scope lists.

This improves run-time from quadratic to linear on average.
We grow by a factor of 2 and shrink by a factor of 2.
Shrinking is only done if the table is filled for less than
a quarter.
Checking for free variables faster.

Added a specialised procedure that checks for free variables, instead
of computing getFreeVars() for every sub term.
Fixed removal of unused fresh symbols.

The removal code did not correctly complement the set of used definitions
leading to left-over definition of fresh function symbols created as pre-
commands for some term commands.  Now, these declarations should be correctly
removed.
Merge branch 'master' into newddtermsimp
Fixes and feature additions for delta debugger.

The delta debugger now recurses on term simplifications whenever a subterm is
pulled upwards (e.g. when replacing an annotated term with its subterm).
Additionally a cache is used to limit the number of tests needed to reach the
minimum.  Caching strategy could still be improved.

Frontend changed to remove the now dead -f flag.  Added a -v flag to increase
verbosity.  See documentation in Minimizer.java.