let k, n be Element of NAT ; :: thesis: for s being State of SCM
for a, b being Data-Location st IC (Comput (ProgramPart s),s,k) = n & s . n = SubFrom a,b holds
( IC (Comput (ProgramPart s),s,(k + 1)) = n + 1 & (Comput (ProgramPart s),s,(k + 1)) . a = ((Comput (ProgramPart s),s,k) . a) - ((Comput (ProgramPart s),s,k) . b) & ( for d being Data-Location st d <> a holds
(Comput (ProgramPart s),s,(k + 1)) . d = (Comput (ProgramPart s),s,k) . d ) )
let s be State of SCM ; :: thesis: for a, b being Data-Location st IC (Comput (ProgramPart s),s,k) = n & s . n = SubFrom a,b holds
( IC (Comput (ProgramPart s),s,(k + 1)) = n + 1 & (Comput (ProgramPart s),s,(k + 1)) . a = ((Comput (ProgramPart s),s,k) . a) - ((Comput (ProgramPart s),s,k) . b) & ( for d being Data-Location st d <> a holds
(Comput (ProgramPart s),s,(k + 1)) . d = (Comput (ProgramPart s),s,k) . d ) )
let a, b be Data-Location ; :: thesis: ( IC (Comput (ProgramPart s),s,k) = n & s . n = SubFrom a,b implies ( IC (Comput (ProgramPart s),s,(k + 1)) = n + 1 & (Comput (ProgramPart s),s,(k + 1)) . a = ((Comput (ProgramPart s),s,k) . a) - ((Comput (ProgramPart s),s,k) . b) & ( for d being Data-Location st d <> a holds
(Comput (ProgramPart s),s,(k + 1)) . d = (Comput (ProgramPart s),s,k) . d ) ) )
assume A1: IC (Comput (ProgramPart s),s,k) = n ; :: thesis: ( not s . n = SubFrom a,b or ( IC (Comput (ProgramPart s),s,(k + 1)) = n + 1 & (Comput (ProgramPart s),s,(k + 1)) . a = ((Comput (ProgramPart s),s,k) . a) - ((Comput (ProgramPart s),s,k) . b) & ( for d being Data-Location st d <> a 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;
assume A2: s . n = SubFrom a,b ; :: thesis: ( IC (Comput (ProgramPart s),s,(k + 1)) = n + 1 & (Comput (ProgramPart s),s,(k + 1)) . a = ((Comput (ProgramPart s),s,k) . a) - ((Comput (ProgramPart s),s,k) . b) & ( for d being Data-Location st d <> a holds
(Comput (ProgramPart s),s,(k + 1)) . d = (Comput (ProgramPart s),s,k) . d ) )
then Comput (ProgramPart s),s,(k + 1) = Exec (SubFrom a,b),(Comput (ProgramPart s),s,k) by A1, Lm4;
hence ( IC (Comput (ProgramPart s),s,(k + 1)) = n + 1 & (Comput (ProgramPart s),s,(k + 1)) . a = ((Comput (ProgramPart s),s,k) . a) - ((Comput (ProgramPart s),s,k) . b) & ( for d being Data-Location st d <> a holds
(Comput (ProgramPart s),s,(k + 1)) . d = (Comput (ProgramPart s),s,k) . d ) ) by A1, A2, Lm4, AMI_3:10; :: thesis: verum