I'm very new to this so please bear with me.
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.