off rlabout;



rlset(qqe,ofsf);


{}


% Example from C. Strasser's diploma thesis
% Ch.10. Software Verifikation, p.171
f := ex({q},((j > 5 and radd(a,q) == qepsilon) or (radd(a,q) <<>>
qepsilon and lhead(radd(a,q)) > 23 + j)) and lhead(radd(a,q)) = x)$



rlqe f;


(a - x = 0 and a - j - 23 > 0) or j - x + 23 < 0


end;

