theorem Th4: :: SCMP_GCD:4

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