theorem Th1: :: SCMFSA8B:5

for P1, P2 being Instruction-Sequence of SCM+FSA
for s1, s2 being State of SCM+FSA
for I being really-closed Program of SCM+FSA st DataPart s1 = DataPart s2 & I is_halting_on s1,P1 holds
I is_halting_on s2,P2