On Friday 05 June 2009 08:32:29 Artur Oliveira Gomes wrote:


>Could someone guide me through this please?

The main problem with your proof so far is that
you have constructed the witness for the existential
from free variables, which won't necessarily satisfy
the required conditions.

You need to replace them with expressions which
satisfy the predicates in your schemas, then
your proof can proceed.

(for example, out_a1! will have to be a real number
between 20 and 30)

Roger Jones

Proofpower mailing list

Reply via email to