let P1, P2 be the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: thesis: for s1, s2 being 0 -started State of SCMPDS
for I being parahalting Program of SCMPDS st stop I c= P1 & stop I c= P2 & NPP s1 = NPP s2 holds
( LifeSpan (P1,s1) = LifeSpan (P2,s2) & NPP (Result (P1,s1)) = NPP (Result (P2,s2)) )
let s1, s2 be 0 -started State of SCMPDS; :: thesis: for I being parahalting Program of SCMPDS st stop I c= P1 & stop I c= P2 & NPP s1 = NPP s2 holds
( LifeSpan (P1,s1) = LifeSpan (P2,s2) & NPP (Result (P1,s1)) = NPP (Result (P2,s2)) )
let I be parahalting Program of SCMPDS; :: thesis: ( stop I c= P1 & stop I c= P2 & NPP s1 = NPP s2 implies ( LifeSpan (P1,s1) = LifeSpan (P2,s2) & NPP (Result (P1,s1)) = NPP (Result (P2,s2)) ) )
set SI = stop I;
assume that
A1: stop I c= P1 and
A2: stop I c= P2 and
A3: NPP s1 = NPP s2 ; :: thesis: ( LifeSpan (P1,s1) = LifeSpan (P2,s2) & NPP (Result (P1,s1)) = NPP (Result (P2,s2)) )
A4: P2 halts_on s2 by A2, SCMPDS_4:def 10;
A5: P1 halts_on s1 by A1, SCMPDS_4:def 10;

A6: now

let l be Element of NAT ; :: thesis: ( CurInstr (P2,(Comput (P2,s2,l))) = halt SCMPDS implies LifeSpan (P1,s1) <= l )
assume A7: 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, A2, A3, Th20;
hence LifeSpan (P1,s1) <= l by A5, A7, 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, A2, A3, Th20
.= halt SCMPDS by A5, EXTPRO_1:def 14 ;
hence LifeSpan (P1,s1) = LifeSpan (P2,s2) by A6, A4, EXTPRO_1:def 14; :: thesis: NPP (Result (P1,s1)) = NPP (Result (P2,s2))
then A8: Result (P2,s2) = Comput (P2,s2,(LifeSpan (P1,s1))) by A2, EXTPRO_1:23, SCMPDS_4:def 10;
Result (P1,s1) = Comput (P1,s1,(LifeSpan (P1,s1))) by A1, EXTPRO_1:23, SCMPDS_4:def 10;
hence NPP (Result (P1,s1)) = NPP (Result (P2,s2)) by A1, A2, A3, A8, Th20; :: thesis: verum