theorem :: SCMFSA6A:33

for i being Instruction of SCM+FSA
for J being Program of holds card (i ";" J) = (card J) + 2