theorem Th17: :: SCMBSORT:27

for I, J being Program of
for i being ins-loc-free Instruction of SCM+FSA st i <> halt SCM+FSA holds
((I ";" i) ";" J) . (card I) = i