Prove:

        (l4+)   ,

under the assumptions:

        (l4:)   ,

        ((+):)   ,

        (|++|)   ,

        (max:)   .

For proving (l4+) 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 (l4:), it suffices to prove:

        (6)   .

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

        (7)   .

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

        (8)   .

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

        (9)   .

We prove (9) by the deduction rule.

We assume

        (10)   

and show

        (11)   .

Using ((+):), the goal (11) is transformed into:

        (12)   .

For proving (12), by (|++|), it suffices to prove

        (14)   .

We prove the individual conjunctive parts of (14):

Proof of (15) :

For proving (15), by (7), it suffices to prove

        (18)   .

From (10), by (max:), we obtain:

        (21)   .

The conjunction (21) splits into (22) and (23).

Formula (18) is true because it is identical to (22).

Proof of (16) :

For proving (16), by (8), it suffices to prove

        (25)   .

From (10), by (max:), we obtain:

        (28)   .

The conjunction (28) splits into (29) and (30).

Formula (25) is true because it is identical to (30).

---

Converted by Mathematica      February 10, 2000