theorem :: SCM_HALT:71

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
for k being Nat holds
( Comput (P1,s,k) = Comput (P2,s,k) & CurInstr (P1,(Comput (P1,s,k))) = CurInstr (P2,(Comput (P2,s,k))) ) by Lm4;