let I be Instruction of SCM; :: thesis:
let A be Integer; :: thesis:
let N be Nat; :: thesis:
let P be Instruction-Sequence of SCM; :: thesis:
assume that
A1: IterativeAlgorithm I c= P and
A2: I is sequential and
A3: I is 0 -dl.constant ; :: thesis:
let s be 0 -started State-consisting of <%1,N,A%>; :: thesis:
A4: P . 1 = halt SCM by A1, Th8;
set s0 = Comput (P,s,0);
set s1 = Comput (P,s,(0 + 1));
set s2 = Comput (P,s,(1 + 1));
set s3 = Comput (P,s,(2 + 1));
set s4 = Comput (P,s,(3 + 1));
set s5 = Comput (P,s,(4 + 1));
assume that
A5: (Comput (P,s,2)) . (dl. 1) = (Comput (P,s,1)) . (dl. 1) and
A6: for k being Nat holds (Comput (P,s,((4 * k) + 6))) . (dl. 1) = (Comput (P,s,((4 * k) + 5))) . (dl. 1) ; :: thesis:
A7: IC (Comput (P,s,0)) = 0 by MEMSTR_0:def 12;
A8: (Comput (P,s,0)) . (dl. 1) = N by Th14;
A9: (Comput (P,s,0)) . (dl. 2) = A by Th14;
A10: (Comput (P,s,(0 + 1))) . (dl. 1) = (Comput (P,s,0)) . (dl. 1) by A1, A7, Th16;
A11: (Comput (P,s,(0 + 1))) . (dl. 2) = (Comput (P,s,0)) . (dl. 2) by A1, A7, Th16;

per cases by NAT_1:6;

suppose A12: N = 0 ; :: thesis:

then P . (IC (Comput (P,s,(0 + 1)))) = halt SCM by A4, A1, A7, A8, Th16;
hence P halts_on s by EXTPRO_1:30; :: thesis:
thus IC (Comput (P,s,0)) = 0 by MEMSTR_0:def 12; :: thesis:
thus (Comput (P,s,1)) . (dl. 2) = A by A9, A11; :: thesis:
thus ( ( for k being Nat st 0 < k & k < N holds
IC (Comput (P,s,(4 * k))) = 5 ) & ( for k being Nat st k < N holds
( IC (Comput (P,s,((4 * k) + 1))) = 2 & IC (Comput (P,s,((4 * k) + 2))) = 3 & IC (Comput (P,s,((4 * k) + 3))) = 4 & (Comput (P,s,((4 * k) + 1))) . (dl. 1) = N - k & (Comput (P,s,((4 * k) + 2))) . (dl. 1) = N - k & (Comput (P,s,((4 * k) + 3))) . (dl. 1) = (N - k) - 1 & (Comput (P,s,((4 * k) + 4))) . (dl. 1) = (N - k) - 1 & (Comput (P,s,(4 * k))) . (dl. 1) > 0 & (Comput (P,s,((4 * k) + 1))) . (dl. 1) > 0 & (Comput (P,s,((4 * k) + 2))) . (dl. 1) > 0 ) ) & ( N <> 0 implies ( LifeSpan (P,s) = 4 * N & ( for k, j being Nat st k >= N holds
( IC (Comput (P,s,((4 * k) + j))) = 1 & (Comput (P,s,(((4 * k) + 1) + j))) . (dl. 1) = 0 ) ) ) ) ) by A12; :: thesis:

end;

suppose ex K being Nat st N = K + 1 ; :: thesis:

