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