[Rodin-b-sharp-user] Question about Static Check of Relational Predicate

[Shawn Z. <sur...@gm...>]

Hi Rodin Developers,

While I was reading the "The Event-B Mathematical Language, March 26, 2009",
I found the following statements confusing:

On page 24, it says:
---------------------------
And the following formula is also illegible (failing to satisfy the
second condition)
(λx·x∈Z| x+ 1) = (λx·x∈Z| x+ 1)
it should be written
(λx·x∈Z| x+ 1) = (λy·y∈Z| y+ 1)
---------------------------


And According to the productions rule "pred-rel" on page 25 it is illegible.
But when I typed it into Rodin 2.6, no error was shown.

My question is: it this a typo, or am I missing anything?

Thanks!
Shawn Zhang