class  % [ parameters ]
		: THEORY
  BEGIN
  % ASSUMING
   % assuming declarations
  % ENDASSUMING


% First some propositional reasoning

a: bool
b: bool
a1,b1,a2,b2: VAR bool

% The difference between variables and constants

claim1 : CLAIM a implies (a or b)

claim2: CLAIM (a or b) implies (b or a)

% this is second order reasoning, albeit propositional

claim3: CLAIM   forall a1,b1: (a1 or b1) implies (b1 or a1)


% First order reasoning

object : TYPE 
x,x1,x2: VAR object
X0 : object
P(x1,x2) :bool


claim4: CLAIM forall x,x1: (P(x,x1) implies exists x2: P(x,x2))


axiom1 : AXIOM forall x,x1: P(x,x1) implies P(x1,x)

axiom2 : AXIOM forall x: P(x,X0)

claim5 : CLAIM forall x: P(X0,x)



end class