let P1, P2 be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for s1, s2 being State of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on s1,P1 & I is_halting_on s1,P1 & DataPart s1 = DataPart s2 holds
( LifeSpan ((P1 +* I),(s1 +* (Initialize I))) = LifeSpan ((P2 +* I),(s2 +* (Initialize I))) & Result ((P1 +* I),(s1 +* (Initialize I))), Result ((P2 +* I),(s2 +* (Initialize I))) equal_outside NAT )
let s1, s2 be State of SCM+FSA; :: thesis: for I being Program of SCM+FSA st I is_closed_on s1,P1 & I is_halting_on s1,P1 & DataPart s1 = DataPart s2 holds
( LifeSpan ((P1 +* I),(s1 +* (Initialize I))) = LifeSpan ((P2 +* I),(s2 +* (Initialize I))) & Result ((P1 +* I),(s1 +* (Initialize I))), Result ((P2 +* I),(s2 +* (Initialize I))) equal_outside NAT )
set D = Data-Locations SCM+FSA;
let I be Program of SCM+FSA; :: thesis: ( I is_closed_on s1,P1 & I is_halting_on s1,P1 & DataPart s1 = DataPart s2 implies ( LifeSpan ((P1 +* I),(s1 +* (Initialize I))) = LifeSpan ((P2 +* I),(s2 +* (Initialize I))) & Result ((P1 +* I),(s1 +* (Initialize I))), Result ((P2 +* I),(s2 +* (Initialize I))) equal_outside NAT ) )
assume A1: I is_closed_on s1,P1 ; :: thesis: ( not I is_halting_on s1,P1 or not DataPart s1 = DataPart s2 or ( LifeSpan ((P1 +* I),(s1 +* (Initialize I))) = LifeSpan ((P2 +* I),(s2 +* (Initialize I))) & Result ((P1 +* I),(s1 +* (Initialize I))), Result ((P2 +* I),(s2 +* (Initialize I))) equal_outside NAT ) )
set ss2 = s2 +* (Initialize I);
set PP2 = P2 +* I;
set ss1 = s1 +* (Initialize I);
set PP1 = P1 +* I;
A2: ProgramPart I = I by RELAT_1:209;
assume A3: I is_halting_on s1,P1 ; :: thesis: ( not DataPart s1 = DataPart s2 or ( LifeSpan ((P1 +* I),(s1 +* (Initialize I))) = LifeSpan ((P2 +* I),(s2 +* (Initialize I))) & Result ((P1 +* I),(s1 +* (Initialize I))), Result ((P2 +* I),(s2 +* (Initialize I))) equal_outside NAT ) )
then A4: P1 +* I halts_on s1 +* (Initialize I) by SCMFSA7B:def 8, A2;
then A5: Result ((P1 +* I),(s1 +* (Initialize I))) = Comput ((P1 +* I),(s1 +* (Initialize I)),(LifeSpan ((P1 +* I),(s1 +* (Initialize I))))) by EXTPRO_1:23;
assume A6: DataPart s1 = DataPart s2 ; :: thesis: ( LifeSpan ((P1 +* I),(s1 +* (Initialize I))) = LifeSpan ((P2 +* I),(s2 +* (Initialize I))) & Result ((P1 +* I),(s1 +* (Initialize I))), Result ((P2 +* I),(s2 +* (Initialize I))) equal_outside NAT )
then I is_halting_on s2,P2 by A1, A3, SCMFSA8B:8;
then A7: P2 +* I halts_on s2 +* (Initialize I) by SCMFSA7B:def 8, A2;

A8: now

let l be Element of NAT ; :: thesis: ( CurInstr ((P2 +* I),(Comput ((P2 +* I),(s2 +* (Initialize I)),l))) = halt SCM+FSA implies LifeSpan ((P1 +* I),(s1 +* (Initialize I))) <= l )
assume A9: CurInstr ((P2 +* I),(Comput ((P2 +* I),(s2 +* (Initialize I)),l))) = halt SCM+FSA ; :: thesis: LifeSpan ((P1 +* I),(s1 +* (Initialize I))) <= l
CurInstr ((P1 +* I),(Comput ((P1 +* I),(s1 +* (Initialize I)),l))) = CurInstr ((P2 +* I),(Comput ((P2 +* I),(s2 +* (Initialize I)),l))) by A1, A3, A6, Th100;
hence LifeSpan ((P1 +* I),(s1 +* (Initialize I))) <= l by A4, A9, EXTPRO_1:def 14; :: thesis: verum

end;

CurInstr ((P2 +* I),(Comput ((P2 +* I),(s2 +* (Initialize I)),(LifeSpan ((P1 +* I),(s1 +* (Initialize I))))))) = CurInstr ((P1 +* I),(Comput ((P1 +* I),(s1 +* (Initialize I)),(LifeSpan ((P1 +* I),(s1 +* (Initialize I))))))) by A1, A3, A6, Th100
.= halt SCM+FSA by A4, EXTPRO_1:def 14 ;
hence LifeSpan ((P1 +* I),(s1 +* (Initialize I))) = LifeSpan ((P2 +* I),(s2 +* (Initialize I))) by A8, A7, EXTPRO_1:def 14; :: thesis: Result ((P1 +* I),(s1 +* (Initialize I))), Result ((P2 +* I),(s2 +* (Initialize I))) equal_outside NAT
then Result ((P2 +* I),(s2 +* (Initialize I))) = Comput ((P2 +* I),(s2 +* (Initialize I)),(LifeSpan ((P1 +* I),(s1 +* (Initialize I))))) by A7, EXTPRO_1:23;
hence Result ((P1 +* I),(s1 +* (Initialize I))), Result ((P2 +* I),(s2 +* (Initialize I))) equal_outside NAT by A1, A3, A6, A5, Th100; :: thesis: verum