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
>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.
The most important thing of course, is to use witnesses
for which the existential is true, then you have a chance.
You not only need out_a1! to be \in real 20 .. real 30
you need SScomp.a1 \in real 20 .. real 30
so you must supply as witness for SScomp not a variable
but a binding in which the value of the component a1 is
\in real 20 .. real 30.
If you do that then the proof tool will simplify the
"binding.a1" expression to the real number and the
proof will go through.
Proofpower mailing list