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 A4, FUNCT_4:98;
A6: P2 = P2 +* (stop I) by A3, FUNCT_4:98;
A7: DataPart s = DataPart s ;
P1 = P1 +* (stop I) by A2, FUNCT_4:98;
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