let F be NAT -defined the InstructionsF of SCM -valued total Function; :: thesis: for k, n being Element of NAT
for s being State of SCM
for il being Element of NAT st IC (Comput (F,s,k)) = n & F . n = SCM-goto il holds
( IC (Comput (F,s,(k + 1))) = il & ( for d being Data-Location holds (Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) )
let k, n be Element of NAT ; :: thesis: for s being State of SCM
for il being Element of NAT st IC (Comput (F,s,k)) = n & F . n = SCM-goto il holds
( IC (Comput (F,s,(k + 1))) = il & ( for d being Data-Location holds (Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) )
let s be State of SCM; :: thesis: for il being Element of NAT st IC (Comput (F,s,k)) = n & F . n = SCM-goto il holds
( IC (Comput (F,s,(k + 1))) = il & ( for d being Data-Location holds (Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) )
let il be Element of NAT ; :: thesis: ( IC (Comput (F,s,k)) = n & F . n = SCM-goto il implies ( IC (Comput (F,s,(k + 1))) = il & ( for d being Data-Location holds (Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) ) )
assume A1: ( IC (Comput (F,s,k)) = n & F . n = SCM-goto il ) ; :: thesis: ( IC (Comput (F,s,(k + 1))) = il & ( for d being Data-Location holds (Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) )
set csk1 = Comput (F,s,(k + 1));
set csk = Comput (F,s,k);
A2: dom F = NAT by PARTFUN1:def 2;
A3: Comput (F,s,(k + 1)) = Exec ((CurInstr (F,(Comput (F,s,k)))),(Comput (F,s,k))) by Lm1
.= Exec ((SCM-goto il),(Comput (F,s,k))) by A1, A2, PARTFUN1:def 6 ;
hence IC (Comput (F,s,(k + 1))) = il by AMI_3:7; :: thesis: for d being Data-Location holds (Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d
thus for d being Data-Location holds (Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d by A3, AMI_3:7; :: thesis: verum