fof( z_s_disjointness, axiom, ![X] : z!=s(X) ).
fof( s_injectivity, axiom, ![X,Y] : (s(X)=s(Y) => X=Y) ).
fof( plus_z, axiom, ![X] : plus(X,z)=X ).
fof( plus_s, axiom, ![X,Y] : plus(X,s(Y))=s(plus(X,Y)) ).
fof( times_z, axiom, ![X] : times(X,z)=z ).
fof( times_s, axiom, ![X,Y] : times(X,s(Y))=plus(times(X,Y),X) ).
fof( sum_z, axiom, ![X] : sum(z)=z ).
fof( sum_s, axiom, ![X] : sum(s(X))=plus(s(X),sum(X)) ).

% an instance of induction scheme
fof( plusAssocP_def, axiom, ![X,Y,Z] : (
plusAssocP(X,Y,Z) <=> (plus(plus(X,Y),Z)=plus(X,plus(Y,Z)))
)).
fof( plusAssocP_ind, axiom, ![X,Y] : (
(plusAssocP(X,Y,z) & (![Z] : plusAssocP(X,Y,Z) => plusAssocP(X,Y,s(Z)))) =>
![Z] : plusAssocP(X,Y,Z)
)).

% an instance of induction scheme
fof( plusP1_def, axiom, ![X] : (
plusP1(X) <=> plus(z,X)=X
)).
fof( plusP1_ind, axiom,
(plusP1(z) & (![X] : plusP1(X) => plusP1(s(Y)))) =>
![X] : plusP1(X)
).

% an instance of induction scheme
fof( plusP2_def, axiom, ![X,Y] : (
plus(s(X),Y)=s(plus(X,Y))
)).
fof( plusP2_ind, axiom, ![X] : (
(plusP2(X,z) & (![Y] : plusP2(X,Y) => plusP2(X,s(Y)))) =>
![X] : plusP2(X,Y)
)).

% an instance of induction scheme
fof( plusCommP_def, axiom, ![X,Y] : (
plusCommP(X,Y) <=> plus(X,Y)=plus(Y,X)
)).
fof( plusCommP_ind, axiom, ![X] : (
(plusCommP(X,z) & (![Y] : plusCommP(X,Y) => plusCommP(X,s(Y)))) =>
![Y] : plusCommP(X,Y)
)).

% an instance of induction scheme
fof( distP_def, axiom, ![X,Y,Z] : (
distP(X,Y,Z) <=> times(plus(X,Y),Z)=plus(times(X,Z),times(Y,Z))
)).
fof( distP_ind, axiom, ![X,Y] : (
(distP(X,Y,z) & (![Z] : distP(X,Y,Z) => distP(X,Y,s(Z)))) =>
![Z] : distP(X,Y,Z)
)).

% an instance of induction scheme
fof( timesAssocP_def, axiom, ![X,Y,Z] : (
timesAssocP(X,Y,Z) <=> (times(times(X,Y),Z)=times(X,times(Y,Z)))
)).
fof( timesAssocP_ind, axiom, ![X,Y] : (
(timesAssocP(X,Y,z) & (![Z] : timesAssocP(X,Y,Z) => timesAssocP(X,Y,s(Z)))) =>
![Z] : timesAssocP(X,Y,Z)
)).

% an instance of induction scheme
fof( timesCommP_def, axiom, ![X,Y] : (
timesCommP(X,Y) <=> times(X,Y)=times(Y,X)
)).
fof( timesCommP_ind, axiom, ![X] : (
(timesCommP(X,z) & (![Y] : timesCommP(X,Y) => timesCommP(X,s(Y)))) =>
![Y] : timesCommP(X,Y)
)).

% an instance of induction scheme
fof( sumP_def, axiom, ![X] : (
sumP(X) <=> (times(sum(X),s(s(z))) = times(X,s(X)))
)).
fof( distP_ind, axiom, 
(sumP(z) & (![X] : sumP(X) => sumP(s(X)))) =>
![X] : sumP(X)
).

% fof( plus_assoc, conjecture, ![X,Y,Z] : plus(plus(X,Y),Z) = plus(X,plus(Y,Z)) ).
% fof( plus_comm, conjecture, ![X,Y] : plus(X,Y) = plus(Y,X) ).
% fof( times_assoc, conjecture, ![X,Y] : times(X,Y) = times(Y,X) ).
% fof( times_comm, conjecture, ![X,Y] : times(X,Y) = times(Y,X) ).
% fof( dist, conjecture, ![X,Y,Z] : times(plus(X,Y),Z) = plus(times(X,Z),times(Y,Z)) ).
fof( sum_eq, conjecture, ![X] : times(sum(X),s(s(z))) = times(X,s(X)) ).

% ~/src/e/PROVER/eprover.exe -l 2 --tptp3-format nat.tptp