then consider K being Nat such that
A13: N = K + 1 ;
A14: IC (Comput (P,s,(0 + 1))) = 2 by A1, A7, A8, A13, Th16;
A15: dom (IterativeAlgorithm I) = {0,1,2,3,4,5} by Th6;
A16: dom (IterativeAlgorithm I) c= dom P by A1, GRFUNC_1:2;
A17: IC (Comput (P,s,(0 + 1))) in dom P by A14, A15, A16, Lm1;
CurInstr (P,(Comput (P,s,(0 + 1)))) = P . (IC (Comput (P,s,(0 + 1)))) by A17, PARTFUN1:def 6
.= I by A1, A14, Th8 ;
then A18: IC (Comput (P,s,(1 + 1))) = 2 + 1 by A14, A2, A17, Th13;
A19: (Comput (P,s,(1 + 1))) . (dl. 0) = 1 by A1, A2, A3, Th26;
A20: IC (Comput (P,s,(2 + 1))) = 4 by A1, A18, Th22;
A21: (Comput (P,s,(2 + 1))) . (dl. 1) = ((Comput (P,s,(1 + 1))) . (dl. 1)) - ((Comput (P,s,(1 + 1))) . (dl. 0)) by A1, A18, Th22;
A22: (Comput (P,s,(3 + 1))) . (dl. 1) = (Comput (P,s,(2 + 1))) . (dl. 1) by A1, A20, Th23;
defpred S₁[ Nat] means ( ( $1 < N implies ( ( for u being State of SCM st u = Comput (P,s,((4 * $1) + 3)) holds
( u . (dl. 1) = (N - $1) - 1 & IC u = 4 ) ) & IC (Comput (P,s,((4 * $1) + 1))) = 2 & IC (Comput (P,s,((4 * $1) + 2))) = 3 & ( 0 < $1 implies IC (Comput (P,s,(4 * $1))) = 5 ) & (Comput (P,s,(4 * $1))) . (dl. 1) > 0 & (Comput (P,s,((4 * $1) + 1))) . (dl. 1) > 0 & (Comput (P,s,((4 * $1) + 2))) . (dl. 1) > 0 & (Comput (P,s,((4 * $1) + 1))) . (dl. 1) = N - $1 & (Comput (P,s,((4 * $1) + 2))) . (dl. 1) = N - $1 & (Comput (P,s,((4 * $1) + 4))) . (dl. 1) = (N - $1) - 1 ) ) & ( N <> 0 implies for j being Nat st $1 >= N holds
(Comput (P,s,(((4 * $1) + 1) + j))) . (dl. 1) = 0 ) & ( N <> 0 & $1 >= N implies for j being Nat holds IC (Comput (P,s,((4 * $1) + j))) = 1 ) );
A23: S₁[ 0 ]

proof

hereby :: thesis:

assume A24: 0 < N ; :: thesis:
thus A25: for u being State of SCM st u = Comput (P,s,((4 * 0) + 3)) holds
( u . (dl. 1) = (N - 0) - 1 & IC u = 4 ) by A8, A10, A19, A5, A20, A21; :: thesis:
thus IC (Comput (P,s,((4 * 0) + 1))) = 2 by A14; :: thesis:
thus IC (Comput (P,s,((4 * 0) + 2))) = 3 by A18; :: thesis:
thus ( 0 > 0 implies IC (Comput (P,s,(4 * 0))) = 5 ) ; :: thesis:
thus ( (Comput (P,s,(4 * 0))) . (dl. 1) > 0 & (Comput (P,s,((4 * 0) + 1))) . (dl. 1) > 0 & (Comput (P,s,((4 * 0) + 2))) . (dl. 1) > 0 ) by A8, A10, A5, A24; :: thesis:
thus (Comput (P,s,((4 * 0) + 1))) . (dl. 1) = N - 0 by A8, A10; :: thesis:
thus (Comput (P,s,((4 * 0) + 2))) . (dl. 1) = N - 0 by A8, A10, A5; :: thesis:
thus (Comput (P,s,((4 * 0) + 4))) . (dl. 1) = (N - 0) - 1 by A22, A25; :: thesis:

end;

thus ( N <> 0 implies for j being Nat st 0 >= N holds
(Comput (P,s,(((4 * 0) + 1) + j))) . (dl. 1) = 0 ) ; :: thesis:
thus ( N <> 0 & 0 >= N implies for j being Nat holds IC (Comput (P,s,((4 * 0) + j))) = 1 ) ; :: thesis:

end;

A26: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis:
assume A27: ( ( k < N implies ( ( for u being State of SCM st u = Comput (P,s,((4 * k) + 3)) holds
( u . (dl. 1) = (N - k) - 1 & IC u = 4 ) ) & IC (Comput (P,s,((4 * k) + 1))) = 2 & IC (Comput (P,s,((4 * k) + 2))) = 3 & ( 0 < k implies IC (Comput (P,s,(4 * k))) = 5 ) & (Comput (P,s,(4 * k))) . (dl. 1) > 0 & (Comput (P,s,((4 * k) + 1))) . (dl. 1) > 0 & (Comput (P,s,((4 * k) + 2))) . (dl. 1) > 0 & (Comput (P,s,((4 * k) + 1))) . (dl. 1) = N - k & (Comput (P,s,((4 * k) + 2))) . (dl. 1) = N - k & (Comput (P,s,((4 * k) + 4))) . (dl. 1) = (N - k) - 1 ) ) & ( N <> 0 implies for j being Nat st k >= N holds
(Comput (P,s,(((4 * k) + 1) + j))) . (dl. 1) = 0 ) & ( N <> 0 & k >= N implies for j being Nat holds IC (Comput (P,s,((4 * k) + j))) = 1 ) ) ; :: thesis:
set S = (4 * k) + 3;
set s3 = Comput (P,s,((4 * k) + 3));
set s4 = Comput (P,s,(((4 * k) + 3) + 1));
set s5 = Comput (P,s,((((4 * k) + 3) + 1) + 1));
set s6 = Comput (P,s,((((4 * k) + 3) + 2) + 1));
set s7 = Comput (P,s,((((4 * k) + 3) + 3) + 1));
set s8 = Comput (P,s,((((4 * k) + 3) + 4) + 1));

