let k, n be Element of NAT ; :: thesis: for s being State of SCM
for il being Element of NAT st IC (Comput (ProgramPart s),s,k) = n & s . n = SCM-goto il holds
( IC (Comput (ProgramPart s),s,(k + 1)) = il & ( for d being Data-Location holds (Comput (ProgramPart s),s,(k + 1)) . d = (Comput (ProgramPart s),s,k) . d ) )
let s be State of SCM ; :: thesis: for il being Element of NAT st IC (Comput (ProgramPart s),s,k) = n & s . n = SCM-goto il holds
( IC (Comput (ProgramPart s),s,(k + 1)) = il & ( for d being Data-Location holds (Comput (ProgramPart s),s,(k + 1)) . d = (Comput (ProgramPart s),s,k) . d ) )
let il be Element of NAT ; :: thesis: ( IC (Comput (ProgramPart s),s,k) = n & s . n = SCM-goto il implies ( IC (Comput (ProgramPart s),s,(k + 1)) = il & ( for d being Data-Location holds (Comput (ProgramPart s),s,(k + 1)) . d = (Comput (ProgramPart s),s,k) . d ) ) )
assume A1: ( IC (Comput (ProgramPart s),s,k) = n & s . n = SCM-goto il ) ; :: thesis: ( IC (Comput (ProgramPart s),s,(k + 1)) = il & ( for d being Data-Location holds (Comput (ProgramPart s),s,(k + 1)) . d = (Comput (ProgramPart s),s,k) . d ) )
set csk1 = Comput (ProgramPart s),s,(k + 1);
set csk = Comput (ProgramPart s),s,k;
Y: (ProgramPart (Comput (ProgramPart s),s,k)) /. (IC (Comput (ProgramPart s),s,k)) = (Comput (ProgramPart s),s,k) . (IC (Comput (ProgramPart s),s,k)) by COMPOS_1:38;
A2: Comput (ProgramPart s),s,(k + 1) = Exec (CurInstr (ProgramPart (Comput (ProgramPart s),s,k)),(Comput (ProgramPart s),s,k)),(Comput (ProgramPart s),s,k) by Lm3
.= Exec (SCM-goto il),(Comput (ProgramPart s),s,k) by A1, Y, AMI_1:54 ;
hence IC (Comput (ProgramPart s),s,(k + 1)) = il by AMI_3:13; :: thesis: for d being Data-Location holds (Comput (ProgramPart s),s,(k + 1)) . d = (Comput (ProgramPart s),s,k) . d
thus for d being Data-Location holds (Comput (ProgramPart s),s,(k + 1)) . d = (Comput (ProgramPart s),s,k) . d by A2, AMI_3:13; :: thesis: verum