# Unclear logic notation for PFX program rules

I'm very new to this so please bear with me.

I found this document describing the PFX language, a stack-oriented language where the instructions act on a stack and replace the arguments with the result.

The image is supposed to be the rules describing the logic of a PFX program, but being very new to logical symbols, I can barely read it.

From what I understand, the top parts are suppositions and the bottom parts are conclusions. The first one, to me, reads, if i is different from n, then if either of the vk's implies i, the program declares an error. But I can tell my understanding is deeply flawed. I searched and have found close to no similar rules.

Also, the use of the letter "i" seems unclear to me mostly.

If someone can explain with words what the rules actually mean, it would help me a lot.

Thank you.

$v_1,\dots,v_n\vdash \cdots$ means "in the environment $v_1,\dots,v_n$, such-and-such is true". (It's not an "or", and it doesn't mean "implies".) See What does ⊢ mean in operational semantics?.