theorem :: SCM_HALT:72

for P1, P2 being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being really-closed InitHalting Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s & I c= P1 & I c= P2 holds
( LifeSpan (P1,s) = LifeSpan (P2,s) & Result (P1,s) = Result (P2,s) ) by Lm5;