3.2.3 Requirements Section
We put only a file called ARYTM on the requirements section at present.
ARYTM is a file for using arithmetic operation comparatively freely.
For example, although the following formula becomes truth
without giving a reason, this is the favor of ARYTM (however, a reason
is required for 132-24 = 108) .
132 + 24 = 156;
For example, the following is a no error. Multiplication
and inequality are also judged automatically. Let's keep in mind that ARYTM
is contained also in notation.
environ
vocabulary REAL_1;
notation ARYTM,REAL_1;
constructors REAL_1;
requirements ARYTM;
begin
theorem 10+4=14 & 10+5=15 &
10+6=16 & 10+7=17;
theorem 10+10=20 & 1000+1000=2000 &
10000+10000=20000;
theorem 44 2=88;
theorem 2 · 1=2 & 3 ·
2=6 & 4 · 5=20;
theorem 45≦50;
theorem 45く50;