Finished xmas shopping at B&N. Hacking on some generalizations of my LinLog paper. Went through and added coproduct types and generalized polynomial recursive types to mu alpha . delta such that alpha only occurs positively in delta. I think I'll try to dig into the polytime proof tomorrow. Probably will need to characterize how many reduction steps it takes to eliminate iteration as a function of delta and the number of free diamonds.
