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

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

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

end;

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