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;