Prove:

      (l2+) ,

under the assumptions:

      (l2:) ,

      (l3+) .

For proving (l2+) 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) , (5).

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

      (6) .

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

      (7) .

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

      (8) .

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

      (9) .

For proving (9) , by (l3+) , it suffices to prove

      (11) .

We prove the individual conjunctive parts of (11):

Proof of (12) :

Formula (12) is proved because it is an instance of (7).

Proof of (13) :

Formula (13) is proved because it is an instance of (8).

---

Converted by Mathematica      February 10, 2000