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, j being Nat st IC (Comput (P,s,k)) = 1 holds
Comput (P,s,(k + j)) = Comput (P,s,k)
let I be Instruction of SCM; :: thesis: for P being Instruction-Sequence of SCM st IterativeAlgorithm I c= P holds
for k, j being Nat st IC (Comput (P,s,k)) = 1 holds
Comput (P,s,(k + j)) = Comput (P,s,k)
let P be Instruction-Sequence of SCM; :: thesis: ( IterativeAlgorithm I c= P implies for k, j being Nat st IC (Comput (P,s,k)) = 1 holds
Comput (P,s,(k + j)) = Comput (P,s,k) )
assume A1: IterativeAlgorithm I c= P ; :: thesis: for k, j being Nat st IC (Comput (P,s,k)) = 1 holds
Comput (P,s,(k + j)) = Comput (P,s,k)
let k, j be Nat; :: thesis: ( IC (Comput (P,s,k)) = 1 implies Comput (P,s,(k + j)) = Comput (P,s,k) )
assume IC (Comput (P,s,k)) = 1 ; :: thesis: Comput (P,s,(k + j)) = Comput (P,s,k)
then P halts_at IC (Comput (P,s,k)) by A1, Th17;
hence Comput (P,s,(k + j)) = Comput (P,s,k) by EXTPRO_1:20, NAT_1:11; :: thesis: verum