app([],L,L).
app([E|R],L,[E|RL]) :- app(R,L,RL).

% Simple meta-interpreter for Prolog:
prove(true) :- !.
prove( (G1,G2) ) :- !, prove(G1), prove(G2).
prove(L) :- clause(L,G), prove(G).

% A meta-interpreter for Prolog which also computes the proof length:
lprove(true,0) :- !.
lprove( (G1,G2), N) :- !, lprove(G1,N1), lprove(G2,N2), N is N1+N2.
lprove(L,N) :- clause(L,G), lprove(G,N1), N is N1+1.

% Simple meta-interpreter for Prolog with tracing.
tprove(true) :- !.
tprove( (G1,G2) ) :- !, tprove(G1), tprove(G2).
tprove(L) :- showcallfail(L), clause(L,G), tprove(G), showexitredo(L).

showcallfail(L) :- write('CALL: '), write(L), nl.
showcallfail(L) :- write('FAIL: '), write(L), nl, fail.

showexitredo(L) :- write('EXIT: '), write(L), nl.
showexitredo(L) :- write('REDO: '), write(L), nl, fail.

p(a).
p(b).
q(b).
s(X) :- p(X), q(X).