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
I quite often find that I want to use a new character in
ProofPower HOL.
However, ProofPower seems to be quite fussy about what
characters you use.
For example, there are three "spares" at the moment,
which would be useful for me. They wouldn't look right
in xpp but I could get them to print nice
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
