Is MAX(a+b,c) = MAX(c,a+b) ?



Hi, to everybody,

below is some strange interaction between ASSUME and MAX

As a result, MAX is not always symmetric function of its arguments.
In my sci work normal definition of MAX is needed. Threfore, I found
a remedy (see at the bottom). But maybe my usage of ASSUME and MAX
is wrong? What was intended as regards MAX by developers ?

Thank you for any comments,
--
Alexander


normal behavior:

(C1) assume(c>a+b)$
(C2) MAX(a+b,c); MAX(c,a+b);
(D2)                                   c
(C3) 
(D3)                                   c
(C4) is(MAX(a+b,c)=MAX(c,a+b));
(D4)                                 TRUE


strange behavior:

(C1) assume(c<a+b)$
(C2) MAX(a+b,c); MAX(c,a+b);
(D2)                                 b + a
(C3) 
(D3)                             MAX(c, b + a)  #why it is not simplified ?
(C4) is(MAX(a+b,c)=MAX(c,a+b));
(D4)                                 FALSE      #why FALSE if must be TRUE ?


another version of the equally strange behavior:

(C1)  assume(a+b>c)$
(C2)  MAX(a+b,c); MAX(c,a+b);
(D2)                                 b + a
(C3) 
(D3)                             MAX(c, b + a) #why it is not simplified ?
(C4) is(MAX(a+b,c)=MAX(c,a+b));
(D4)                                 FALSE     #why FALSE if must be TRUE ?



interesting, that if nothing is assumed about a,b,c behavior is normal:

(C1)  MAX(a+b,c); MAX(c,a+b);
(D1)                             MAX(c, b + a)
(C2) 
(D2)                             MAX(c, b + a)
(C3) is(MAX(a+b,c)=MAX(c,a+b));
(D3)                                 TRUE


a remedy:

(C1) matchdeclare(ud,true,vd,true)$
(C2) SMAX(ud, vd) ::= BUILDQ([ud, vd], 
                      IF max(ud,vd)=vd THEN vd 
		      ELSE if max(ud,vd)=ud then ud 
		      else max(vd,ud))$
(C3) assume(a+b>c)$
(C4) SMAX(a+b,c); SMAX(c,a+b);
(D4)                                 b + a
(C5) 
(D5)                                 b + a
(C6) is(SMAX(a+b,c)=SMAX(c,a+b));
(D6)                                 TRUE