% Copyright (c) 2001  Andrew W. Appel.

% Assignment 6:
% Prove the following theorems from pages 166-167 of Huth & Ryan.


% This one is rather difficult.  Look at the proof of not_AE_not
% (in "classiclem.elf") for inspiration.
thm3_1a: pf (G |-  #not (#AF Q) #equiv #EG (#not Q)) = bighole.

% This one is easier than 3_1a.
thm3_1b: pf (G |- #not (#EF Q) #equiv #AG (#not Q)) = bighole.

% This proof is similar to thm3_1a
thm3_2: pf (G |- #not (#AX Q)  #equiv  #EX (#not Q)) = bighole.

thm3_3a: pf (G |- #A (B #U C)) ->
        pf (G |- #not (#E (#not C #U (#not B #and #not C)) #or #EG (#not C))) =
 [p1: pf (G |- #A (B #U C))] 
 cut p1 [_] bighole.

thm3_3b: pf (G |- #not (#E (#not C #U (#not B #and #not C)) #or #EG (#not C))) ->
pf (G |- #A (B #U C)) = 
  [p1] cut p1 [_] bighole.

thm3_3: pf (G |- #A (B #U C)  #equiv
                 #not (#E (#not C #U (#not B #and #not C)) #or #EG (#not C))) =
 #equiv_i2 thm3_3a thm3_3b.