# Re: [ProofPower] Calculate preconditions in Z using ProofPower

Roger,

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
>
> (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
numbers).
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
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com