tuple  % [ parameters ]
		: THEORY

  BEGIN

  % ASSUMING
   % assuming declarations
  % ENDASSUMING

Z4 : TYPE = {x:nat | x < 4}
Z3 : TYPE = {x:nat | x < 3}

 Z2 : TYPE = {x:nat | x < 2}

m, c : VAR Z4

pair2 : TYPE = [Z3,Z3]
% a pair is the number of missionaries and cannibals that move


 moves : TYPE = { u:pair2 | proj_1(u) + proj_2(u) <=2 AND proj_1(u) + proj_2(u)>= 1}

% we say what the allowable mves are, the sum of the people moving must be
% less than 3 and at least one.


move : VAR moves

state : TYPE =  [Z4,Z4,Z2]

% the state is the number of missionaries, cannibals and boats on
% the left bank

s : VAR state

ok1(m,c) : bool = ( m = 0 OR m >= c)

% a bank is ok1 if the cannibals don't outnumber the missionaires.

ok(s): bool = ok1(proj_1(s),proj_2(s)) AND ok1(3 - proj_1(s), 3 - proj_2(s))

% we are ok if both banks are ok1.

result(move,s) : state = (if proj_1(s) - (( (2 * proj_3(s)) - 1) * proj_1(move)) < 4 and proj_1(s) - (( (2 * proj_3(s)) - 1) * proj_1(move)) >= 0 then proj_1(s) - (( (2 * proj_3(s)) - 1) * proj_1(move)) else proj_1(s) endif , if proj_2(s) - (( (2 * proj_3(s)) - 1) * proj_2(move)) < 4 AND proj_2(s) - (( (2 * proj_3(s)) - 1) * proj_2(move)) >= 0 then proj_2(s) - (( (2 * proj_3(s)) - 1) * proj_2(move)) else proj_2(s) endif , 1 - proj_3(s))

% this encodes the result of moving.

attainable(s) : bool

Lemma1: LEMMA result((0,2),result((0,1),result((0,2),result((0,1),result((2,0),result((1,1),result((2,0),result((0,1),result((0,2),result((0,1),result((0,2),(3,3,1)))))))))))) = (0,0,0)

Axiom1 : AXIOM  Forall s, move: attainable(s) AND ok(result(move,s)) => attainable(result(move,s))

Axiom2 : AXIOM attainable((3,3,1))

Claim1 : CLAIM attainable((0,0,0))



 





  END tuple