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

% Meta-Interpretierer fuer Prolog: prove(G)  <=> ?- G.
prove(true) :- !.
prove( (A,B) ) :- !,
        prove(A),
        prove(B).
prove(A) :-
        clause(A,Body),
        prove(Body).

% Meta-Interpretierer fuer Prolog mit Beweislaengenberechnung:
% lprove(G,N)  <=> ?- G.  und N ist die Anzahl der Resolutionsschritte
lprove(true,0) :- !.
lprove( (A,B), N) :- !,
        lprove(A,N1),
        lprove(B,N2),
        N is N1+N2.
lprove(A,N) :-
        clause(A,Body),
        lprove(Body,N1),
        N is N1+1.

