Prove:

      (~~=>~) ,

under the assumptions:

      (~:<=,<=) ,

      (<=,<= =><=) .

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

      (6) .

The formula (4) is expanded by the definition (~:<=,<=,) into:

      (7) .

The conjunction (7) splits into (8) , (9).

The formula (5) is expanded by the definition (~:<=,<=,) into:

      (10) .

The conjunction (10) splits into (11) , (12).

We prove the individual conjunctive parts of (6):

Proof of (13) :

Because the formula (<=,<=,=> <=,) matches the goal (13) , we specialize it to:

      (15) .

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

      (16) .

For proving (16) it is sufficient to prove:

      (17) .

We prove the individual conjunctive parts of (17):

Proof of (18) :

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

Proof of (19) :

Formula (19) is true because it is identical to (11).

Proof of (14) :

Because the formula (<=,<=,=> <=,) matches the goal (14) , we specialize it to:

      (20) .

For proving (14) , by (20) , it suffices to prove

      (21) .

For proving (21) it is sufficient to prove:

      (22) .

We prove the individual conjunctive parts of (22):

Proof of (23) :

Formula (23) is true because it is identical to (12).

Proof of (24) :

Formula (24) is true because it is identical to (9).

---

Converted by Mathematica      February 10, 2000