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 = Divide a,b & 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) div ((Comput (ProgramPart s),s,k) . b) & (Comput (ProgramPart s),s,(k + 1)) . b = ((Comput (ProgramPart s),s,k) . a) mod ((Comput (ProgramPart s),s,k) . b) & ( for d being Data-Location st d <> a & d <> b 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 = Divide a,b & 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) div ((Comput (ProgramPart s),s,k) . b) & (Comput (ProgramPart s),s,(k + 1)) . b = ((Comput (ProgramPart s),s,k) . a) mod ((Comput (ProgramPart s),s,k) . b) & ( for d being Data-Location st d <> a & d <> b 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 = Divide a,b & 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) div ((Comput (ProgramPart s),s,k) . b) & (Comput (ProgramPart s),s,(k + 1)) . b = ((Comput (ProgramPart s),s,k) . a) mod ((Comput (ProgramPart s),s,k) . b) & ( for d being Data-Location st d <> a & d <> b 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 = Divide a,b or not 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) div ((Comput (ProgramPart s),s,k) . b) & (Comput (ProgramPart s),s,(k + 1)) . b = ((Comput (ProgramPart s),s,k) . a) mod ((Comput (ProgramPart s),s,k) . b) & ( for d being Data-Location st d <> a & d <> b 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 = Divide a,b & 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) div ((Comput (ProgramPart s),s,k) . b) & (Comput (ProgramPart s),s,(k + 1)) . b = ((Comput (ProgramPart s),s,k) . a) mod ((Comput (ProgramPart s),s,k) . b) & ( for d being Data-Location st d <> a & d <> b holds
(Comput (ProgramPart s),s,(k + 1)) . d = (Comput (ProgramPart s),s,k) . d ) )
then Comput (ProgramPart s),s,(k + 1) = Exec (Divide 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) div ((Comput (ProgramPart s),s,k) . b) & (Comput (ProgramPart s),s,(k + 1)) . b = ((Comput (ProgramPart s),s,k) . a) mod ((Comput (ProgramPart s),s,k) . b) & ( for d being Data-Location st d <> a & d <> b holds
(Comput (ProgramPart s),s,(k + 1)) . d = (Comput (ProgramPart s),s,k) . d ) ) by A1, A2, Lm4, AMI_3:12; :: thesis: verum