off rlabout;



rlset(qqe,ofsf);


{}


% 2-periodic queue of odd length with prefix [0,0] and postfix [1,1]:
p2 := ex(qp,q == ladd(0,ladd(0,radd(1,radd(1,qp)))) and
ex({x,y},x <> y and ladd(y,ladd(x,qp)) == radd(y,radd(x,qp))))$



rlqe p2;


(rtail(ltail(ltail(rtail(rtail(q))))) == qepsilon

 and ltail(ltail(rtail(rtail(q)))) <<>> qepsilon and 

lhead(ltail(ltail(rtail(rtail(q))))) - rhead(ltail(ltail(rtail(rtail(q))))) = 0

 and rhead(ltail(rtail(rtail(q)))) - 1 = 0 and rhead(rtail(rtail(q))) - 1 = 0

 and lhead(rtail(q)) = 0 and lhead(q) = 0) or (

ltail(ltail(ltail(ltail(rtail(rtail(q))))))

 == rtail(rtail(ltail(ltail(rtail(rtail(q))))))

 and rtail(ltail(ltail(rtail(rtail(q))))) <<>> qepsilon and 

lhead(rtail(ltail(ltail(rtail(rtail(q))))))

 - rhead(ltail(ltail(ltail(rtail(rtail(q)))))) = 0 and 

lhead(ltail(ltail(rtail(rtail(q))))) - rhead(ltail(ltail(rtail(rtail(q))))) = 0 

and rhead(ltail(ltail(ltail(rtail(rtail(q))))))

 - rhead(ltail(ltail(rtail(rtail(q))))) <> 0

 and rhead(ltail(rtail(rtail(q)))) - 1 = 0 and rhead(rtail(rtail(q))) - 1 = 0

 and lhead(rtail(q)) = 0 and lhead(q) = 0)


end;

