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 > 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 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
