% 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)));