let P1, P2 be the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: thesis: for s1, s2 being State of SCMPDS
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 & ex k being Element of NAT st NPP (Comput (P1,s1,k)) = NPP s2 holds
NPP (Result (P1,s1)) = NPP (Result (P2,s2))
let s1, s2 be State of SCMPDS; :: 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 & ex k being Element of NAT st NPP (Comput (P1,s1,k)) = NPP s2 holds
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 & ex k being Element of NAT st NPP (Comput (P1,s1,k)) = NPP s2 implies NPP (Result (P1,s1)) = NPP (Result (P2,s2)) )
set pI = stop I;
assume A1: I is_closed_on s1,P1 ; :: thesis: ( not I is_halting_on s1,P1 or not stop I c= P1 or not stop I c= P2 or not Start-At (0,SCMPDS) c= s1 or not Start-At (0,SCMPDS) c= s2 or for k being Element of NAT holds not NPP (Comput (P1,s1,k)) = NPP s2 or NPP (Result (P1,s1)) = NPP (Result (P2,s2)) )
assume A3: I is_halting_on s1,P1 ; :: thesis: ( not stop I c= P1 or not stop I c= P2 or not Start-At (0,SCMPDS) c= s1 or not Start-At (0,SCMPDS) c= s2 or for k being Element of NAT holds not NPP (Comput (P1,s1,k)) = NPP s2 or NPP (Result (P1,s1)) = NPP (Result (P2,s2)) )
assume stop I c= P1 ; :: thesis: ( not stop I c= P2 or not Start-At (0,SCMPDS) c= s1 or not Start-At (0,SCMPDS) c= s2 or for k being Element of NAT holds not NPP (Comput (P1,s1,k)) = NPP s2 or NPP (Result (P1,s1)) = NPP (Result (P2,s2)) )
then A5: P1 = P1 +* (stop I) by FUNCT_4:104;
assume stop I c= P2 ; :: thesis: ( not Start-At (0,SCMPDS) c= s1 or not Start-At (0,SCMPDS) c= s2 or for k being Element of NAT holds not NPP (Comput (P1,s1,k)) = NPP s2 or NPP (Result (P1,s1)) = NPP (Result (P2,s2)) )
then XX: P2 = P2 +* (stop I) by FUNCT_4:104;
assume Start-At (0,SCMPDS) c= s1 ; :: thesis: ( not Start-At (0,SCMPDS) c= s2 or for k being Element of NAT holds not NPP (Comput (P1,s1,k)) = NPP s2 or NPP (Result (P1,s1)) = NPP (Result (P2,s2)) )
then A2: s1 = Initialize s1 by FUNCT_4:104;
then A6: P1 halts_on s1 by A3, SCMPDS_6:def 3, A5;
then consider n being Element of NAT such that
A7: CurInstr (P1,(Comput (P1,s1,n))) = halt SCMPDS by EXTPRO_1:30;
assume Start-At (0,SCMPDS) c= s2 ; :: thesis: ( for k being Element of NAT holds not NPP (Comput (P1,s1,k)) = NPP s2 or NPP (Result (P1,s1)) = NPP (Result (P2,s2)) )
then A9: s2 = Initialize s2 by FUNCT_4:104;
given k being Element of NAT such that A10: NPP (Comput (P1,s1,k)) = NPP s2 ; :: thesis: NPP (Result (P1,s1)) = NPP (Result (P2,s2))
set s3 = Comput (P1,s1,k);
set P3 = P1;
A11: IC in dom (Comput (P1,s1,k)) by COMPOS_1:9;
IC (Comput (P1,s1,k)) = IC (Initialize s2) by A10, A9, COMPOS_1:230
.= 0 by COMPOS_1:def 16 ;
then (IC ) .--> 0 c= Comput (P1,s1,k) by A11, FUNCOP_1:88;
then Start-At (0,SCMPDS) c= Comput (P1,s1,k) ;
then A14: Comput (P1,s1,k) = Initialize (Comput (P1,s1,k)) by FUNCT_4:104;

A15: now

let n be Element of NAT ; :: thesis: IC (Comput (P1,(Comput (P1,s1,k)),n)) in dom (stop I)
IC (Comput (P1,(Comput (P1,s1,k)),n)) = IC (Comput (P1,s1,(k + n))) by EXTPRO_1:5;
hence IC (Comput (P1,(Comput (P1,s1,k)),n)) in dom (stop I) by A1, A5, SCMPDS_6:def 2, A2; :: thesis: verum

end;

A18: Comput (P1,s1,(k + n)) = Comput (P1,(Comput (P1,s1,k)),n) by EXTPRO_1:5;
A19: Comput (P1,s1,(k + n)) = Comput (P1,s1,n) by A7, EXTPRO_1:6, NAT_1:11;
CurInstr (P1,(Comput (P1,(Comput (P1,s1,k)),n))) = CurInstr (P1,(Comput (P1,s1,(k + n)))) by A18
.= CurInstr (P1,(Comput (P1,s1,n))) by A19 ;
then P1 halts_on Comput (P1,s1,k) by A7, EXTPRO_1:30;
then A20: I is_halting_on Comput (P1,s1,k),P1 by A14, SCMPDS_6:def 3, A5;
A21: DataPart (Comput (P1,s1,k)) = DataPart s2 by A10, SCMPDS_6:4;
consider k being Element of NAT such that
A22: CurInstr (P1,(Comput (P1,s1,k))) = halt SCMPDS by A6, EXTPRO_1:30;
A23: P1 /. (IC (Comput (P1,s1,k))) = P1 . (IC (Comput (P1,s1,k))) by PBOOLE:158;
A25: P1 . (IC (Comput (P1,s1,k))) = P1 . (IC (Comput (P1,s1,k)))
.= halt SCMPDS by A22, A23 ;
I is_closed_on Comput (P1,s1,k),P1 by A14, A15, SCMPDS_6:def 2, A5;
then NPP (Result (P1,(Comput (P1,s1,k)))) = NPP (Result (P2,s2)) by A9, A21, A14, A20, Th29, XX, A5;
hence NPP (Result (P1,s1)) = NPP (Result (P2,s2)) by A25, EXTPRO_1:9; :: thesis: verum