% Meta-Interpretierer: beweise Anfragen
prove(true) :- !.
prove( (A,B) ) :- !, prove(A), prove(B).
prove(P) :- clause(P,Body), prove(Body).

% Meta-Interpretierer: beweise Anfragen und Beweislaenge berechnen
lprove(true,0) :- !.
lprove( (A,B) ,L) :- !, lprove(A,LA), lprove(B,LB), L is LA+LB.
lprove(P,L) :- clause(P,Body), lprove(Body,LB), L is LB+1.

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