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 a, b being Data-Location st IC (Comput (F,s,k)) = n & F . n = Divide (a,b) & a <> b holds

( IC (Comput (F,s,(k + 1))) = n + 1 & (Comput (F,s,(k + 1))) . a = ((Comput (F,s,k)) . a) div ((Comput (F,s,k)) . b) & (Comput (F,s,(k + 1))) . b = ((Comput (F,s,k)) . a) mod ((Comput (F,s,k)) . b) & ( for d being Data-Location st d <> a & d <> b 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 a, b being Data-Location st IC (Comput (F,s,k)) = n & F . n = Divide (a,b) & a <> b holds

( IC (Comput (F,s,(k + 1))) = n + 1 & (Comput (F,s,(k + 1))) . a = ((Comput (F,s,k)) . a) div ((Comput (F,s,k)) . b) & (Comput (F,s,(k + 1))) . b = ((Comput (F,s,k)) . a) mod ((Comput (F,s,k)) . b) & ( for d being Data-Location st d <> a & d <> b holds

(Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) )

let s be State of SCM; :: thesis: for a, b being Data-Location st IC (Comput (F,s,k)) = n & F . n = Divide (a,b) & a <> b holds

( IC (Comput (F,s,(k + 1))) = n + 1 & (Comput (F,s,(k + 1))) . a = ((Comput (F,s,k)) . a) div ((Comput (F,s,k)) . b) & (Comput (F,s,(k + 1))) . b = ((Comput (F,s,k)) . a) mod ((Comput (F,s,k)) . b) & ( for d being Data-Location st d <> a & d <> b holds

(Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) )

let a, b be Data-Location; :: thesis: ( IC (Comput (F,s,k)) = n & F . n = Divide (a,b) & a <> b implies ( IC (Comput (F,s,(k + 1))) = n + 1 & (Comput (F,s,(k + 1))) . a = ((Comput (F,s,k)) . a) div ((Comput (F,s,k)) . b) & (Comput (F,s,(k + 1))) . b = ((Comput (F,s,k)) . a) mod ((Comput (F,s,k)) . b) & ( for d being Data-Location st d <> a & d <> b holds

(Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) ) )

assume A1: IC (Comput (F,s,k)) = n ; :: thesis: ( not F . n = Divide (a,b) or not a <> b or ( IC (Comput (F,s,(k + 1))) = n + 1 & (Comput (F,s,(k + 1))) . a = ((Comput (F,s,k)) . a) div ((Comput (F,s,k)) . b) & (Comput (F,s,(k + 1))) . b = ((Comput (F,s,k)) . a) mod ((Comput (F,s,k)) . b) & ( for d being Data-Location st d <> a & d <> b holds

(Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) ) )

assume A2: ( F . n = Divide (a,b) & a <> b ) ; :: thesis: ( IC (Comput (F,s,(k + 1))) = n + 1 & (Comput (F,s,(k + 1))) . a = ((Comput (F,s,k)) . a) div ((Comput (F,s,k)) . b) & (Comput (F,s,(k + 1))) . b = ((Comput (F,s,k)) . a) mod ((Comput (F,s,k)) . b) & ( for d being Data-Location st d <> a & d <> b holds

(Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) )

then Comput (F,s,(k + 1)) = Exec ((Divide (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) div ((Comput (F,s,k)) . b) & (Comput (F,s,(k + 1))) . b = ((Comput (F,s,k)) . a) mod ((Comput (F,s,k)) . b) & ( for d being Data-Location st d <> a & d <> b holds

(Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) ) by A1, A2, AMI_3:6; :: thesis: verum

for s being State of SCM

for a, b being Data-Location st IC (Comput (F,s,k)) = n & F . n = Divide (a,b) & a <> b holds

( IC (Comput (F,s,(k + 1))) = n + 1 & (Comput (F,s,(k + 1))) . a = ((Comput (F,s,k)) . a) div ((Comput (F,s,k)) . b) & (Comput (F,s,(k + 1))) . b = ((Comput (F,s,k)) . a) mod ((Comput (F,s,k)) . b) & ( for d being Data-Location st d <> a & d <> b 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 a, b being Data-Location st IC (Comput (F,s,k)) = n & F . n = Divide (a,b) & a <> b holds

( IC (Comput (F,s,(k + 1))) = n + 1 & (Comput (F,s,(k + 1))) . a = ((Comput (F,s,k)) . a) div ((Comput (F,s,k)) . b) & (Comput (F,s,(k + 1))) . b = ((Comput (F,s,k)) . a) mod ((Comput (F,s,k)) . b) & ( for d being Data-Location st d <> a & d <> b holds

(Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) )

let s be State of SCM; :: thesis: for a, b being Data-Location st IC (Comput (F,s,k)) = n & F . n = Divide (a,b) & a <> b holds

( IC (Comput (F,s,(k + 1))) = n + 1 & (Comput (F,s,(k + 1))) . a = ((Comput (F,s,k)) . a) div ((Comput (F,s,k)) . b) & (Comput (F,s,(k + 1))) . b = ((Comput (F,s,k)) . a) mod ((Comput (F,s,k)) . b) & ( for d being Data-Location st d <> a & d <> b holds

(Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) )

let a, b be Data-Location; :: thesis: ( IC (Comput (F,s,k)) = n & F . n = Divide (a,b) & a <> b implies ( IC (Comput (F,s,(k + 1))) = n + 1 & (Comput (F,s,(k + 1))) . a = ((Comput (F,s,k)) . a) div ((Comput (F,s,k)) . b) & (Comput (F,s,(k + 1))) . b = ((Comput (F,s,k)) . a) mod ((Comput (F,s,k)) . b) & ( for d being Data-Location st d <> a & d <> b holds

(Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) ) )

assume A1: IC (Comput (F,s,k)) = n ; :: thesis: ( not F . n = Divide (a,b) or not a <> b or ( IC (Comput (F,s,(k + 1))) = n + 1 & (Comput (F,s,(k + 1))) . a = ((Comput (F,s,k)) . a) div ((Comput (F,s,k)) . b) & (Comput (F,s,(k + 1))) . b = ((Comput (F,s,k)) . a) mod ((Comput (F,s,k)) . b) & ( for d being Data-Location st d <> a & d <> b holds

(Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) ) )

assume A2: ( F . n = Divide (a,b) & a <> b ) ; :: thesis: ( IC (Comput (F,s,(k + 1))) = n + 1 & (Comput (F,s,(k + 1))) . a = ((Comput (F,s,k)) . a) div ((Comput (F,s,k)) . b) & (Comput (F,s,(k + 1))) . b = ((Comput (F,s,k)) . a) mod ((Comput (F,s,k)) . b) & ( for d being Data-Location st d <> a & d <> b holds

(Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) )

then Comput (F,s,(k + 1)) = Exec ((Divide (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) div ((Comput (F,s,k)) . b) & (Comput (F,s,(k + 1))) . b = ((Comput (F,s,k)) . a) mod ((Comput (F,s,k)) . b) & ( for d being Data-Location st d <> a & d <> b holds

(Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) ) by A1, A2, AMI_3:6; :: thesis: verum