deq(nullq).
deq(fnq(A, D)) :- integer(A), deq(D).
deq(rnq(B, D)) :- integer(B), deq(D).

nonnull(fnq(A, D)) :- integer(A), deq(D).
nonnull(rnq(B, D)) :- integer(B), deq(D).

deq(fdq(D)) :- nonnull(D).
deq(rdq(D)) :- nonnull(D).

nf(nullq).
nf(fnq(A, D)) :- integer(A), nf(D).

rewrite(D, D) :- nf(D).
%induction step for normal forms
rewrite(fnq(A, D), fnq(A, E)) :- integer(A), rewrite(D, E).

% for all forms other than normal forms
rewrite(rnq(B, nullq), fnq(B, nullq)):- integer(B). % basis of induction
rewrite(rdq(fnq(A, nullq)), nullq). % basis of induction

% rewrite(fdq(fnq(A, nullq)), nullq) follows from the more general rewrite
rewrite(fdq(fnq(A, D)), E):- integer(A), rewrite(D, E). % fdq for all nonnull

rewrite(rnq(B, fnq(A, D)), fnq(A, E)) :- % for rnq on normal forms
	integer(A), integer(B),
	rewrite(D, F),
	rewrite(rnq(B, F), E), nf(E).

rewrite(rnq(B, D), E) :- % for rnq on other forms
	integer(B),
	rewrite(D, F),
	rewrite(rnq(B, F), E).

rewrite(rdq(fnq(A, D)), fnq(A, E)) :-  % for rdq on normal forms
	integer(A),
	rewrite(D, F), nonnull(F),
	rewrite(rdq(F), E).

rewrite(rdq(D), E) :- % for rdq on other forms
	rewrite(D, F), rewrite(rdq(F), E).

% rewrite(rdq(rnq(B, D)), D) follows by induction from the various rewrites above
fv(fnq(A, D), A):- integer(A), deq(D). % value at the front of the dequeue
fv(D, B) :- rewrite(D,E), fv(E,B).
rv(fnq(A, nullq), B) :- integer(A), A=B.
rv(fnq(A, D), B) :- integer(A), rewrite(D, E), rv(E, B).
rv(D, B) :- rewrite(D, E), rv(E, B).

/* Testing
% Restoring file /usr/local/lib/Yap/startup
YAP version Yap-5.1.1
   ?-  % reconsulting /home/sak/prolog/deques.P...
 % reconsulted /home/sak/prolog/deques.P in module user, 0 msec 4096 bytes
yes
   ?- rewrite(fnq(2, fnq(1, nullq)), X).
X = fnq(2,fnq(1,nullq)) ? 
yes
   ?- rv(fnq(1, fnq(2, nullq)), B).
B = 2 ? 
yes
   ?- rv(rnq(3, fnq(1, fnq(2, nullq))), B).
B = 3 ? 
yes
   ?- rewrite(rnq(4, fdq(fnq(1, fnq(2, rnq(3, nullq))))), X).
X = fnq(2,fnq(3,fnq(4,nullq))) ? 
yes
   ?- rv(rnq(4, fdq(fnq(1, fnq(2, rnq(3, nullq))))), B).
B = 4 ? 
yes
   ?- rv(rdq(rnq(4, fdq(fnq(1, fnq(2, rnq(3, nullq)))))), B).
B = 3 ? 
yes
   ?- fv(rnq(4, fdq(fnq(1, fnq(2, rnq(3, nullq))))), B).
B = 2 ? 
yes
*/