let s1, s2 be State of SCMPDS; :: thesis: for P1, P2 being the Instructions of SCMPDS -valued ManySortedSet of NAT
for I being Program of SCMPDS st I is_closed_on s1,P1 & I is_halting_on s1,P1 & stop I c= P1 & stop I c= P2 & Start-At (0,SCMPDS) c= s1 & Start-At (0,SCMPDS) c= s2 & NPP s1 = NPP s2 holds
( LifeSpan (P1,s1) = LifeSpan (P2,s2) & NPP (Result (P1,s1)) = NPP (Result (P2,s2)) )
let P1, P2 be the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: thesis: for I being Program of SCMPDS st I is_closed_on s1,P1 & I is_halting_on s1,P1 & stop I c= P1 & stop I c= P2 & Start-At (0,SCMPDS) c= s1 & Start-At (0,SCMPDS) c= s2 & NPP s1 = NPP s2 holds
( LifeSpan (P1,s1) = LifeSpan (P2,s2) & NPP (Result (P1,s1)) = NPP (Result (P2,s2)) )
let I be Program of SCMPDS; :: thesis: ( I is_closed_on s1,P1 & I is_halting_on s1,P1 & stop I c= P1 & stop I c= P2 & Start-At (0,SCMPDS) c= s1 & Start-At (0,SCMPDS) c= s2 & NPP s1 = NPP s2 implies ( LifeSpan (P1,s1) = LifeSpan (P2,s2) & NPP (Result (P1,s1)) = NPP (Result (P2,s2)) ) )
assume that
A1: I is_closed_on s1,P1 and
A2: I is_halting_on s1,P1 and
A3: stop I c= P1 and
A4: stop I c= P2 and
B3: Start-At (0,SCMPDS) c= s1 and
B4: Start-At (0,SCMPDS) c= s2 and
A5: NPP s1 = NPP s2 ; :: thesis: ( LifeSpan (P1,s1) = LifeSpan (P2,s2) & NPP (Result (P1,s1)) = NPP (Result (P2,s2)) )
DataPart s1 = DataPart s2 by A5, SCMPDS_6:4;
then A6: I is_halting_on s2,P2 by A1, A2, SCMPDS_6:37;
A7: Initialize s1 = s1 by B3, FUNCT_4:104;
A8: Initialize s2 = s2 by B4, FUNCT_4:104;
P2 = P2 +* (stop I) by A4, FUNCT_4:104;
then A9: P2 halts_on s2 by A6, SCMPDS_6:def 3, A8;
P1 = P1 +* (stop I) by A3, FUNCT_4:104;
then A10: P1 halts_on s1 by A2, SCMPDS_6:def 3, A7;

A11: now

let l be Element of NAT ; :: thesis: ( CurInstr (P2,(Comput (P2,s2,l))) = halt SCMPDS implies LifeSpan (P1,s1) <= l )
assume A12: CurInstr (P2,(Comput (P2,s2,l))) = halt SCMPDS ; :: thesis: LifeSpan (P1,s1) <= l
CurInstr (P1,(Comput (P1,s1,l))) = CurInstr (P2,(Comput (P2,s2,l))) by A1, A3, A4, A5, Th26, B3, B4;
hence LifeSpan (P1,s1) <= l by A10, A12, EXTPRO_1:def 14; :: thesis: verum

end;

CurInstr (P2,(Comput (P2,s2,(LifeSpan (P1,s1))))) = CurInstr (P1,(Comput (P1,s1,(LifeSpan (P1,s1))))) by A1, A3, A4, A5, Th26, B3, B4
.= halt SCMPDS by A10, EXTPRO_1:def 14 ;
hence LifeSpan (P1,s1) = LifeSpan (P2,s2) by A11, A9, EXTPRO_1:def 14; :: thesis: NPP (Result (P1,s1)) = NPP (Result (P2,s2))
then A13: Result (P2,s2) = Comput (P2,s2,(LifeSpan (P1,s1))) by A9, EXTPRO_1:23;
Result (P1,s1) = Comput (P1,s1,(LifeSpan (P1,s1))) by A10, EXTPRO_1:23;
hence NPP (Result (P1,s1)) = NPP (Result (P2,s2)) by A1, A3, A4, A5, A13, Th26, B3, B4; :: thesis: verum