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

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