I just wanted somewhere to note this. The system on page 40-41 of Asperti's book is not implemented anywhere AFAICT. If you read chapter 12 on the BOHM machine, BOHM is actually based on Stefano Guerrini's work with muxes and uses a fan with two auxiliary ports and a triangle with one auxiliary port. So in fact their system is quite similar to Lambdascope's, with the addition of explicit level indices on the nodes.