let s be State of SCM; :: thesis: for I being Instruction of SCM
for P being Instruction-Sequence of SCM st IterativeAlgorithm I c= P holds
for k being Nat st IC (Comput (P,s,k)) = 0 holds
( ( (Comput (P,s,k)) . (dl. 1) > 0 implies IC (Comput (P,s,(k + 1))) = 2 ) & ( (Comput (P,s,k)) . (dl. 1) <= 0 implies IC (Comput (P,s,(k + 1))) = 1 ) & ( for j being Nat holds (Comput (P,s,(k + 1))) . (dl. j) = (Comput (P,s,k)) . (dl. j) ) )
let I be Instruction of SCM; :: thesis: for P being Instruction-Sequence of SCM st IterativeAlgorithm I c= P holds
for k being Nat st IC (Comput (P,s,k)) = 0 holds
( ( (Comput (P,s,k)) . (dl. 1) > 0 implies IC (Comput (P,s,(k + 1))) = 2 ) & ( (Comput (P,s,k)) . (dl. 1) <= 0 implies IC (Comput (P,s,(k + 1))) = 1 ) & ( for j being Nat holds (Comput (P,s,(k + 1))) . (dl. j) = (Comput (P,s,k)) . (dl. j) ) )
let P be Instruction-Sequence of SCM; :: thesis: ( IterativeAlgorithm I c= P implies for k being Nat st IC (Comput (P,s,k)) = 0 holds
( ( (Comput (P,s,k)) . (dl. 1) > 0 implies IC (Comput (P,s,(k + 1))) = 2 ) & ( (Comput (P,s,k)) . (dl. 1) <= 0 implies IC (Comput (P,s,(k + 1))) = 1 ) & ( for j being Nat holds (Comput (P,s,(k + 1))) . (dl. j) = (Comput (P,s,k)) . (dl. j) ) ) )
assume A1: IterativeAlgorithm I c= P ; :: thesis: for k being Nat st IC (Comput (P,s,k)) = 0 holds
( ( (Comput (P,s,k)) . (dl. 1) > 0 implies IC (Comput (P,s,(k + 1))) = 2 ) & ( (Comput (P,s,k)) . (dl. 1) <= 0 implies IC (Comput (P,s,(k + 1))) = 1 ) & ( for j being Nat holds (Comput (P,s,(k + 1))) . (dl. j) = (Comput (P,s,k)) . (dl. j) ) )
let k be Nat; :: thesis: ( IC (Comput (P,s,k)) = 0 implies ( ( (Comput (P,s,k)) . (dl. 1) > 0 implies IC (Comput (P,s,(k + 1))) = 2 ) & ( (Comput (P,s,k)) . (dl. 1) <= 0 implies IC (Comput (P,s,(k + 1))) = 1 ) & ( for j being Nat holds (Comput (P,s,(k + 1))) . (dl. j) = (Comput (P,s,k)) . (dl. j) ) ) )
assume A2: IC (Comput (P,s,k)) = 0 ; :: thesis: ( ( (Comput (P,s,k)) . (dl. 1) > 0 implies IC (Comput (P,s,(k + 1))) = 2 ) & ( (Comput (P,s,k)) . (dl. 1) <= 0 implies IC (Comput (P,s,(k + 1))) = 1 ) & ( for j being Nat 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 (((dl. 1) >0_goto 2),(Comput (P,s,k))) by A1, A2, Th8 ;
hence ( (Comput (P,s,k)) . (dl. 1) > 0 implies IC (Comput (P,s,(k + 1))) = 2 ) by AMI_3:9; :: thesis: ( ( (Comput (P,s,k)) . (dl. 1) <= 0 implies IC (Comput (P,s,(k + 1))) = 1 ) & ( for j being Nat holds (Comput (P,s,(k + 1))) . (dl. j) = (Comput (P,s,k)) . (dl. j) ) )
thus ( (Comput (P,s,k)) . (dl. 1) <= 0 implies IC (Comput (P,s,(k + 1))) = 1 ) :: thesis: for j being Nat holds (Comput (P,s,(k + 1))) . (dl. j) = (Comput (P,s,k)) . (dl. j)

proof

assume (Comput (P,s,k)) . (dl. 1) <= 0 ; :: thesis: IC (Comput (P,s,(k + 1))) = 1
hence IC (Comput (P,s,(k + 1))) = (IC (Comput (P,s,k))) + 1 by A3, AMI_3:9
.= 1 by A2 ;
:: thesis: verum

end;

thus for j being Nat holds (Comput (P,s,(k + 1))) . (dl. j) = (Comput (P,s,k)) . (dl. j) by A3, AMI_3:9; :: thesis: verum