2009/6/5 Roger Bishop Jones <r...@rbjones.com>
> 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
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 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
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