2009/6/5 Roger Bishop Jones <>

> 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)

In fact, in this particular case, using out_a1!  as a real number between 20
and 30
has the same effect than rewrite the definition of "pre Op" and "|R" (real
It will eliminate the predicate which says that out_a1 \in |R, or by using a
real number,
real 30 \in |R.

>From the produced subgoals, I have to prove the state SS. After rewriting,
new subgoals are produced, and it becomes harder to prove, since the
subgoals are like
the following:

SScomp.a1 \in real 20 .. real 30

It seems quite strange for me to prove it without any clue.

Artur Oliveira Gomes
Proofpower mailing list

Reply via email to