hereby :: thesis:

assume A28: k + 1 < N ; :: thesis:
A29: k < N by A28, XXREAL_0:2, NAT_1:16;
A30: N - (k + 1) > (k + 1) - (k + 1) by A28, XREAL_1:9;
A31: IC (Comput (P,s,((4 * k) + 3))) = 4 by A27, A29;
A32: (Comput (P,s,((4 * k) + 3))) . (dl. 1) = (N - k) - 1 by A27, A29;
then A33: IC (Comput (P,s,(((4 * k) + 3) + 1))) = 5 by A1, A30, A31, Th23;
then A34: IC (Comput (P,s,((((4 * k) + 3) + 1) + 1))) = 2 by A1, Th24;
A35: (Comput (P,s,(((4 * k) + 3) + 1))) . (dl. 1) = (Comput (P,s,((4 * k) + 3))) . (dl. 1) by A1, A31, Th23;
A36: (Comput (P,s,((((4 * k) + 3) + 1) + 1))) . (dl. 1) = (Comput (P,s,(((4 * k) + 3) + 1))) . (dl. 1) by A1, A33, Th24;
(Comput (P,s,((4 * k) + 6))) . (dl. 1) = (Comput (P,s,((4 * k) + 5))) . (dl. 1) by A6;
then A37: (Comput (P,s,((((4 * k) + 3) + 2) + 1))) . (dl. 1) = (Comput (P,s,((((4 * k) + 3) + 1) + 1))) . (dl. 1) ;
A38: IC (Comput (P,s,((((4 * k) + 3) + 1) + 1))) in dom P by A34, A15, A16, Lm1;
CurInstr (P,(Comput (P,s,((((4 * k) + 3) + 1) + 1)))) = P . (IC (Comput (P,s,((((4 * k) + 3) + 1) + 1)))) by A38, PARTFUN1:def 6
.= I by A1, A34, Th8 ;
then A39: IC (Comput (P,s,((((4 * k) + 3) + 2) + 1))) = 2 + 1 by A34, A2, A38, Th13;
A40: (Comput (P,s,((((4 * k) + 3) + 3) + 1))) . (dl. 1) = ((Comput (P,s,((((4 * k) + 3) + 2) + 1))) . (dl. 1)) - ((Comput (P,s,((((4 * k) + 3) + 2) + 1))) . (dl. 0)) by A1, A39, Th22;
A41: IC (Comput (P,s,((((4 * k) + 3) + 3) + 1))) = 4 by A1, A39, Th22;
then A42: (Comput (P,s,((((4 * k) + 3) + 4) + 1))) . (dl. 1) = (Comput (P,s,((((4 * k) + 3) + 3) + 1))) . (dl. 1) by A1, Th23;
(Comput (P,s,((((4 * k) + 3) + 2) + 1))) . (dl. 0) = 1 by A1, A2, A3, Th26;
hence A43: for u being State of SCM st u = Comput (P,s,((4 * (k + 1)) + 3)) holds
( u . (dl. 1) = (N - (k + 1)) - 1 & IC u = 4 ) by A32, A40, A41, A37, A36, A35; :: thesis:
thus IC (Comput (P,s,((4 * (k + 1)) + 1))) = 2 by A34; :: thesis:
thus IC (Comput (P,s,((4 * (k + 1)) + 2))) = 3 by A39; :: thesis:
thus ( 0 < k + 1 implies IC (Comput (P,s,(4 * (k + 1)))) = 5 ) by A33; :: thesis:
thus (Comput (P,s,(4 * (k + 1)))) . (dl. 1) > 0 by A30, A32, A35; :: thesis:
thus (Comput (P,s,((4 * (k + 1)) + 1))) . (dl. 1) > 0 by A30, A32, A35, A36; :: thesis:
thus (Comput (P,s,((4 * (k + 1)) + 2))) . (dl. 1) > 0 by A30, A32, A35, A36, A37; :: thesis:
thus (Comput (P,s,((4 * (k + 1)) + 1))) . (dl. 1) = N - (k + 1) by A32, A35, A36; :: thesis:
thus (Comput (P,s,((4 * (k + 1)) + 2))) . (dl. 1) = N - (k + 1) by A32, A35, A36, A37; :: thesis:
thus (Comput (P,s,((4 * (k + 1)) + 4))) . (dl. 1) = (N - (k + 1)) - 1 by A42, A43; :: thesis:

