theorem Th13: :: SCMFSA6A:23

for I being preProgram of SCM+FSA
for k being Element of NAT holds Reloc ((Directed I),k) = (Reloc (I,k)) +~ ((halt SCM+FSA),(goto ((card I) + k)))