% RA: grupos.in
% Formalización de la estructura de grupo y grupo conmutativo
% Departamento de Ciencias de la Computación e Inteligencia Artificial
% Universidad de Sevilla
%==============================================================================


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

op(400, xfy, *).
op(300, yf, ^).

set(auto2).

formula_list(sos).
 all x (e * x = x).                       % Ax. 1
 all x (x * e = x).                       % Ax. 2
 all x (x^ * x = e).                      % Ax. 3
 all x (x * x^ = e).                      % Ax. 4
 all x y z ((x * y) * z = x * (y * z)).   % Ax. 5
 all x (x = x).                           % Ax. 6

 all x (x * x = e).                       % Hip.

 b * a != a * b.                          % Conc.
end_of_list.

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