!((A -o B) -o (C (x) D)), !E, !(F -o G) |- H -o I
are derivable, I can decide whether things like
!((!A -o !B) -o (!C (x) !D)), !E, !(!F -o !G) |- !H -o !I
with lots of "deeply buried" !s are derivable. This restriction of MELL to only "top-left" bangs is, in turn, equivalent to a slight variant of Petri Nets, or at least I think I've worked it out correctly. It doesn't even seem entirely impossible that the standard Petri Net decidability machinery might even be adaptable to these bizarre Petri-Nets-with-a-Stack. I'm not quite ready to lay my left nut on the line as Rudich did about Primes in P, but I'm really starting to suspect MELL is decidable.