Hi Thomas,

You will get that message sometimes when you do Existential
Specification. It is for informational purposes only to help you
understand warnings sometimes given with the Premise Rule.

The x in your message refers to the variable being specified. The
other variables in your message are "green" variables in previous
active statements.

See the example in "Specification" in the User Reference Guide. Also
see documentation on the "Premise Rule" which will give you warnings
about unintended dependencies that could save you much frustration.

Is this confusing? It is a difficult concept that almost never comes
up in math courses. If the User documentation still leaves you (or
other readers here) confused on this matter, PLEASE let me know and
I will consider rewriting these sections or reworking the messages.

Regards,
Dan


--- In dcproof@yahoogroups.com, Thomas Heye <1910-131@...> wrote:
>
> Hi Dan,
> here's a fragment of a proof. Applying the uspec/espec rule to line
> 94, I get the warning: "x will depend on: x1, x2, y1, y2."
>
> Note that none of these variables occur inside the "source" I
> generalized; nor occurs x inside the block where x1..., y2 occur.
>
> It's not too bad, I just wanted to tell you :-).
>
> Regards,
>
> Thomas
>
>
> [Non-text portions of this message have been removed]
>