THEORY exercises IS

     p or not(p);

     p => q or p;

     (p & p) <=> p;

     (p or p) <=> p;

     (p & q) <=> (q & p);

     (p & (q or p)) <=> p;

     ((p & q) or p) <=> p;

     (p & q => r) => (p => (q => r));

     ((p => q) & (p => r)) => (p => (q & r));

     (p => q) => (q <=> (p or q));

     (p => q) => (p <=> (p & q))

TAC

  (propX~;DED;HYP)~

END
&
THEORY propX IS

     (a => c) &
     (b => c)
    =>
     (a or b => c);

     (not(a) => b)
    =>
     (a or b);

     (a => b) &
     (b => a)
    =>
     a <=> b


END
