We prove:

under the assumptions:

For proving MouseOver we choose A, B, C, and x arbitrary but fixed and show

In order to prove MouseOver we assume

and then prove

We prove both directions of MouseOver.

⇒:

In order to prove MouseOver we assume

and then prove

New constants have been generated, but no instantiations could be carried out.

We expand definitions:

In order to prove MouseOver, using definition MouseOver, we now show

From MouseOver we know, by definition MouseOver,

From MouseOver we know, by definition MouseOver,

For proving MouseOver we prove the individual conjuncts.

Proof of MouseOver:

We need to prove

The goal MouseOver is identical to formula MouseOver in the knowledge base. Thus, this part of the proof is finished.

Proof of MouseOver:

We need to prove

No goal rewriting.

We augment the knowledge base:

From MouseOver, using MouseOver, we can deduce

No knowledge rewriting.

We expand definitions:

In order to prove MouseOver, using definition MouseOver, we now show

For proving MouseOver we prove the individual conjuncts.

Proof of MouseOver:

We need to prove

The goal MouseOver is identical to formula MouseOver in the knowledge base. Thus, this part of the proof is finished.

Proof of MouseOver:

We need to prove

The goal MouseOver is identical to formula MouseOver in the knowledge base. Thus, this part of the proof is finished.

⇐:

In order to prove MouseOver we assume

and then prove

New constants have been generated, but no instantiations could be carried out.

We expand definitions:

In order to prove MouseOver, using definition MouseOver, we now show

From MouseOver we know, by definition MouseOver,

From MouseOver we know, by definition MouseOver,

For proving MouseOver we prove the individual conjuncts.

Proof of MouseOver:

We need to prove

The goal MouseOver is identical to formula MouseOver in the knowledge base. Thus, this part of the proof is finished.

Proof of MouseOver:

We need to prove

No goal rewriting.

We augment the knowledge base:

From MouseOver, using MouseOver, we can deduce

No knowledge rewriting.

We prove MouseOver by contradiction, i.e. we assume

and derive a contradiction.

No goal rewriting.

No knowledge rewriting.

We expand definitions:

From MouseOver we know, by definition MouseOver,

This part of the proof is herewith finished, because MouseOver contradicts MouseOver.