Prove:

        (==>)    ,

under the assumption:

        ((-):)    .

We prove (==>) by the deduction rule.

We assume

        (1)    

and show

        (2)    .

For proving (2), by the definition ((-):), it suffices to prove:

        (3)    .

The formula (1) is expanded by the definition ((-):) into:

        (4)    .

We prove (3) by proving the first alternative negating the other(s).

We assume

        (6)    .

We now show

        (5)    .

Formula (6) is simplified to

        (7)    .

We prove the individual conjunctive parts of (5):

Proof of (8) :

We prove (8) by case distinction using (7).

Case  (10) :

Formula (10) is simplified to

        (12)    .

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

Case  (11) :

The formula (11) is expanded by the definition ((-):) into:

        (13)    .

Formula (13) is simplified to

        (14)    .

The conjunction (14) splits into (15) and (16).

Formula (15) is simplified to

        (17)    .

Formula (16) is simplified to

        (18)    .

We prove (8) by case distinction using (17).

Case  (19) :

From (19) and (18) we obtain by resolution

        (21)    .

We prove (8) by case distinction using (4).

Case  (22) :

The conjunction (22) splits into (24) and (25).

We delete (25) because it is identical to (21).

The formula (24) is expanded by the definition ((-):) into:

        (26)    .

We prove (8) by case distinction using (26).

Case  (27) :

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

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

Case  (28) :

The conjunction (28) splits into (31) and (32).

Formula (8) is proved because (19) and (32) are contradictory.

Case  (23) :

The conjunction (23) splits into (33) and (34).

Formula (8) is proved because (21) and (34) are contradictory.

Case  (20) :

Formula (20) is simplified to

        (35)    .

From (35) and (18) we obtain by resolution

        (36)    .

Formula (36) is simplified to

        (37)    .

We prove (8) by case distinction using (4).

Case  (38) :

The conjunction (38) splits into (40) and (41).

Formula (8) is proved because (35) and (41) are contradictory.

Case  (39) :

The conjunction (39) splits into (42) and (43).

We delete (43) because it is identical to (35).

The formula (42) is expanded by the definition ((-):) into:

        (44)    .

Formula (44) is simplified to

        (45)    .

The conjunction (45) splits into (46) and (47).

Formula (46) is simplified to

        (48)    .

Formula (47) is simplified to

        (49)    .

From (37) and (49) we obtain by resolution

        (50)    .

Formula (50) is simplified to

        (51)    .

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

Proof of (9) :

We prove (9) by contradiction.

We assume

        (52)    ,

and show

From (52) and (7) we obtain by resolution

        (53)    .

Formula (53) is simplified to

        (54)    .

The formula (52) is expanded by the definition ((-):) into:

        (55)    .

We prove (a contradiction) by case distinction using (55).

Case  (56) :

The conjunction (56) splits into (58) and (59).

We prove (a contradiction) by case distinction using (4).

Case  (60) :

The conjunction (60) splits into (62) and (63).

We delete (63) because it is identical to (59).

The formula (62) is expanded by the definition ((-):) into:

        (64)    .

We prove (a contradiction) by case distinction using (64).

Case  (65) :

The conjunction (65) splits into (67) and (68).

Formula (a contradiction) is proved because (58) and (68) are contradictory.

Case  (66) :

The conjunction (66) splits into (69) and (70).

Formula (a contradiction) is proved because (54) and (69) are contradictory.

Case  (61) :

The conjunction (61) splits into (71) and (72).

Formula (a contradiction) is proved because (59) and (72) are contradictory.

Case  (57) :

The conjunction (57) splits into (73) and (74).

We prove (a contradiction) by case distinction using (4).

Case  (75) :

The conjunction (75) splits into (77) and (78).

Formula (a contradiction) is proved because (74) and (78) are contradictory.

Case  (76) :

The conjunction (76) splits into (79) and (80).

We delete (80) because it is identical to (74).

The formula (79) is expanded by the definition ((-):) into:

        (81)    .

Formula (81) is simplified to

        (82)    .

The conjunction (82) splits into (83) and (84).

Formula (83) is simplified to

        (85)    .

Formula (84) is simplified to

        (86)    .

We delete (86) because it is subsumed by (73).

From (73) and (85) we obtain by resolution

        (87)    .

Formula (a contradiction) is proved because (54) and (87) are contradictory.

---

Converted by Mathematica      February 10, 2000