% generates directory exercise0
newcontext "exercise0";

% a type
T: TYPE;

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

% a constant
c: T;

% formulas to be proved
A: FORMULA
  p(c) AND (FORALL(x:T): p(x) => r(x)) =>
    (EXISTS (x:T): r(x));

B: FORMULA
  (EXISTS(y:T): FORALL(x:T): q(x,y)) =>
    (FORALL(x:T): EXISTS(y:T): q(x,y));

C: FORMULA
  (EXISTS(x:T): p(x)) AND
    (FORALL(x:T): p(x) => (EXISTS(y:T): q(x,y))) =>
    (EXISTS(x, y:T): q(x,y));
 
D: FORMULA
  (EXISTS(x:T): p(x)) OR (EXISTS(x:T): r(x)) =>
    (EXISTS(x:T): p(x) OR r(x));

E: FORMULA
  (FORALL(x:T): r(x) => p(x)) AND (FORALL(x:T): s(x) => p(x)) AND 
    (FORALL(x:T): r(x) OR s(x)) =>
      (FORALL(x:T): p(x));

% the addition function recursively defined
add: (NAT,NAT) -> NAT;
A1: AXIOM FORALL(m: NAT): add(m, 0) = m;
AB: AXIOM FORALL(m, n: NAT): add(m, n+1) = 1+add(m, n);

% properties of addition
T1: FORMULA FORALL(m: NAT): add(0, m) = m;
T2: FORMULA FORALL(m, n: NAT): add(m+1, n) = add(m, n)+1;
T3: FORMULA FORALL(m, n: NAT): add(m, n) = add(n, m);