avvisinc is redundant in the last two lines of the definition of locord

[RobinMorisset]

This is not a bug, but a proposed simplification.

These lines include the following parts:

• (stor[W]) . (hb & avvisinc) . avdv
• visdv . (hb & avvisinc) . (stor[R]) Where avdv = stor[AVDEVICE] and visdv = stor[VISDEVICE]

We know that "SC0+SC1 = R+W" , and avvisinc = (rai[((SC0+SC1)->(AVDEVICE+VISDEVICE)) + ...]) - iden + ... , and no (R+W)&(AVDEVICE+VISDEVICE) (so we don't fall in the '- iden' case) So (stor[W]) . avdv in avvisinc, and visdv . (stor[R]) in avvisinc. So I suggest replacing "(hb & avvisinc)" by "hb" in these two lines. This in turn would allow us to remove (SC0+SC1)->(AVDEVICE+VISDEVICE) from avvisinc, since avvisinc no longer appears in a position where either end could be AVDEVICE or VISDEVICE.

[jeffbolznv]

I'm a bit torn on this. I like the consistency of having avvisinc everywhere there is an av/vis operation, even if it is redundant. But there's also an appeal to just saying "AVDEVICE/VISDEVICE affect everything and don't need to be factored into avvisinc."