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