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 <artur.o.go...@gmail.com <mailto:artur.o.go...@gmail.com>>

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

Reply via email to