let k, n be Element of NAT ; :: thesis: for s being State of
for a, b being Data-Location st IC (Computation s,k) = il. n & s . (il. n) = Divide a,b & a <> b holds
( IC (Computation s,(k + 1)) = il. (n + 1) & (Computation s,(k + 1)) . a = ((Computation s,k) . a) div ((Computation s,k) . b) & (Computation s,(k + 1)) . b = ((Computation s,k) . a) mod ((Computation s,k) . b) & ( for d being Data-Location st d <> a & d <> b holds
(Computation s,(k + 1)) . d = (Computation s,k) . d ) )
let s be State of ; :: thesis: for a, b being Data-Location st IC (Computation s,k) = il. n & s . (il. n) = Divide a,b & a <> b holds
( IC (Computation s,(k + 1)) = il. (n + 1) & (Computation s,(k + 1)) . a = ((Computation s,k) . a) div ((Computation s,k) . b) & (Computation s,(k + 1)) . b = ((Computation s,k) . a) mod ((Computation s,k) . b) & ( for d being Data-Location st d <> a & d <> b holds
(Computation s,(k + 1)) . d = (Computation s,k) . d ) )
let a, b be Data-Location ; :: thesis: ( IC (Computation s,k) = il. n & s . (il. n) = Divide a,b & a <> b implies ( IC (Computation s,(k + 1)) = il. (n + 1) & (Computation s,(k + 1)) . a = ((Computation s,k) . a) div ((Computation s,k) . b) & (Computation s,(k + 1)) . b = ((Computation s,k) . a) mod ((Computation s,k) . b) & ( for d being Data-Location st d <> a & d <> b holds
(Computation s,(k + 1)) . d = (Computation s,k) . d ) ) )
assume A1: IC (Computation s,k) = il. n ; :: thesis: ( not s . (il. n) = Divide a,b or not a <> b or ( IC (Computation s,(k + 1)) = il. (n + 1) & (Computation s,(k + 1)) . a = ((Computation s,k) . a) div ((Computation s,k) . b) & (Computation s,(k + 1)) . b = ((Computation s,k) . a) mod ((Computation s,k) . b) & ( for d being Data-Location st d <> a & d <> b holds
(Computation s,(k + 1)) . d = (Computation s,k) . d ) ) )
set csk1 = Computation s,(k + 1);
set csk = Computation s,k;
assume A2: ( s . (il. n) = Divide a,b & a <> b ) ; :: thesis: ( IC (Computation s,(k + 1)) = il. (n + 1) & (Computation s,(k + 1)) . a = ((Computation s,k) . a) div ((Computation s,k) . b) & (Computation s,(k + 1)) . b = ((Computation s,k) . a) mod ((Computation s,k) . b) & ( for d being Data-Location st d <> a & d <> b holds
(Computation s,(k + 1)) . d = (Computation s,k) . d ) )
then Computation s,(k + 1) = Exec (Divide a,b),(Computation s,k) by A1, Lm4;
hence ( IC (Computation s,(k + 1)) = il. (n + 1) & (Computation s,(k + 1)) . a = ((Computation s,k) . a) div ((Computation s,k) . b) & (Computation s,(k + 1)) . b = ((Computation s,k) . a) mod ((Computation s,k) . b) & ( for d being Data-Location st d <> a & d <> b holds
(Computation s,(k + 1)) . d = (Computation s,k) . d ) ) by A1, A2, Lm4, AMI_3:12; :: thesis: verum