Re: A question about structural congruence

[Davide Sangiorgi <Davide.Sangiorgi@xxxxxxxxxxxxxxx>]

Sorry, i overlooked n!=m, my examples were using n=m and hence do not
apply -- thanks Luis (see below)

davide

---------------------------


 From: Luis Caires <Luis.Caires@xxxxxxxxxxxxx>
 Subject: Re: A question about structural congruence


Hi Davide,


Note that there are two alternative cases (a) and (b);
and (b) should apply when the roles of the
topmost restrictions do not "match":

>  either (a) P == Q{n<->m} (where {n<->m} denotes exchange of n and m),
>  or          (b) P == (nu m)P' and Q == (nu n)Q' and P' == Q' [ for some
P' and Q' ].

In your first example,
(nu n)P = (nu n) n.0 == (nu m)(nu n) n.0 = (nu m)Q
hence P = n.0 and Q = (nu n) n.0
But then P == (nu m) n.0 (since m is not free in n.0) so we
can pick P' = n.0 and P == (nu m)P'.
On the other hand, we may pick Q' = n.0.
So Q == (nu n)Q' and therefore P' == Q'. So (b) holds.
Your second example also goes through
in a similar way,  note that in (nu n)P == (nu m)Q
I'm assuming n!=m, so we need to start from say
(nu x)(nu y) (x.x + y)  ==   (nu z)(nu y) (y.y + z)...

Luis
  
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The "models for mobility" mailing list     mailto:moca@xxxxxxxxxxxxxxx
 http://www-sop.inria.fr/mimosa/personnel/Davide.Sangiorgi/moca.html