Prove:

        (l3+)   ,

under the assumptions:

        (l3:)   ,

        (l4+)   .

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

        (1)   .

We prove (1) by the deduction rule.

We assume

        (2)   

and show

        (3)   .

The conjunction (2) splits into (4) and (5).

For proving (3), by the definition (l3:), it suffices to prove:

        (6)   .

The formula (4) is expanded by the definition (l3:) into:

        (7)   .

By (7) we can take appropriate values such that:

        (8)   .

The formula (5) is expanded by the definition (l3:) into:

        (9)   .

By (9) we can take appropriate values such that:

        (10)   .

Because the formula (l4+) matches the goal (6), we specialize it to:

        (11)   .

For proving (6), by (11), it suffices to prove

        (12)   .

Because (8) matches a part of (12), we can proceed in several ways.

Alternative proof 1: proved

For proving (12) it is sufficient to prove:

        (13)   .

Because (10) matches a part of (13), we can proceed in several ways.

Alternative proof 1: proved

For proving (13) it is sufficient to prove:

        (14)   .

We prove the individual conjunctive parts of (14):

Proof of (15) :

Formula (15) is true because it is identical to (8).

Proof of (16) :

Formula (16) is true because it is identical to (10).

Alternative proof 2: pending

Pending proof of (13).

Alternative proof 2: pending

Pending proof of (12).

---

Converted by Mathematica      February 10, 2000