On Friday 05 June 2009 09:20:11 Artur Oliveira Gomes wrote:
>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
>numbers).
>It will eliminate the predicate which says that out_a1 \in |R, o
Roger,
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
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 nee
Hi there,
I am trying to calculate preconditions of operations in Z using ProofPower.
But after strip and rewriting, I can not be able to current goal. (see
attached file)
I am not pretty sure of which steps should I take to achieve the goal.
Maybe I am not using the correct witnesses in the z_E_t
