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) :

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

        (10)    .

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

We assume

        (12)    .

We now show

        (11)    .

Formula (12) is simplified to

        (13)    .

We prove the individual conjunctive parts of (11):

Proof of (14) :

We prove (14) by case distinction using (13).

Case  (16) :

Formula (16) is simplified to

        (18)    .

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

Case  (17) :

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

Case  (19) :

Formula (19) is simplified to

        (21)    .

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

        (22)    .

We prove (14) by case distinction using (22).

Case  (23) :

The conjunction (23) splits into (25) and (26).

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

Case  (24) :

The conjunction (24) splits into (27) and (28).

Formula (14) is proved because (17) and (28) are contradictory.

Case  (20) :

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

Case  (29) :

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

Formula (14) is true because it is identical to (31).

Case  (30) :

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

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

        (35)    .

We prove (14) by case distinction using (35).

Case  (36) :

The conjunction (36) splits into (38) and (39).

Formula (14) is proved because (17) and (38) are contradictory.

Case  (37) :

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

Formula (14) is proved because (20) and (41) are contradictory.

Proof of (15) :

We prove (15) by contradiction.

We assume

        (42)    ,

and show

From (42) and (13) we obtain by resolution

        (43)    .

Formula (43) is simplified to

        (44)    .

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

Case  (45) :

Formula (45) is simplified to

        (47)    .

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

        (48)    .

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

Case  (49) :

The conjunction (49) splits into (51) and (52).

Formula (a contradiction) is proved because (42) and (52) are contradictory.

Case  (50) :

The conjunction (50) splits into (53) and (54).

Formula (a contradiction) is proved because (44) and (53) are contradictory.

Case  (46) :

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

Case  (55) :

The conjunction (55) splits into (57) and (58).

We delete (57) because it is identical to (44).

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

        (59)    .

Formula (59) is simplified to

        (60)    .

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

Formula (61) is simplified to

        (63)    .

Formula (62) is simplified to

        (64)    .

We delete (64) because it is subsumed by (46).

From (42) and (63) we obtain by resolution

        (65)    .

Formula (a contradiction) is proved because (46) and (65) are contradictory.

Case  (56) :

The conjunction (56) splits into (66) and (67).

Formula (a contradiction) is proved because (44) and (66) are contradictory.

Proof of (9) :

We prove (9) by contradiction.

We assume

        (68)    ,

and show

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

        (69)    .

Formula (69) is simplified to

        (70)    .

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

        (71)    .

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

Case  (72) :

The conjunction (72) splits into (74) and (75).

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

Case  (76) :

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

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

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

        (80)    .

Formula (80) is simplified to

        (81)    .

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

Formula (82) is simplified to

        (84)    .

We delete (84) because it is subsumed by (75).

Formula (83) is simplified to

        (85)    .

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

        (86)    .

Formula (a contradiction) is proved because (75) and (86) are contradictory.

Case  (77) :

The conjunction (77) splits into (87) and (88).

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

Case  (73) :

The conjunction (73) splits into (89) and (90).

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

Case  (91) :

The conjunction (91) splits into (93) and (94).

Formula (a contradiction) is proved because (89) and (93) are contradictory.

Case  (92) :

The conjunction (92) splits into (95) and (96).

We delete (95) because it is identical to (89).

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

        (97)    .

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

Case  (98) :

The conjunction (98) splits into (100) and (101).

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

Case  (99) :

The conjunction (99) splits into (102) and (103).

Formula (a contradiction) is proved because (90) and (102) are contradictory.

---

Converted by Mathematica      February 10, 2000