let s1, s2 be 0 -started State of SCMPDS; :: thesis: for I being parahalting Program of SCMPDS st stop I c= s1 & stop I c= s2 & s1,s2 equal_outside NAT holds
for k being Element of NAT holds
( Comput ((ProgramPart s1),s1,k), Comput ((ProgramPart s2),s2,k) equal_outside NAT & CurInstr ((ProgramPart s1),(Comput ((ProgramPart s1),s1,k))) = CurInstr ((ProgramPart s2),(Comput ((ProgramPart s2),s2,k))) )
let I be parahalting Program of SCMPDS; :: thesis: ( stop I c= s1 & stop I c= s2 & s1,s2 equal_outside NAT implies for k being Element of NAT holds
( Comput ((ProgramPart s1),s1,k), Comput ((ProgramPart s2),s2,k) equal_outside NAT & CurInstr ((ProgramPart s1),(Comput ((ProgramPart s1),s1,k))) = CurInstr ((ProgramPart s2),(Comput ((ProgramPart s2),s2,k))) ) )
set SI = stop I;
assume that
A1: stop I c= s1 and
A2: stop I c= s2 and
A3: s1,s2 equal_outside NAT ; :: thesis: for k being Element of NAT holds
( Comput ((ProgramPart s1),s1,k), Comput ((ProgramPart s2),s2,k) equal_outside NAT & CurInstr ((ProgramPart s1),(Comput ((ProgramPart s1),s1,k))) = CurInstr ((ProgramPart s2),(Comput ((ProgramPart s2),s2,k))) )

hereby :: thesis: verum

let k be Element of NAT ; :: thesis: ( Comput ((ProgramPart s1),s1,k), Comput ((ProgramPart s2),s2,k) equal_outside NAT & CurInstr ((ProgramPart s2),(Comput ((ProgramPart s2),s2,k))) = CurInstr ((ProgramPart s1),(Comput ((ProgramPart s1),s1,k))) )
A6: IC (Comput ((ProgramPart s1),s1,k)) in dom (stop I) by A1, SCMPDS_4:def 9;
A7: IC (Comput ((ProgramPart s2),s2,k)) in dom (stop I) by A2, SCMPDS_4:def 9;
for m being Element of NAT st m < k holds
IC (Comput ((ProgramPart s2),s2,m)) in dom (stop I) by A2, SCMPDS_4:def 9;
hence Comput ((ProgramPart s1),s1,k), Comput ((ProgramPart s2),s2,k) equal_outside NAT by A3, A1, A2, SCMPDS_4:67; :: thesis: CurInstr ((ProgramPart s2),(Comput ((ProgramPart s2),s2,k))) = CurInstr ((ProgramPart s1),(Comput ((ProgramPart s1),s1,k)))
then A8: IC (Comput ((ProgramPart s1),s1,k)) = IC (Comput ((ProgramPart s2),s2,k)) by COMPOS_1:24;
thus CurInstr ((ProgramPart s2),(Comput ((ProgramPart s2),s2,k))) = s2 . (IC (Comput ((ProgramPart s2),s2,k))) by COMPOS_1:38
.= (stop I) . (IC (Comput ((ProgramPart s2),s2,k))) by A2, A7, GRFUNC_1:8
.= s1 . (IC (Comput ((ProgramPart s1),s1,k))) by A1, A8, A6, GRFUNC_1:8
.= CurInstr ((ProgramPart s1),(Comput ((ProgramPart s1),s1,k))) by COMPOS_1:38 ; :: thesis: verum

end;