Re: Deep inference and speed-up in proof search

Hi Alessio,

I am still not back in Canberra and am reading this via a browser but the
notion you seem to need is that CoS polynomially simulates LK but not vice
versa. A class of interesting formulae may be D'Agastino's class from [MD]
which shows that KE polynomially simulates LK but not vice versa (or some
tweeking of this class suited for CoS).

[MD] Mondadori and D'Agostino, "The taming of the cut", JLC 1994 (but the
date could be wrong).

Raj