%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Situation Formalization of the Elementary-MCP				%
%									%
%	Written by Eyal Amir						%
%	1/24/96								%
%									%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%




situation1  % [ parameters ]
		: THEORY

  BEGIN

  % ASSUMING
   % assuming declarations
  % ENDASSUMING


%%%%%%%%%%%%%%%%%%%%%%% Declarations, etc. %%%%%%%%%%%%%%%%%%%%%%%%%%

Person : TYPE = {M,C} %Missionary, Cannibal


p, t1, t2 : VAR Person

Bank:	TYPE = { Rb,Lb } %RightBank, LeftBank

Action : TYPE

Situation: TYPE

s : VAR Situation
s0: Situation

a : VAR Action

bank: VAR Bank



Cross_bridge : [ Person -> Action ]

result :	[Action, Situation -> Situation]

location :	[Person, Situation -> Bank]

opposite(bank): Bank = (IF bank = Lb THEN Rb
			ELSE Lb
			ENDIF)


%%%%%%%%%%%%%%%%%%%%%%%% Axioms %%%%%%%%%%%%%%%%%%%%%%%%%%

Axiom1:	AXIOM	Forall s, p:	location(p, result(Cross_bridge(p), s)) = 
					opposite(location(p,s))

% Frame Axiom

Axiom2: AXIOM	Forall s, p, a:	a /= Cross_bridge(p) IMPLIES
				location(p, result(a, s)) = location(p,s)

%Initial Situation

Axiom3: AXIOM	location(M,s0) = Lb AND location(C,s0) = Lb




% DNA (Distinct Names Assumption):

DNA1: AXIOM	C /= M
DNA2: AXIOM	Rb /= Lb



% Distinct Action Assumption (for the inertia formalization)

DAA: AXIOM	t1 /= t2 IMPLIES Cross_bridge(t1)/=Cross_bridge(t2)




% Final Lemma

Lemma1: LEMMA forall s: s = result(Cross_bridge(M),result(Cross_bridge(C), s0))
			IMPLIES location(M,s) = Rb AND location(C,s) = Rb


 





END situation1