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) = MultBy a,b holds
( IC (Computation s,(k + 1)) = il. (n + 1) & (Computation s,(k + 1)) . a = ((Computation s,k) . a) * ((Computation s,k) . b) & ( for d being Data-Location st d <> a 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) = MultBy a,b holds
( IC (Computation s,(k + 1)) = il. (n + 1) & (Computation s,(k + 1)) . a = ((Computation s,k) . a) * ((Computation s,k) . b) & ( for d being Data-Location st d <> a 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) = MultBy a,b implies ( IC (Computation s,(k + 1)) = il. (n + 1) & (Computation s,(k + 1)) . a = ((Computation s,k) . a) * ((Computation s,k) . b) & ( for d being Data-Location st d <> a holds
(Computation s,(k + 1)) . d = (Computation s,k) . d ) ) )
assume A1: IC (Computation s,k) = il. n ; :: thesis: ( not s . (il. n) = MultBy a,b or ( IC (Computation s,(k + 1)) = il. (n + 1) & (Computation s,(k + 1)) . a = ((Computation s,k) . a) * ((Computation s,k) . b) & ( for d being Data-Location st d <> a 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) = MultBy a,b ; :: thesis: ( IC (Computation s,(k + 1)) = il. (n + 1) & (Computation s,(k + 1)) . a = ((Computation s,k) . a) * ((Computation s,k) . b) & ( for d being Data-Location st d <> a holds
(Computation s,(k + 1)) . d = (Computation s,k) . d ) )
then Computation s,(k + 1) = Exec (MultBy 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) * ((Computation s,k) . b) & ( for d being Data-Location st d <> a holds
(Computation s,(k + 1)) . d = (Computation s,k) . d ) ) by A1, A2, Lm4, AMI_3:11; :: thesis: verum