Artur,
You may like to know that there is a so-called "component" proof context called
'z_reals which will make evaluation of real arithmetic expressions happen
automatically when you rewrite.
Try:
set_merge_pcs["'z_reals", "z_library"];
set_goal([], %SZT% real 30 %mem% real 20 ..%down%R real 40 %>%);
a(rewrite_tac[z_%bbR%_dot_dot_def]);
Regards,
Rob.
Artur Oliveira Gomes wrote:
Hi there
Now I know how to prove it: using z_R_<=_conv.
Thanks anyway,
Artur
2009/3/25 Artur Oliveira Gomes <[email protected]
<mailto:[email protected]>>
Hi there,
How could I prove that given two real numbers, 20 and 30, that 20 <=40?
Moreover, given three real numbers, 20, 30 and 40,
how could I prove that 30 <in> 20..40.
Regards,
--
Artur Oliveira Gomes
--
Artur Oliveira Gomes
------------------------------------------------------------------------
_______________________________________________
Proofpower mailing list
[email protected]
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
_______________________________________________
Proofpower mailing list
[email protected]
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
