let P1, P2 be Instruction-Sequence of SCMPDS; :: thesis: for s being 0 -started State of SCMPDS
for I being Program of st I is_closed_on s,P1 & stop I c= P1 & stop I c= P2 holds
for k being 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 st I is_closed_on s,P1 & stop I c= P1 & stop I c= P2 holds
for k being 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 ; :: thesis: ( I is_closed_on s,P1 & stop I c= P1 & stop I c= P2 implies for k being 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
A1: I is_closed_on s,P1 and
A2: stop I c= P1 and
A3: stop I c= P2 ; :: thesis: for k being Nat holds
( Comput (P1,s,k) = Comput (P2,s,k) & CurInstr (P1,(Comput (P1,s,k))) = CurInstr (P2,(Comput (P2,s,k))) )

A4: Start-At (0,SCMPDS) c= s by MEMSTR_0:29;
A5: s = Initialize s by ;
A6: P2 = P2 +* (stop I) by ;
A7: DataPart s = DataPart s ;
P1 = P1 +* (stop I) by ;
hence for k being Nat holds
( Comput (P1,s,k) = Comput (P2,s,k) & CurInstr (P1,(Comput (P1,s,k))) = CurInstr (P2,(Comput (P2,s,k))) ) by A1, A6, A7, Th6, A5; :: thesis: verum