Hi Thomas,

The usual order precedence for algebraic operators is built into DC
Proof. In this case r=c+a+b is interpreted as r=(c+a)+b, the left-
most + operator having the higher precedence. To make the
substitution you want, you must first apply the associative property
of + (needs to be proven), to get r=c+(a+b).

Dan


--- In dcproof@yahoogroups.com, Thomas Heye <1910-131@...> wrote:
>
> Hi list,
> there's something odd about substitution:
>
> Suppose you have
>
> r=c+a+b
> and
> x=a+b
>
> then substituting x in the 1st equation is impossible; whereas it
> works if a+b appears first.
>
> I guess it has something to do with '+' being a binary operation--
or
> is there another reason?
>
> Regards,
> Thomas
>