maybe it's just my previous exposure to overline notation in logic/type systems where the premise goes above the conclusion but i found this pretty hard to read.
also, the use of y in x^y to refer to the previous y's exponent also confused me for a moment until i realized what you were doing -- i'm used to seeing this notation in math where x^y would have a totally different meaning.