% From John Kalman
% 
%      (4) The input file %i4 below, which includes several
% illustrations of list processing using Otter.
%
%
%     A railroad DEF has two sidings DBA and FCA connected at A.
% It is understood that D, E are respectively to the left of E, F;
% D, B are respectively to the left of B, A; and A, C are respectively
% to the left of C, F.
% The portion of the rails at A which is common to the two sidings is
% long enough to permit a single wagon, like P or Q, to run in or out of it,
% but is too short to contain the whole of an engine, like R. Hence, if an
% engine turns up one siding, such as DBA, it must come back the same way.
% Initially, P is at B, Q is at C, and R is at E. The problem is to use
% the engine R to interchange the wagons P and Q.
% [W.W.R. Ball and H.S.M. Coxeter, Mathematical Recreations and Essays,
% Univ. of Toronto Press, 12th ed., 1974, page 116.]
 
set(hyper_res).
assign(stats_level,1).
assign(max_given,2000).

list(usable).

%     H(u,xA,xB,xC,xD,xE,xF), where u is a position and xA, xB, ... are lists,
% means that it is possible to attain the configuration where the engine is
% at position u and xA, xB, ... list the vehicles (engine, wagons) at positions
% A, B, ... .

%     In describing the allowable moves, we first consider the case where
% (u,v) is a pair of adjacent positions each distinct from A, v is to
% the right of u (thus  (u,v) is (C,F) or (D,B) or (D,E) or (E,F)), and
% the engine is at position u.

%     If (u,v) is such a pair of positions, K1(u,v,y,z,x1,x2,x3,x4) means
% that it is possible to attain the configuration where y and z list the
% vehicles at positions u and v, and x1, x2, x3, x4 list the vehicles at
% the remaining four positions.

%     The following clauses transform H-representations of attainable
% configurations to K1-representations:

-H(C,xA,xB,xC,xD,xE,xF) | K1(C,F,xC,xF,xA,xB,xD,xE).
-H(D,xA,xB,xC,xD,xE,xF) | K1(D,B,xD,xB,xA,xC,xE,xF).
-H(D,xA,xB,xC,xD,xE,xF) | K1(D,E,xD,xE,xA,xB,xC,xF).
-H(E,xA,xB,xC,xD,xE,xF) | K1(E,F,xE,xF,xA,xB,xC,xD).

%     Given a pair of adjacent positions (u,v) as above and an attainable
% configuration K1(u,v, ... ), the next three clauses describe all
% allowable moves in which the engine goes from position u to position v.

%     In these clauses, K2(u,v,y,z,x1,x2,x3,x4) means that, after the move,
% y and z are the lists of vehicles at position u and v; u, v, x1, x2, x3, x4
% are as before the move.

%     Move whole list at position u to position v (if [R] or [R,y0] or
% [R,y0,y00] was the list at position u, this is the only allowable
% move that takes R to position v):

-K1(u,v,y,z,x1,x2,x3,x4) | K2(u,v,[],app(y,z),x1,x2,x3,x4).

%     For [y0|y1] at position u, where R is a member of y1, move y1
% to position v (if [y0,R] or [y0,R,y00] was the list at position u,
% this is the only remaining allowable move that takes R to position v):

-K1(u,v,[y0|y1],z,x1,x2,x3,x4) | -$TRUE(member(R,y1))
                        | K2(u,v,[y0],app(y1,z),x1,x2,x3,x4).

%     For [y0,y00,R] at position u, move R to position v:

-K1(u,v,[y0,y00,R],[],x1,x2,x3,x4) |  K2(u,v,[y0,y00],[R],x1,x2,x3,x4).

%     The following clauses transform K2-representations of attainable
% configurations to H-representations:

-K2(C,F,xC,xF,xA,xB,xD,xE) | H(F,xA,xB,xC,xD,xE,xF).
-K2(D,B,xD,xB,xA,xC,xE,xF) | H(B,xA,xB,xC,xD,xE,xF).
-K2(D,E,xD,xE,xA,xB,xC,xF) | H(E,xA,xB,xC,xD,xE,xF).
-K2(E,F,xE,xF,xA,xB,xC,xD) | H(F,xA,xB,xC,xD,xE,xF).

%     The case where (u,v) is a pair of adjacent positions each distinct
% from A, v is to the left of u (thus (u,v) is (B,D) or (E,D) or (F,C) or
% (F,E)), and the engine is at position u, may be reduced to the previous case
% with the help of the 'reverse' function.

%     Clauses to transform H-representations to K1-representations:

-H(B,xA,xB,xC,xD,xE,xF) | K1(B,D,rev(xB),rev(xD),xA,xC,xE,xF).
-H(E,xA,xB,xC,xD,xE,xF) | K1(E,D,rev(xE),rev(xD),xA,xB,xC,xF).
-H(F,xA,xB,xC,xD,xE,xF) | K1(F,C,rev(xF),rev(xC),xA,xB,xD,xE).
-H(F,xA,xB,xC,xD,xE,xF) | K1(F,E,rev(xF),rev(xE),xA,xB,xC,xD).

%     Clauses to transform K2-representations to H-representations:

-K2(B,D,xB,xD,xA,xC,xE,xF) | H(D,xA,rev(xB),xC,rev(xD),xE,xF).
-K2(E,D,xE,xD,xA,xB,xC,xF) | H(D,xA,xB,xC,rev(xD),rev(xE),xF).
-K2(F,C,xF,xC,xA,xB,xD,xE) | H(C,xA,xB,rev(xC),xD,xE,rev(xF)).
-K2(F,E,xF,xE,xA,xB,xC,xD) | H(E,xA,xB,xC,xD,rev(xE),rev(xF)).

%     Allowable moves between the position B (containing R) and A.

-H(B,[],[R,u],xC,xD,xE,xF) | H(B,[u],[R],xC,xD,xE,xF).
-H(B,[],[R,u,v],xC,xD,xE,xF) | H(B,[v],[R,u],xC,xD,xE,xF).
-H(B,[],[u,R,v],xC,xD,xE,xF) | H(B,[v],[u,R],xC,xD,xE,xF).
-H(B,[u],xB,xC,xD,xE,xF) | H(B,[],app(xB,[u]),xC,xD,xE,xF).
  
%     Allowable moves between the position C (containing R) and A.

-H(C,[],xB,[y0|y1],xD,xE,xF) | -$TRUE(member(R,y1)) | H(C,[y0],xB,y1,xD,xE,xF).
-H(C,[y0],xB,y1,xD,xE,xF) | H(C,[],xB,[y0|y1],xD,xE,xF). 
  
end_of_list.

list(sos).
  H(E,[],[P],[Q],[],[R],[]).
end_of_list.

list(passive).
  -H(E,[],[Q],[P],[],[R],[]).
end_of_list. 

list(demodulators).
  (member(x,[]) = $F).
  (member(x,[u|v]) = $IF($ID(x,u),$T,member(x,v))).

  (rev(x) = rev2(x,[])).
  (rev2([],x) = x).
  (rev2([y1|y2],z) = rev2(y2,[y1|z])).

  (app([u|v],y) = [u|app(v,y)]).
  (app([],y) = y).
end_of_list.