<div>I think simplifying notions of path expressions aren't necessary. IMO the challenge here is to come to discreet formal steps. I'd start with applying all normalisations in <a href="http://www.w3.org/TR/xquery-semantics/#id-axis-steps">http://www.w3.org/TR/xquery-semantics/#id-axis-steps</a>, from which a single evaluable function could be derived. The function should be rewritable as yielding the same set (for /x/w and //w). Next the relation to the subset should become obvious.</div><div><br></div><div><br></div><div>Op woensdag 27 januari 2016 heeft Michael Kay <<a href="javascript:_e(%7B%7D,'cvml','mike@saxonica.com');" target="_blank">mike@saxonica.com</a>> het volgende geschreven:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><br>
><br>
><br>
> If you want to do a formal proof, you might want to use simplified notions of XML documents and path expressions.<br>
<br>
It seems to be a long-standing tradition that computer scientists, when asked to prove a difficult conjecture C, respond by giving a proof for a simplified conjecture C'. While this might lead to progress in the long run, and enables them to get papers published in the academic literature, it is totally useless to practical engineeers who want to know whether they can safely rely on C.<br>
<br>
Michael Kay<br>
Saxonica<br>
<br>
<br>
<br>
</blockquote></div>
<br><br>-- <br><div>
<p> 
W.S. Hager<br>
Lagua Web Solutions<br>
<a href="http://lagua.nl/" target="_blank">http://lagua.nl</a><br></p></div><br>