Prove:

        (fg)    ,

under the assumptions:

        (d+)    ,

        (c+)    .

For proving (fg) we take all variables arbitrary but fixed and prove:

        (1)    .

Proving (1) by contradiction fails.

We assume

        (2)    ,

and show

The proof of (a contradiction) fails.(The PND was unable to transform the proof situation.)

---

Converted by Mathematica      February 11, 2000