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