for i being Instruction of SCMPDS
for I, J being Program of SCMPDS holds ((I ';' i) ';' J) . (card I) = i