Note: Pigeonhole principle in deep inference

I have written a short note on the proof complexity of the propositional 
pigeonhole principle for `cut-free' deep inference:

http://www.anupamdas.com/items/PHPProofs/PHPProofs.pdf

An outline of the material is given below this message.

Together with some other results, I am planning to expand this to a full 
article on the complexity of combinatorial principles in deep inference, 
using broadly the same techniques as presented here.

Unfortunately the note currently relies on much of the existing 
literature, hindering the accessibility of any article derived from it.

I would appreciate any feedback on this, especially regarding any 
possible simplifications or existing confusions.

Kind regards,
Anupam

A note on proofs of the pigeonhole principle in deep inference.

The propositional pigeonhole principle (PHP) is known to have 
polynomial-size proofs in systems with cut [Bus], and 
quasipolynomial-size ( n ^ (log^c n) ) proofs in deep inference systems 
that are cut-free but exhibit dag-like behaviour [Jer], [BGGP]. In the 
absence of this behaviour nothing is known, although it has recently 
been shown that the `functional' and `onto' variants have 
polynomial-size proofs [Das]. Here we consider the unrestricted version 
and give quasipolynomial-size proofs in such systems, matching the upper