Artur, You can use:

## Advertising

a(conv_tac(ONCE_MAP_C z_float_conv));

`to change things like "3.0" into "real 3" or "3.5" into "7/2" and then`

`rewriting in the proof context 'z_reals will do the arithmetic for you.`

`We don't do this automatically in the proof context 'z_reals in case`

`you have floating literals like 1.2e3333333 which would take ages to`

`expand. Perhaps we should have another proof context 'z_floats for use`

`at the user's discretion to do the expansion as part of rewriting.`

Regards, Rob. On 26 Mar 2009, at 18:18, Artur Oliveira Gomes wrote:

Rob, Thank you. Just one more question: and how about floating numbers? How to prove it? For example: set_merge_pcs["'z_reals", "z_library"]; set_goal([], %SZT% 0.4 %mem% 0.1 ..%down%R 1.9 %>%); a(rewrite_tac[z_%bbR%_dot_dot_def]); With those steps, ProofPower change the goal to: %SZT%0.1 %leq%%down%R 0.4 %and% 0.4 %leq%%down%R 1.9%>% How can I prove it? Thanks again. Regards, -- Artur Oliveira Gomes _______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

_______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com