let m, n be Nat; :: thesis: for s being State of SCM
for P being Instruction-Sequence of SCM st IterativeAlgorithm (AddTo ((dl. m),(dl. n))) c= P holds
for k being Nat st IC (Comput (P,s,k)) = 2 holds
( IC (Comput (P,s,(k + 1))) = 3 & (Comput (P,s,(k + 1))) . (dl. m) = ((Comput (P,s,k)) . (dl. m)) + ((Comput (P,s,k)) . (dl. n)) & ( for j being Nat st j <> m holds
(Comput (P,s,(k + 1))) . (dl. j) = (Comput (P,s,k)) . (dl. j) ) )
let s be State of SCM; :: thesis: for P being Instruction-Sequence of SCM st IterativeAlgorithm (AddTo ((dl. m),(dl. n))) c= P holds
for k being Nat st IC (Comput (P,s,k)) = 2 holds
( IC (Comput (P,s,(k + 1))) = 3 & (Comput (P,s,(k + 1))) . (dl. m) = ((Comput (P,s,k)) . (dl. m)) + ((Comput (P,s,k)) . (dl. n)) & ( for j being Nat st j <> m holds
(Comput (P,s,(k + 1))) . (dl. j) = (Comput (P,s,k)) . (dl. j) ) )
let P be Instruction-Sequence of SCM; :: thesis: ( IterativeAlgorithm (AddTo ((dl. m),(dl. n))) c= P implies for k being Nat st IC (Comput (P,s,k)) = 2 holds
( IC (Comput (P,s,(k + 1))) = 3 & (Comput (P,s,(k + 1))) . (dl. m) = ((Comput (P,s,k)) . (dl. m)) + ((Comput (P,s,k)) . (dl. n)) & ( for j being Nat st j <> m holds
(Comput (P,s,(k + 1))) . (dl. j) = (Comput (P,s,k)) . (dl. j) ) ) )
set c = dl. m;
set b = dl. n;
assume A1: IterativeAlgorithm (AddTo ((dl. m),(dl. n))) c= P ; :: thesis: for k being Nat st IC (Comput (P,s,k)) = 2 holds
( IC (Comput (P,s,(k + 1))) = 3 & (Comput (P,s,(k + 1))) . (dl. m) = ((Comput (P,s,k)) . (dl. m)) + ((Comput (P,s,k)) . (dl. n)) & ( for j being Nat st j <> m holds
(Comput (P,s,(k + 1))) . (dl. j) = (Comput (P,s,k)) . (dl. j) ) )
let k be Nat; :: thesis: ( IC (Comput (P,s,k)) = 2 implies ( IC (Comput (P,s,(k + 1))) = 3 & (Comput (P,s,(k + 1))) . (dl. m) = ((Comput (P,s,k)) . (dl. m)) + ((Comput (P,s,k)) . (dl. n)) & ( for j being Nat st j <> m holds
(Comput (P,s,(k + 1))) . (dl. j) = (Comput (P,s,k)) . (dl. j) ) ) )
assume A2: IC (Comput (P,s,k)) = 2 ; :: thesis: ( IC (Comput (P,s,(k + 1))) = 3 & (Comput (P,s,(k + 1))) . (dl. m) = ((Comput (P,s,k)) . (dl. m)) + ((Comput (P,s,k)) . (dl. n)) & ( for j being Nat st j <> m holds
(Comput (P,s,(k + 1))) . (dl. j) = (Comput (P,s,k)) . (dl. j) ) )
A3: Comput (P,s,(k + 1)) = Exec ((P . (IC (Comput (P,s,k)))),(Comput (P,s,k))) by EXTPRO_1:6
.= Exec ((AddTo ((dl. m),(dl. n))),(Comput (P,s,k))) by A1, A2, Th8 ;
hence IC (Comput (P,s,(k + 1))) = (IC (Comput (P,s,k))) + 1 by AMI_3:3
.= 3 by A2 ;
:: thesis: ( (Comput (P,s,(k + 1))) . (dl. m) = ((Comput (P,s,k)) . (dl. m)) + ((Comput (P,s,k)) . (dl. n)) & ( for j being Nat st j <> m holds
(Comput (P,s,(k + 1))) . (dl. j) = (Comput (P,s,k)) . (dl. j) ) )
thus (Comput (P,s,(k + 1))) . (dl. m) = ((Comput (P,s,k)) . (dl. m)) + ((Comput (P,s,k)) . (dl. n)) by A3, AMI_3:3; :: thesis: for j being Nat st j <> m holds
(Comput (P,s,(k + 1))) . (dl. j) = (Comput (P,s,k)) . (dl. j)
thus for j being Nat st j <> m holds
(Comput (P,s,(k + 1))) . (dl. j) = (Comput (P,s,k)) . (dl. j) by A3, AMI_3:3, AMI_3:10; :: thesis: verum