[TYPES] connectedness and acyclicity in IMLL proof nets

[Satoshi Matsuoka]

Dear Aurelien,

In MLL, your observation holds if a proof structure satisfies  
the equation #(ID) = #( x ) + 1, where #(ID) is the number of 
the ID-links and #( x ) is the number of the tensor-links in 
the proof structure. 

The equation is an invariant of MLL proof nets, which you can find 
in "Le Point Aveugle I" by Girard. 

Best regards, 
-- 
Satoshi Matsuoka
National Institute of
Advanced Industrial Science and Technology
1-1-1 Umezono,Tsukuba,Ibaraki
305-8563, Japan
E-mail : matsuoka at ni.aist.go.jp
TEL : +81-29-861-4106