% RA: 08-fichasAR.in
% Cambiar la posición de las fichas Azules y Rojas
% Departamento de Ciencias de la Computación e Inteligencia Artificial
% Universidad de Sevilla
%==============================================================================


%==============================================================================
% Enunciado
%==============================================================================

% En una fila de 7 huecos se disponen tres fichas azules y tres fichas rojas
% tal y como se indica en la figura. Una ficha se puede mover al hueco
% saltando, como mucho, por encima de otras dos fichas. Encontrar una forma de
% cambiar de posición las fichas rojas con las azules moviendo de manera
% alternativa unas y otras.
%
%                      ┏━━━┯━━━┯━━━┯━━━┯━━━┯━━━┯━━━┓
%                      ┃ A │ A │ A │   │ R │ R │ R ┃
%                      ┗━━━┷━━━┷━━━┷━━━┷━━━┷━━━┷━━━┛

% Utilizar Otter para encontrar una solución al problema.

%==============================================================================
% Formalización
%==============================================================================

% Configuración del sistema

set(para_into).
set(para_from).

% Lenguaje del problema

% Constantes:
%  a, r, h

% Funciones:
%  c(X) : La ficha de color contrario a X.

% Propiedades:
%  estado(L) :
%    L es una lista que representa una fila de 7 huecos que se puede alcanzar
%    con pasos del juego. Los elementos de L son a (ficha azul), r (ficha
%    roja) y h(X) (hueco), donde X es el color de la ficha a la que le toca
%    mover.

list(demodulators).
% Comportamiento de la función c.
  c(a) = r.
  c(r) = a.

% La función c es idempotente.
  c(c(x)) = x.
end_of_list.

list(usable).
% Saltos hacia la izquierda.
 [h(x),x|w] = [x,h(c(x))|w].
 [h(x),x1,x|w] = [x,x1,h(c(x))|w].
 [h(x),x1,x2,x|w] = [x,x1,x2,h(c(x))|w].

% Saltos hacia la derecha.
 [x,h(x)|w] = [h(c(x)),x|w].
 [x,x1,h(x)|w] = [h(c(x)),x1,x|w].
 [x,x1,x2,h(x)|w] = [h(c(x)),x1,x2,x|w].
end_of_list.

list(sos).
% Situación inicial, comienza el juego la ficha roja.
 estado([a,a,a,h(r),r,r,r]).

% Objetivo final.
 -estado([r,r,r,x,a,a,a]).
end_of_list.

%==============================================================================
% Soluciones:
%==============================================================================

% Se obtiene la siguiente prueba:

% ---------------- PROOF ----------------
%   1 [] c(a)=r.
%   2 [] c(r)=a.
%   4 [] [h(x),x|w]=[x,h(c(x))|w].
%   5 [] [h(x),x1,x|w]=[x,x1,h(c(x))|w].
%   6 [] [h(x),x1,x2,x|w]=[x,x1,x2,h(c(x))|w].
%   8 [] [x,x1,h(x)|w]=[h(c(x)),x1,x|w].
%   9 [] [x,x1,x2,h(x)|w]=[h(c(x)),x1,x2,x|w].
%  10 [] estado([a,a,a,h(r),r,r,r]).
%  11 [] -estado([r,r,r,x,a,a,a]).
%  16 [para_into,11.1.1.2.2.2,5.1.1,demod,1] -estado([r,r,r,a,a,h(r),a]).
%  25 [para_into,10.1.1.2.2.2,5.1.1,demod,2] estado([a,a,a,r,r,h(a),r]).
%  27 [para_into,16.1.1.2.2,9.1.1,demod,2] -estado([r,r,h(a),a,a,r,a]).
%  33 [para_into,25.1.1.2.2,9.1.1,demod,1] estado([a,a,h(r),r,r,a,r]).
%  36 [para_into,27.1.1.2.2,5.1.1,demod,1] -estado([r,r,a,a,h(r),r,a]).
%  47 [para_into,33.1.1.2.2,4.1.1,demod,2] estado([a,a,r,h(a),r,a,r]).
%  52 [para_into,36.1.1.2,9.1.1,demod,2] -estado([r,h(a),a,a,r,r,a]).
%  73 [para_into,47.1.1.2.2.2,5.1.1,demod,1] estado([a,a,r,a,r,h(r),r]).
%  84 [para_into,52.1.1.2,4.1.1,demod,1] -estado([r,a,h(r),a,r,r,a]).
% 107 [para_into,73.1.1.2.2.2.2.2,4.1.1,demod,2] estado([a,a,r,a,r,r,h(a)]).
% 127 [para_into,84.1.1,8.1.1,demod,2] -estado([h(a),a,r,a,r,r,a]).
% 167 [para_into,107.1.1.2.2.2,9.1.1,demod,1] estado([a,a,r,h(r),r,r,a]).
% 194 [para_into,127.1.1,6.1.1,demod,1] -estado([a,a,r,h(r),r,r,a]).
% 195 [binary,194.1,167.1] $F.
% ------------ end of proof -------------

%==============================================================================
