:- dynamic append/3, loop/0, quickSort/2, quickSort_dl/3, splitLGE/4.

% zum Testen

append([],Ys,Ys).
append([X|Xs],Ys,[X|Zs]) :- append(Xs,Ys,Zs).

loop.
loop :- loop.

quickSort(L,S) :- quickSort_dl(L,S,[]).

quickSort_dl([],L,L).
quickSort_dl([E|R],M,N) :-
	splitLGE(E,R,L,GE),
	quickSort_dl(L,M,[E|GESorted]),
	quickSort_dl(GE,GESorted,N).

splitLGE(_,[],[],[]).
splitLGE(X,[Y|Ys],[Y|L],GE) :- Y < X, splitLGE(X,Ys,L,GE).
splitLGE(X,[Y|Ys],L,[Y|GE]) :- Y >= X, splitLGE(X,Ys,L,GE).

% einfacher Interpreter

prove(true) :- !.
prove((A,B)) :- !, prove(A), prove(B).
prove(A) :- clause(A,R), prove(R).

% beschränkter Interpreter

bounded(G,N) :- bounded(G,N,_).

bounded(G,N,K) :- N >= 0, bprove(G,N,K).

bprove(true,_,0) :- !.
bprove((A,B),N,K) :- !,
	bounded(A,N,K1), N2 is N - K1, bounded(B,N2,K2), K is K1 + K2.
bprove(A,N,K1) :- N1 is N-1, clause(A,R), bounded(R,N1,K), K1 is K + 1.

% Beweis berechnen

proof(G,P) :- proof(G,P,[]).

proof(true,P,P) :- !.
proof((A,B),P,R) :- !, proof(A,P,Q), proof(B,Q,R).
% für quickSort 
proof(<(X,Y),[<(X,Y)|P],P) :- !, X < Y.
proof(>=(X,Y),[>=(X,Y)|P],P) :- !, X >= Y.
proof(A,[:-(A,G)|P],Q) :- clause(A,G), proof(G,P,Q).

printProof(G) :- proof(G,P), printClauses(P).

printClauses([]).
printClauses([:-(A,true)|Cs]) :- !,
	write(A), write('.'), nl,
	printClauses(Cs).
printClauses([:-(A,B)|Cs]) :- !,
	write(A), tab(1), write(':-'), tab(1), write(B), write('.'), nl,
	printClauses(Cs).
printClauses([A|Cs]) :- 
	write(A), write('.'), nl,
	printClauses(Cs).