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





situation2  % [ parameters ]
                : THEORY

  BEGIN

  % ASSUMING
   % assuming declarations
  % ENDASSUMING


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

Person : TYPE = {M1,M2,C1,C2} %Missionaries, Cannibals


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(M1,s0) = Lb AND location(M2,s0) = Lb AND location(C1,s0) = Lb AND location(C2,s0) = Lb




% DNA (Distinct Names Assumption):

DNA1: AXIOM     C1 /= C2 
DNA2: AXIOM C1 /= M1 
DNA3: AXIOM C1 /= M2 
DNA4: AXIOM C2 /= M1 
DNA5: AXIOM C2 /= M2 
DNA6: AXIOM M1 /= M2  
DNA7: AXIOM     Rb /= Lb

DNA: AXIOM     C1 /= C2 and C1 /= M1 and C1 /= M2 and C2 /= M1 and
	C2 /= M2 and M1 /= M2  and 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(M2), result(cross_bridge(C2) ,result(cross_bridge(M1),result(cross_bridge(C1), s0))))
                        IMPLIES location(M2,s) = Rb AND location(C2,s) = Rb AND location(M1,s) = Rb AND location(C1,s) = Rb


 





END situation2