let P1, P2 be Instruction-Sequence of SCMPDS; :: thesis: for s being 0 -started State of SCMPDS
for I being Program of SCMPDS st I is_closed_on s,P1 & stop I c= P1 & stop I c= P2 holds
for k being Element of NAT holds
( Comput (P1,s,k) = Comput (P2,s,k) & CurInstr (P1,(Comput (P1,s,k))) = CurInstr (P2,(Comput (P2,s,k))) )
let s be 0 -started State of SCMPDS; :: thesis: for I being Program of SCMPDS st I is_closed_on s,P1 & stop I c= P1 & stop I c= P2 holds
for k being Element of NAT holds
( Comput (P1,s,k) = Comput (P2,s,k) & CurInstr (P1,(Comput (P1,s,k))) = CurInstr (P2,(Comput (P2,s,k))) )
let I be Program of SCMPDS; :: thesis: ( I is_closed_on s,P1 & stop I c= P1 & stop I c= P2 implies for k being Element of NAT holds
( Comput (P1,s,k) = Comput (P2,s,k) & CurInstr (P1,(Comput (P1,s,k))) = CurInstr (P2,(Comput (P2,s,k))) ) )
set iI = stop I;
assume that
A3: I is_closed_on s,P1 and
A4: stop I c= P1 and
A5: stop I c= P2 ; :: thesis: for k being Element of NAT holds
( Comput (P1,s,k) = Comput (P2,s,k) & CurInstr (P1,(Comput (P1,s,k))) = CurInstr (P2,(Comput (P2,s,k))) )
B4: Start-At (0,SCMPDS) c= s by MEMSTR_0:29;
A1: s = Initialize s by B4, FUNCT_4:98;
A7: P2 = P2 +* (stop I) by A5, FUNCT_4:98;
A8: DataPart s = DataPart s ;
P1 = P1 +* (stop I) by A4, FUNCT_4:98;
hence for k being Element of NAT holds
( Comput (P1,s,k) = Comput (P2,s,k) & CurInstr (P1,(Comput (P1,s,k))) = CurInstr (P2,(Comput (P2,s,k))) ) by A3, A7, A8, Th25, A1; :: thesis: verum