theorem :: SCMFSA6A:2

for m being Nat
for I being Program of holds Reloc ((Directed I),m) = ((id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA) .--> (goto (m + (card I))))) * (Reloc (I,m))