[xquery-talk] Function for determining one XPath as subset of another

[Christian Grün]

> Its a common practice for everybody, who needs to come up with formal proofs. You start with the most simplified definitions possible, that capture the essence of the problem.
> Then you get the skeleton of the proof that is hopefully very simple. Then you can add details back, hoping that the proof remains simple and tractable.
>
> So imagine starting the proof while considering all the possible variations of path expressions, all the Infoset stuff, all XML Schema details. I think its hopeless.

I’m completely in line with Michael’s observations. It would obviously
be nice to have proofs for the full rule sets of the discussed
languages; but as experience shows, no one will do it (the rare
exception might prove the rule), so we are stuck with the work that is
of limited practical use.