let P1, P2 be Instruction-Sequence of SCM+FSA; :: thesis: for s1, s2 being State of SCM+FSA
for I being really-closed Program of SCM+FSA st I is_halting_on s1,P1 & DataPart s1 = DataPart s2 holds
( LifeSpan ((P1 +* I),(Initialize s1)) = LifeSpan ((P2 +* I),(Initialize s2)) & Result ((P1 +* I),(Initialize s1)) = Result ((P2 +* I),(Initialize s2)) )
let s1, s2 be State of SCM+FSA; :: thesis: for I being really-closed Program of SCM+FSA st I is_halting_on s1,P1 & DataPart s1 = DataPart s2 holds
( LifeSpan ((P1 +* I),(Initialize s1)) = LifeSpan ((P2 +* I),(Initialize s2)) & Result ((P1 +* I),(Initialize s1)) = Result ((P2 +* I),(Initialize s2)) )
set D = Data-Locations ;
let I be really-closed Program of SCM+FSA; :: thesis: ( I is_halting_on s1,P1 & DataPart s1 = DataPart s2 implies ( LifeSpan ((P1 +* I),(Initialize s1)) = LifeSpan ((P2 +* I),(Initialize s2)) & Result ((P1 +* I),(Initialize s1)) = Result ((P2 +* I),(Initialize s2)) ) )
set ss2 = Initialize s2;
set PP2 = P2 +* I;
set ss1 = Initialize s1;
set PP1 = P1 +* I;
assume A1: I is_halting_on s1,P1 ; :: thesis: ( not DataPart s1 = DataPart s2 or ( LifeSpan ((P1 +* I),(Initialize s1)) = LifeSpan ((P2 +* I),(Initialize s2)) & Result ((P1 +* I),(Initialize s1)) = Result ((P2 +* I),(Initialize s2)) ) )
then A2: P1 +* I halts_on Initialize s1 ;
then A3: Result ((P1 +* I),(Initialize s1)) = Comput ((P1 +* I),(Initialize s1),(LifeSpan ((P1 +* I),(Initialize s1)))) by EXTPRO_1:23;
assume A4: DataPart s1 = DataPart s2 ; :: thesis: ( LifeSpan ((P1 +* I),(Initialize s1)) = LifeSpan ((P2 +* I),(Initialize s2)) & Result ((P1 +* I),(Initialize s1)) = Result ((P2 +* I),(Initialize s2)) )
then I is_halting_on s2,P2 by A1, SCMFSA8B:5;
then A5: P2 +* I halts_on Initialize s2 ;

A6: now :: thesis: for l being Nat st CurInstr ((P2 +* I),(Comput ((P2 +* I),(Initialize s2),l))) = halt SCM+FSA holds
LifeSpan ((P1 +* I),(Initialize s1)) <= l

let l be Nat; :: thesis: ( CurInstr ((P2 +* I),(Comput ((P2 +* I),(Initialize s2),l))) = halt SCM+FSA implies LifeSpan ((P1 +* I),(Initialize s1)) <= l )
assume A7: CurInstr ((P2 +* I),(Comput ((P2 +* I),(Initialize s2),l))) = halt SCM+FSA ; :: thesis: LifeSpan ((P1 +* I),(Initialize s1)) <= l
CurInstr ((P1 +* I),(Comput ((P1 +* I),(Initialize s1),l))) = CurInstr ((P2 +* I),(Comput ((P2 +* I),(Initialize s2),l))) by A1, A4, Th62;
hence LifeSpan ((P1 +* I),(Initialize s1)) <= l by A2, A7, EXTPRO_1:def 15; :: thesis: verum

end;

CurInstr ((P2 +* I),(Comput ((P2 +* I),(Initialize s2),(LifeSpan ((P1 +* I),(Initialize s1)))))) = CurInstr ((P1 +* I),(Comput ((P1 +* I),(Initialize s1),(LifeSpan ((P1 +* I),(Initialize s1)))))) by A1, A4, Th62
.= halt SCM+FSA by A2, EXTPRO_1:def 15 ;
hence LifeSpan ((P1 +* I),(Initialize s1)) = LifeSpan ((P2 +* I),(Initialize s2)) by A6, A5, EXTPRO_1:def 15; :: thesis: Result ((P1 +* I),(Initialize s1)) = Result ((P2 +* I),(Initialize s2))
then Result ((P2 +* I),(Initialize s2)) = Comput ((P2 +* I),(Initialize s2),(LifeSpan ((P1 +* I),(Initialize s1)))) by A5, EXTPRO_1:23;
hence Result ((P1 +* I),(Initialize s1)) = Result ((P2 +* I),(Initialize s2)) by A1, A4, A3, Th62; :: thesis: verum