% generates proof directory exercise0 newcontext "exercise0"; % a type T: TYPE; % constants and functions a: T; f: T->T; % predicates p: T -> BOOLEAN; q: T -> BOOLEAN; r: T -> BOOLEAN; s: (T,T) -> BOOLEAN; % formulas to be proved A: FORMULA (FORALL(x:T): p(x) => q(x)) AND (FORALL(x:T): NOT r(x) => NOT q(x)) => (FORALL(x:T): NOT p(x) OR r(x)); B: FORMULA (EXISTS(x:T): p(x)) AND (FORALL(x:T): p(x) => (EXISTS(y:T): s(x,y))) => (EXISTS(x:T,y:T): s(x,y)); C: FORMULA (FORALL(x:T): p(x) => q(x) OR (EXISTS(y:T): s(x,y))) AND (FORALL(x:T): NOT s(a,x)) => NOT q(a) => NOT p(a); D: FORMULA (FORALL(x:T): p(x) => q(x) OR r(x)) AND (FORALL(x:T): q(x) => s(x,f(x))) AND (FORALL(x:T): r(x) => (EXISTS(y:T): s(x,y))) => (FORALL(x:T): p(x) => (EXISTS(y:T): s(x,y))); % sum(m,n) = the sum of all values from m (inclusive) to m+n (exclusive) % e.g. sum(2,5) = 2+3+4+5+6 sum: (NAT, NAT) -> NAT; S1: AXIOM FORALL(m: NAT): sum(m,0)=0; S2: AXIOM FORALL(m,n: NAT): sum(m,n+1) = (m+n)+sum(m,n); M: FORMULA FORALL(m,n,o: NAT): sum(m,o+n)=sum(m,o)+sum(m+o,n);