let k, n be Element of NAT ; :: thesis: for s being State of
for a being Data-Location
for il being Instruction-Location of SCM st IC (Computation s,k) = il. n & s . (il. n) = a >0_goto il holds
( ( (Computation s,k) . a > 0 implies IC (Computation s,(k + 1)) = il ) & ( (Computation s,k) . a <= 0 implies IC (Computation s,(k + 1)) = il. (n + 1) ) & ( for d being Data-Location holds (Computation s,(k + 1)) . d = (Computation s,k) . d ) )
let s be State of ; :: thesis: for a being Data-Location
for il being Instruction-Location of SCM st IC (Computation s,k) = il. n & s . (il. n) = a >0_goto il holds
( ( (Computation s,k) . a > 0 implies IC (Computation s,(k + 1)) = il ) & ( (Computation s,k) . a <= 0 implies IC (Computation s,(k + 1)) = il. (n + 1) ) & ( for d being Data-Location holds (Computation s,(k + 1)) . d = (Computation s,k) . d ) )
let a be Data-Location ; :: thesis: for il being Instruction-Location of SCM st IC (Computation s,k) = il. n & s . (il. n) = a >0_goto il holds
( ( (Computation s,k) . a > 0 implies IC (Computation s,(k + 1)) = il ) & ( (Computation s,k) . a <= 0 implies IC (Computation s,(k + 1)) = il. (n + 1) ) & ( 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) = a >0_goto il implies ( ( (Computation s,k) . a > 0 implies IC (Computation s,(k + 1)) = il ) & ( (Computation s,k) . a <= 0 implies IC (Computation s,(k + 1)) = il. (n + 1) ) & ( for d being Data-Location holds (Computation s,(k + 1)) . d = (Computation s,k) . d ) ) )
assume that
A1: IC (Computation s,k) = il. n and
A2: s . (il. n) = a >0_goto il ; :: thesis: ( ( (Computation s,k) . a > 0 implies IC (Computation s,(k + 1)) = il ) & ( (Computation s,k) . a <= 0 implies IC (Computation s,(k + 1)) = il. (n + 1) ) & ( 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;
A3: Computation s,(k + 1) = Exec (CurInstr (Computation s,k)),(Computation s,k) by Lm3
.= Exec (a >0_goto il),(Computation s,k) by A1, A2, AMI_1:54 ;
hence ( (Computation s,k) . a > 0 implies IC (Computation s,(k + 1)) = il ) by AMI_3:15; :: thesis: ( ( (Computation s,k) . a <= 0 implies IC (Computation s,(k + 1)) = il. (n + 1) ) & ( for d being Data-Location holds (Computation s,(k + 1)) . d = (Computation s,k) . d ) )

hereby :: thesis: for d being Data-Location holds (Computation s,(k + 1)) . d = (Computation s,k) . d

assume (Computation s,k) . a <= 0 ; :: thesis: IC (Computation s,(k + 1)) = il. (n + 1)
hence IC (Computation s,(k + 1)) = Next (il. n) by A1, A3, AMI_3:15
.= il. (n + 1) ;
:: thesis: verum

end;

thus for d being Data-Location holds (Computation s,(k + 1)) . d = (Computation s,k) . d by A3, AMI_3:15; :: thesis: verum