end;

hereby :: thesis:

assume A44: N <> 0 ; :: thesis:
let j be Nat; :: thesis:
assume k + 1 >= N ; :: thesis:

per cases by XXREAL_0:1;

suppose A45: N = k + 1 ; :: thesis:

then ( IC (Comput (P,s,((4 * k) + 3))) = 4 & (Comput (P,s,((4 * k) + 3))) . (dl. 1) = 0 ) by A27, NAT_1:16;
then IC (Comput (P,s,(((4 * k) + 3) + 1))) = 1 by A1, Th23;
then Comput (P,s,((4 * k) + 4)) = Comput (P,s,(((4 * k) + 4) + (1 + j))) by A1, Th18;
hence (Comput (P,s,(((4 * (k + 1)) + 1) + j))) . (dl. 1) = 0 by A27, A45, NAT_1:16; :: thesis:

end;

suppose N < k + 1 ; :: thesis:

then (Comput (P,s,(((4 * k) + 1) + (4 + j)))) . (dl. 1) = 0 by A27, A44, NAT_1:13;
hence (Comput (P,s,(((4 * (k + 1)) + 1) + j))) . (dl. 1) = 0 ; :: thesis:

end;

assume that
A46: N <> 0 and
A47: k + 1 >= N ; :: thesis:
let j be Nat; :: thesis:

per cases by A47, XXREAL_0:1;

suppose k + 1 > N ; :: thesis:

then IC (Comput (P,s,((4 * k) + (4 + j)))) = 1 by A27, A46, NAT_1:13;
hence IC (Comput (P,s,((4 * (k + 1)) + j))) = 1 ; :: thesis:

end;

suppose k + 1 = N ; :: thesis:

then ( IC (Comput (P,s,((4 * k) + 3))) = 4 & (Comput (P,s,((4 * k) + 3))) . (dl. 1) = 0 ) by A27, NAT_1:16;
then IC (Comput (P,s,(((4 * k) + 3) + 1))) = 1 by A1, Th23;
hence IC (Comput (P,s,((4 * (k + 1)) + j))) = 1 by A1, Th18; :: thesis:

end;

A48: for k being Nat holds S₁[k] from NAT_1:sch 2(A23, A26);
set t = Comput (P,s,((4 * K) + 3));
set t1 = Comput (P,s,(((4 * K) + 3) + 1));
A49: K < N by A13, NAT_1:13;
then A50: IC (Comput (P,s,((4 * K) + 3))) = 4 by A48;
(Comput (P,s,((4 * K) + 3))) . (dl. 1) = (N - K) - 1 by A48, A49
.= 0 by A13 ;
then A51: IC (Comput (P,s,(((4 * K) + 3) + 1))) = 1 by A1, A50, Th23;
hence P halts_on s by A4, EXTPRO_1:30; :: thesis:
thus IC (Comput (P,s,0)) = 0 by A7; :: thesis:
thus (Comput (P,s,1)) . (dl. 2) = A by A9, A11; :: thesis:
thus for k being Nat st 0 < k & k < N holds
IC (Comput (P,s,(4 * k))) = 5 by A48; :: thesis:
thus for k being Nat st k < N holds
( IC (Comput (P,s,((4 * k) + 1))) = 2 & IC (Comput (P,s,((4 * k) + 2))) = 3 & IC (Comput (P,s,((4 * k) + 3))) = 4 & (Comput (P,s,((4 * k) + 1))) . (dl. 1) = N - k & (Comput (P,s,((4 * k) + 2))) . (dl. 1) = N - k & (Comput (P,s,((4 * k) + 3))) . (dl. 1) = (N - k) - 1 & (Comput (P,s,((4 * k) + 4))) . (dl. 1) = (N - k) - 1 & (Comput (P,s,(4 * k))) . (dl. 1) > 0 & (Comput (P,s,((4 * k) + 1))) . (dl. 1) > 0 & (Comput (P,s,((4 * k) + 2))) . (dl. 1) > 0 ) by A48; :: thesis:
assume A52: N <> 0 ; :: thesis:
thus LifeSpan (P,s) = 4 * N by A4, A13, A50, A51, EXTPRO_1:33; :: thesis:
thus for k, j being Nat st k >= N holds
( IC (Comput (P,s,((4 * k) + j))) = 1 & (Comput (P,s,(((4 * k) + 1) + j))) . (dl. 1) = 0 ) by A48, A52; :: thesis:

end;