let F be NAT -defined the InstructionsF of SCM -valued total Function; for k, n being Element of NAT
for s being State of SCM
for a, b being Data-Location st IC (Comput (F,s,k)) = n & F . n = SubFrom (a,b) holds
( IC (Comput (F,s,(k + 1))) = n + 1 & (Comput (F,s,(k + 1))) . a = ((Comput (F,s,k)) . a) - ((Comput (F,s,k)) . b) & ( for d being Data-Location st d <> a holds
(Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) )
let k, n be Element of NAT ; for s being State of SCM
for a, b being Data-Location st IC (Comput (F,s,k)) = n & F . n = SubFrom (a,b) holds
( IC (Comput (F,s,(k + 1))) = n + 1 & (Comput (F,s,(k + 1))) . a = ((Comput (F,s,k)) . a) - ((Comput (F,s,k)) . b) & ( for d being Data-Location st d <> a holds
(Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) )
let s be State of SCM; for a, b being Data-Location st IC (Comput (F,s,k)) = n & F . n = SubFrom (a,b) holds
( IC (Comput (F,s,(k + 1))) = n + 1 & (Comput (F,s,(k + 1))) . a = ((Comput (F,s,k)) . a) - ((Comput (F,s,k)) . b) & ( for d being Data-Location st d <> a holds
(Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) )
let a, b be Data-Location; ( IC (Comput (F,s,k)) = n & F . n = SubFrom (a,b) implies ( IC (Comput (F,s,(k + 1))) = n + 1 & (Comput (F,s,(k + 1))) . a = ((Comput (F,s,k)) . a) - ((Comput (F,s,k)) . b) & ( for d being Data-Location st d <> a holds
(Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) ) )
assume A1:
IC (Comput (F,s,k)) = n
; ( not F . n = SubFrom (a,b) or ( IC (Comput (F,s,(k + 1))) = n + 1 & (Comput (F,s,(k + 1))) . a = ((Comput (F,s,k)) . a) - ((Comput (F,s,k)) . b) & ( for d being Data-Location st d <> a holds
(Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) ) )
assume
F . n = SubFrom (a,b)
; ( IC (Comput (F,s,(k + 1))) = n + 1 & (Comput (F,s,(k + 1))) . a = ((Comput (F,s,k)) . a) - ((Comput (F,s,k)) . b) & ( for d being Data-Location st d <> a holds
(Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) )
then
Comput (F,s,(k + 1)) = Exec ((SubFrom (a,b)),(Comput (F,s,k)))
by A1, Lm2;
hence
( IC (Comput (F,s,(k + 1))) = n + 1 & (Comput (F,s,(k + 1))) . a = ((Comput (F,s,k)) . a) - ((Comput (F,s,k)) . b) & ( for d being Data-Location st d <> a holds
(Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) )
by A1, AMI_3:4; verum