% generates proof directory "exercise1a"
newcontext "exercise1a";

% a type
T: TYPE;

% predicates
p:  T -> BOOLEAN;
q:  T -> BOOLEAN;
p0: T -> BOOLEAN;
q0: T -> BOOLEAN;
r: (T,T) -> BOOLEAN;

% a function
f: T->T;

% formulas to be proved

A: FORMULA
     (EXISTS(x: T): p(x)) AND
     (FORALL(x: T): p(x) => (EXISTS(y: T): r(x, y))) =>
       (EXISTS(x, y: T): r(x, y));

B: FORMULA
     (FORALL(x: T): p(x) OR q(x)) AND
     (FORALL(x: T): p(x) => p0(f(x))) AND
     (FORALL(x: T): q(x) => q0(f(x))) =>
       (FORALL(x: T): (EXISTS(y: T): p0(y) OR q0(y)));
 
C: FORMULA
    (FORALL(x: T): p(x) => q(f(x))) AND
    (FORALL(x: T): q(x) => (EXISTS(y: T): r(x, y))) AND
    (FORALL(x, y: T): NOT r(x, y)) => 
      (FORALL(x: T): NOT p(x));