theorem Th1: :: SCMPDS_6:6

for i being Instruction of SCMPDS
for I being Program of holds card (i ';' I) = (card I) + 1