/*
Для всех[ "x": слагаемое ; y: real_выражение ],
если[ y==1 ],
то[ x*(y) ] => [x] ("умножение на единицу"),
если, кроме того,[].
*/
Для всех[ "x": слагаемое ; y: real_выражение ],
если[ y==1 ],
то[ (y)*(x) ] => [x] ("умножение на единицу"),
если, кроме того,[].
a, b, "с" : слагаемое.
/* Определение функции вес */
вес: real_выражение -> real_выражение.
вес(a)=10000.
вес(b)=10001.
Для всех[ "x": real ]
[ вес(x)] => [ x] ("вес числа").
Для всех[ "x", y: real_выражение ]
[ вес((x)*(y))] => [(вес(x))+(вес(y))] ("вес произведения").
Для всех["x",y: real_выражение ],
если[ вес(y)то [ (x)*(y)] => [ (y)*(x)] ("коммутативность"),
если, кроме того,[].
/* Вопросы: */.
/* Чему равно a*1? */.
/*Чему равно 1*(a)?*/.
/* вес((a)*(b))?*/.
