Added some code for term elimination (used for case splits)

The module Assertion_table can recognize elimination rules. It stores them and
returns the with the function 'consequences'. In the prover context we can
store elimination rules and a set of eliminated terms to avoid eliminating the
same term over and over.

However the prover does not yet insert elimination terms. Some complexity
problems have to be thought through before.

E.g. if we have the term '(a or b) or c' in the context we get because of the
commutativity of 'or' the term 'c or (a or b)' into the context as well. Both
are elimination terms i.e. for any target we can introduce the two elimination
rules into the context

    (a or b) or c => (a or b => t) => (c => t) => c
    c or (a or b) => (c => t) => (a or b => t) => c

If one of the succeeds then both succeed and if one of the fails both
fail. Therefore in the case of failure the prover would try both options.

With associativity the problem gets worse. Putting '(a or b) or c' into the
context we get the following closure

    (a or b) or c
    c or (a or b)
    a or (b or c)
    (b or c) or a

With equational resoning we could also use subterm commutativity and get
therefore 8 elimination terms into the context. This means in case of failure
we explore 8 routes which are practically equivalent. This combinatorial
explosion has to be avoided.

	modified:   ocaml/assertion_table.ml
	modified:   ocaml/assertion_table.mli
	modified:   ocaml/prover.ml
	modified:   ocaml/term.ml
Restriction of backward reasoning

Consider the following situation

    ..., a=>b=>c                 |- b=>c

In the current implementation two alternatives can be explored

    a) ..., a=>b=>c              |- a

    b) ..., a=>b=>c, b           |- c
       ..., a=>b=>c, b           |- a, b

Both alternatives are equivalent. In the first alternative we have to prove 'a'
under the assumptions '...,a=>b=>c' and in the second we have to prove 'a' and
'b' under the assumptions '...,a=>b=>c,b'. Either both succeed or both fail.

Therefore I have cut off the first alternative from the algorithm. In case of
success the performance is the same. In case of failure the performance is
increased significantly (if there are some of these possibilities).

	modified:   ocaml/prover.ml
Removed redundancies in the backward set

Assume then the prover has the following terms in the context

   a => b => c
   b => a => c

Then the backward set of 'c' consists of {[a,b], [b,a]}. Both alternatives are
equivalent. Either they both succeed or fail to prove 'c'. Therefore only one
of them is added to the backward set of 'c'. This has been done to reduce the
paths to explore if the prover has to prove 'c'.

	modified:   ocaml/prover.ml
Removed the unneeded 'globals'

	modified:   ocaml/prover.ml
Optimized entering

Whenever the goal is an implication chain of the form

    a => b => ... => c

the prover just checks if it can prove the assertion directly (without
backward reasoning) and enters recursively until the goal is 'c' (or one of
the previous direct proofs succeeded). Then it tries to prove 'c' by backward
reasoning. This improved algorithm cuts off some backward reasonings and
therefore improves the performance.

The theoretical basis for this improvement.

    (C |- a => b)  = (C,a |- b)

i.e. if we want to prove 'a=>b' in the context 'C' then we can prove 'b' in
the context 'C' augmented by 'a' as well (and vice versa).

	modified:   ocaml/prover.ml
Missing trace added

	modified:   ocaml/prover.ml
Fix: Original backward loop breaker fixed

Both loop breaker (the original base on the tried map and the database
approach with the attempt map) are still in the code. Currently the original
one is actived. It has the advantage that it is simpler.

The attempt_map not only detects but also detects if the same goal has already
failed or succeeded earlier. Therefore it generates less goals.

The question remains which of the loop breaker is more efficient from the
globlal perspective. It is a trade off between the number of goals generated
and the effort to maintain the attempt map.

	modified:   ocaml/prover.ml