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;