% 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;
% some functions
f: T->T;
g: (T,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) => q(x)) AND
(FORALL(x: T): q(x) => p0(x) OR q0(x)) AND
(FORALL(x: T): q0(x) => p0(f(x))) =>
(FORALL(x: T): p(x) => (EXISTS(y: T): p0(y)));
C: FORMULA
(FORALL(x: T): p(x) => (EXISTS(y: T): r(x, y))) AND
(FORALL(x, y: T): r(x,y) => q(g(x,y))) AND
(FORALL(x: T): NOT q(x)) =>
(FORALL(x: T): NOT p(x));