theorem :: SCMFSA6A:34
for j being Instruction of SCM+FSA
for I being Program of holds card (I ";" j) = (card I) + 2