% generates proof directory "exercise1a"
newcontext "exercise1a";
% a type
T: TYPE;
% predicates
p: T -> BOOLEAN;
q: (T,T) -> BOOLEAN;
r: T -> BOOLEAN;
s: T -> BOOLEAN;
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): q(x, y))) =>
(EXISTS(x: T, y: T): q(x, y));
B: FORMULA
(FORALL(x: T): r(x) => p(x) OR s(x)) AND
(FORALL(x: T): s(x) => q(x,x)) =>
(FORALL(x:T): p(x) => q(x, f(x))) =>
(FORALL(x: T): r(x) => (EXISTS(y:T): q(x,y)));
C: FORMULA
(EXISTS(x: T): NOT r(x)) AND
(FORALL(x: T): p(x) OR r(x)) AND
(FORALL(x: T, y: T): q(x, y) => r(x) OR s(y)) AND
(FORALL(x:T): p(x) => q(x, f(x))) =>
(NOT (FORALL(y: T): NOT s(y)));