Here is Girard's `technical condition', then the reformulation by
Abramsky and Mellies (in their LICS'99 paper):
(G) if v is a weight generated by the weights occurring in \Theta,
and x is a &-vertex, then v.~w(x) does not depend on the
eigenvariable p_x.
(AM) If v is a weight occuring in \Theta and x is a &-vertex,
if v depends on p_x then v < w(L).
(In (G), ~z means "not z".) The following is the simplest
(non-monomial) example I could come up with that satisfies (G) but not
(AM):
p|q ~p~q
_______________ 1 1
| ____________| \ / p|q = "p or q"
| | __________| + ~p~q = "(not p) and (not q)"
| \ / | / 1 = tensor unit
| &q \ / * = tensor
\ / * &p = "&-vertex with eigenweight p"
&p
(literals and remaining weights implicit). Note that this is in fact
a (non-monomial) MALL proof net --- so (AM) is non-sensical ("too
strong") once the monomial constraint is removed. Similarly, the
3-formula Gustave example fails (AM), but satisfies (G). [To see that
the Gustave example satisfies (G), observe that it satisfies
(PRESENCE) an axiom link z depends on a &-vertex x in a slice S
only if x is in S.
proved equivalent to (G) in one of the other FAQ answers.]
In summary:
(1) The Gustave example satisfies Girard's technical condition.
(2) Girard's technical condition does not imply softness.
(3) The Abramsky-Mellies technical condition is strictly stronger than
Girard's technical condition.
(4) The Abramsky-Mellies technical condition becomes "too strong" upon
relaxing the monomial constraint (cf. the example drawn above).
DJDH 2003/07/16