%%%
%%%    NAME/LOGIN-ID _____________________/______________________
%%%
%%%    ACKNOWLEDGMENTS:
%%%      * List the names of people whom you worked with or who helped you
%%%        with this assignment
%%%      * Cite any references you used to complete this work
%%%
%%%    ===================
%%%    Propositional Logic
%%%    ===================
%%%    
%%%    Prove these theorems using only the (SPLIT) and (FLATTEN) commands
%%%                               ~~~~

th_A: Theory

BEGIN

%%% Elementary propositions.
%%%

p,q,r: bool

%%% 
%%% Propositional Formulas
%%%
%%%   (CLAIM, CONJECTURE, ..., THEOREM all mean the same thing)
%%% 

A_0: CLAIM  ((p => q) AND p) => q

A_1: CONJECTURE  ((p AND q) AND r) => (p AND (q AND r))

A_2: COROLLARY  NOT (p OR q) IFF (NOT p AND NOT q)

A_3: FACT  NOT (p AND q) IFF (NOT p OR NOT q)

A_4: FORMULA  (p => (q => r)) IFF (p AND q => r)

A_5: LAW  (p AND (q OR r)) IFF (p AND q) OR (p AND r)

A_6: LEMMA  (p OR (q AND r)) IFF (p OR q) AND (p OR r)

A_7: PROPOSITION  ((p => q) AND (p => r)) IFF (p => (q AND r))

A_8: SUBLEMMA  ((p => q) => (p AND q)) IFF ((NOT p => q) AND (q => p))

A_9: THEOREM  ((p OR q) AND r) => (p AND (q AND r))

A_10: CLAIM p => (q => p)

A_11: CLAIM ((p => (q => r)) => ((p => q) => (p => r)))

A_12: CLAIM ((NOT q) => (NOT p)) => (((NOT q) => p) => q)

END th_A