% praenex bereinigt zuerst die Formel F zu einer Formel X.
% Die bereinigte Formel X wird Durch ein dreistelliges
% Praedikat praenex so umgewandelt, dass in Y der Anfang
% der Formel aus Quantoren und in Z der quantorfreie Teil
% stehen. Das Praedikat join verbindet diese beiden Teile
% wieder zu einer normalen Formel.

praenex(F,G) :-
	normalize(F,X),
	praenex(X,Y,Z),
	join(Y,Z,G).
        
%
%
% HIER KOENNTE IHR CODE STEHEN
%
%

% Das Praedikat join verbindet ein Formelanfangsstueck,
% welches nur aus forall und exists besteht, mit einer
% zweiten Formel.

join(hole,Y,Y).
join(forall(V,X),Y,forall(V,Z)) :- join(X,Y,Z).
join(exists(V,X),Y,exists(V,Z)) :- join(X,Y,Z).

% Das 2-stellige Praedikat normalize bereinigt eine Formel
% in dem freie Variablen und Mehrfachvorkommen von Variablen
% auseinanderbenannt werden.

normalize(X, Y) :- normalize(X, 0, [], Y, _, _).

normalize(implies(X1,X2), M, T, Y, N, U) :- normalize(or(not(X1), X2), M, T, Y, N, U).
normalize(predicate(X,L), M, T, predicate(X,K), N, U) :- normalize(L, M, T, K, N, U).
normalize([], M, T, [], M, T).
normalize([X|L], M, T, [Y|K], N, U) :-
	normalize(X, M, T, Y, N1, U1),
	normalize(L, N1, U1, K, N, U).
normalize(var(X), M, T, var(Y), N, U) :- lookup(X, M, T, Y, N, U).
normalize(function(X,L), M, T, function(X,K), N, U) :- normalize(L, M, T, K, N, U).
normalize(not(X), M, T, not(Y), N, U) :- normalize(X, M, T, Y, N, U).
normalize(and(X1,X2), M, T, and(Y1, Y2), N, U) :-
	normalize(X1, M, T, Y1, O, S),
	normalize(X2, O, S, Y2, N, U).
normalize(or(X1,X2), M, T, or(Y1, Y2), N, U) :-
	normalize(X1, M, T, Y1, O, S),
	normalize(X2, O, S, Y2, N, U).
normalize(exists(V,X), M, T, exists(W,Y), N, U) :-
	remove(V, T, Q, R),
	lookup(V, M, Q, W, O, S),
	normalize(X, O, S, Y, N, P),
	add(R, P, U).
normalize(forall(V,X), M, T, forall(W,Y), N, U) :-
	remove(V, T, Q, R),
	lookup(V, M, Q, W, O, S),
	normalize(X, O, S, Y, N, P),
	add(R, P, U).

lookup(X, M, [], M, s(M), [m(X,M)]).
lookup(X, M, [m(X, N)|R], N, M, [m(X,N)|R]).
lookup(X, M, [m(Y, N)|R], Z, O, [m(Y,N)|S]) :-
	unequal(X, Y),
        lookup(X, M, R, Z, O, S).

unequal(0,s(_)).
unequal(s(_),0).
unequal(s(X),s(Y)) :- unequal(X,Y).

remove(X, [], [], none(X)).
remove(X, [m(X,M)|R], R, m(X,M)).
remove(X, [m(Y,M)|R], [m(Y,M)|S], Z) :- unequal(X,Y), remove(X, R, S, Z).

add(none(X), T, U) :- remove(X, T, U, _).
add(m(X,M), [m(X,_)|T], [m(X,M)|T]).
add(m(X,M), [m(Y,N)|T], [m(Y,N)|U]) :- unequal(X,Y), add(m(X,M), T, U).