Also, what levels of isolation do you actually offer? Serialized snapshot isolation appears to be MVCC, but I see you also have just snapshot isolation - what is the difference?
Edit: oh brother, the proof you link to, I just realized I bought that book some time ago and never got around to reading it... Transactional Information Systems by Weikum & Vossen, right? time for me to hit the books I guess. Still trying to get my head around that second graph you have drawn, can't work out how you have gotten it :(