let i1, i2 be Integer; :: thesis:
let I be Instruction of SCM; :: thesis:
assume A1: ( I is sequential & I is 0 -dl.constant ) ; :: thesis:
let P be Instruction-Sequence of SCM; :: thesis:
assume A2: IterativeAlgorithm I c= P ; :: thesis:
let s be 0 -started State-consisting of <%i1,0,i2%>; :: thesis:
thus IC (Comput (P,s,0)) = 0 by MEMSTR_0:def 12; :: thesis:
set s0 = Comput (P,s,0);
set s1 = Comput (P,s,(0 + 1));
A3: IC (Comput (P,s,0)) = 0 by MEMSTR_0:def 12;
A4: (Comput (P,s,0)) . (dl. 1) = 0 by Th14;
A5: (Comput (P,s,0)) . (dl. 2) = i2 by Th14;
A6: IC (Comput (P,s,(0 + 1))) = 1 by A2, A3, A4, Th16;

hereby :: thesis:

let k be Nat; :: thesis:
assume k >= 1 ; :: thesis:
then reconsider z = k - 1 as Element of NAT by INT_1:3;
Comput (P,s,(1 + z)) = Comput (P,s,(0 + 1)) by A2, A6, Th18;
hence IC (Comput (P,s,k)) = 1 by A2, A3, A4, Th16; :: thesis:

end;

hereby :: thesis:

let k be Nat; :: thesis:
thus (Comput (P,s,k)) . (dl. 0) = i1 by A1, A2, Th26; :: thesis:

per cases by NAT_1:6;

suppose k = 0 ; :: thesis:

hence ( (Comput (P,s,k)) . (dl. 1) = 0 & (Comput (P,s,k)) . (dl. 2) = i2 ) by Th14; :: thesis:

end;

suppose ex z being Nat st k = z + 1 ; :: thesis:

then consider z being Nat such that
A7: k = z + 1 ;
( (Comput (P,s,(0 + 1))) . (dl. 1) = (Comput (P,s,0)) . (dl. 1) & (Comput (P,s,(0 + 1))) . (dl. 2) = (Comput (P,s,0)) . (dl. 2) ) by A2, A3, Th16;
hence ( (Comput (P,s,k)) . (dl. 1) = 0 & (Comput (P,s,k)) . (dl. 2) = i2 ) by A2, A4, A5, A6, A7, Th18; :: thesis:

end;

end;

end;

P . 1 = halt SCM by A2, Th8;
hence LifeSpan (P,s) = 1 by A3, A6, EXTPRO_1:33; :: thesis: