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: ( I = AddTo ((dl. 2),(dl. 1)) or I = SubFrom ((dl. 2),(dl. 1)) or I = MultBy ((dl. 2),(dl. 1)) ) and
A2: IterativeAlgorithm I c= P ; :: thesis:
let s be 0 -started State-consisting of <%1,N,A%>; :: thesis:
A3: P . 1 = halt SCM by A2, 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));
A4: IC (Comput (P,s,0)) = 0 by MEMSTR_0:def 12;
A5: (Comput (P,s,0)) . (dl. 0) = 1 by Th14;
A6: (Comput (P,s,0)) . (dl. 1) = N by Th14;
A7: (Comput (P,s,0)) . (dl. 2) = A by Th14;
A8: (Comput (P,s,(0 + 1))) . (dl. 0) = (Comput (P,s,0)) . (dl. 0) by A2, A4, Th16;
A9: (Comput (P,s,(0 + 1))) . (dl. 1) = (Comput (P,s,0)) . (dl. 1) by A2, A4, Th16;
A10: (Comput (P,s,(0 + 1))) . (dl. 2) = (Comput (P,s,0)) . (dl. 2) by A2, A4, Th16;

per cases by NAT_1:6;

suppose A11: N = 0 ; :: thesis:

then P . (IC (Comput (P,s,(0 + 1)))) = halt SCM by A3, A2, A4, A6, Th16;
hence P halts_on s by EXTPRO_1:30; :: thesis:
thus (Comput (P,s,1)) . (dl. 2) = A by A7, A10; :: 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 A11; :: thesis:

end;

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

then consider K being Nat such that
A12: N = K + 1 ;
A13: IC (Comput (P,s,(0 + 1))) = 2 by A2, A4, A6, A12, Th16;
A14: IC (Comput (P,s,(1 + 1))) = 3 by A1, A2, A13, Th19, Th20, Th21;
A15: (Comput (P,s,(1 + 1))) . (dl. 0) = (Comput (P,s,(0 + 1))) . (dl. 0) by A1, A2, A13, Th19, Th20, Th21;
A16: (Comput (P,s,(1 + 1))) . (dl. 1) = (Comput (P,s,(0 + 1))) . (dl. 1) by A1, A2, A13, Th19, Th20, Th21;
A17: IC (Comput (P,s,(2 + 1))) = 4 by A2, A14, Th22;
A18: (Comput (P,s,(2 + 1))) . (dl. 0) = (Comput (P,s,(1 + 1))) . (dl. 0) by A2, A14, Th22;
A19: (Comput (P,s,(2 + 1))) . (dl. 1) = ((Comput (P,s,(1 + 1))) . (dl. 1)) - ((Comput (P,s,(1 + 1))) . (dl. 0)) by A2, A14, Th22;
A20: (Comput (P,s,(3 + 1))) . (dl. 1) = (Comput (P,s,(2 + 1))) . (dl. 1) by A2, A17, 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. 0) = 1 & 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 ) );
A21: S₁[ 0 ]

proof

hereby :: thesis:

assume A22: 0 < N ; :: thesis:
thus A23: for u being State of SCM st u = Comput (P,s,((4 * 0) + 3)) holds
( u . (dl. 0) = 1 & u . (dl. 1) = (N - 0) - 1 & IC u = 4 ) by A5, A6, A8, A9, A15, A16, A17, A18, A19; :: thesis:
thus IC (Comput (P,s,((4 * 0) + 1))) = 2 by A13; :: thesis:
thus IC (Comput (P,s,((4 * 0) + 2))) = 3 by A14; :: 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 A6, A9, A16, A22; :: thesis:
thus (Comput (P,s,((4 * 0) + 1))) . (dl. 1) = N - 0 by A6, A9; :: thesis:
thus (Comput (P,s,((4 * 0) + 2))) . (dl. 1) = N - 0 by A6, A9, A16; :: thesis:
thus (Comput (P,s,((4 * 0) + 4))) . (dl. 1) = (N - 0) - 1 by A20, A23; :: 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;

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

proof

let k be Nat; :: thesis:
assume A25: ( ( k < N implies ( ( for u being State of SCM st u = Comput (P,s,((4 * k) + 3)) holds
( u . (dl. 0) = 1 & 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 A26: k + 1 < N ; :: thesis:
A27: k < N by A26, XXREAL_0:2, NAT_1:16;
A28: N - (k + 1) > (k + 1) - (k + 1) by A26, XREAL_1:9;
A29: (Comput (P,s,((4 * k) + 3))) . (dl. 0) = 1 by A25, A27;
A30: IC (Comput (P,s,((4 * k) + 3))) = 4 by A25, A27;
A31: (Comput (P,s,((4 * k) + 3))) . (dl. 1) = (N - k) - 1 by A25, A27;
then A32: IC (Comput (P,s,(((4 * k) + 3) + 1))) = 5 by A2, A28, A30, Th23;
then A33: IC (Comput (P,s,((((4 * k) + 3) + 1) + 1))) = 2 by A2, Th24;
A34: (Comput (P,s,(((4 * k) + 3) + 1))) . (dl. 0) = (Comput (P,s,((4 * k) + 3))) . (dl. 0) by A2, A30, Th23;
A35: (Comput (P,s,(((4 * k) + 3) + 1))) . (dl. 1) = (Comput (P,s,((4 * k) + 3))) . (dl. 1) by A2, A30, Th23;
A36: (Comput (P,s,((((4 * k) + 3) + 1) + 1))) . (dl. 1) = (Comput (P,s,(((4 * k) + 3) + 1))) . (dl. 1) by A2, A32, Th24;
A37: (Comput (P,s,((((4 * k) + 3) + 2) + 1))) . (dl. 1) = (Comput (P,s,((((4 * k) + 3) + 1) + 1))) . (dl. 1) by A1, A2, A33, Th19, Th20, Th21;
A38: IC (Comput (P,s,((((4 * k) + 3) + 2) + 1))) = 3 by A1, A2, A33, Th19, Th20, Th21;
A39: (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 A2, A38, Th22;
A40: IC (Comput (P,s,((((4 * k) + 3) + 3) + 1))) = 4 by A2, A38, Th22;
then A41: (Comput (P,s,((((4 * k) + 3) + 4) + 1))) . (dl. 1) = (Comput (P,s,((((4 * k) + 3) + 3) + 1))) . (dl. 1) by A2, Th23;
A42: (Comput (P,s,((((4 * k) + 3) + 1) + 1))) . (dl. 0) = (Comput (P,s,(((4 * k) + 3) + 1))) . (dl. 0) by A2, A32, Th24;
A43: (Comput (P,s,((((4 * k) + 3) + 2) + 1))) . (dl. 0) = (Comput (P,s,((((4 * k) + 3) + 1) + 1))) . (dl. 0) by A1, A2, A33, Th19, Th20, Th21;
A44: (Comput (P,s,((((4 * k) + 3) + 3) + 1))) . (dl. 0) = (Comput (P,s,((((4 * k) + 3) + 2) + 1))) . (dl. 0) by A2, A38, Th22;
thus A45: for u being State of SCM st u = Comput (P,s,((4 * (k + 1)) + 3)) holds
( u . (dl. 0) = 1 & u . (dl. 1) = (N - (k + 1)) - 1 & IC u = 4 ) by A29, A31, A34, A35, A36, A37, A39, A40, A42, A43, A44; :: thesis:
thus IC (Comput (P,s,((4 * (k + 1)) + 1))) = 2 by A33; :: thesis:
thus IC (Comput (P,s,((4 * (k + 1)) + 2))) = 3 by A38; :: thesis:
thus ( 0 < k + 1 implies IC (Comput (P,s,(4 * (k + 1)))) = 5 ) by A32; :: thesis:
thus (Comput (P,s,(4 * (k + 1)))) . (dl. 1) > 0 by A28, A31, A35; :: thesis:
thus (Comput (P,s,((4 * (k + 1)) + 1))) . (dl. 1) > 0 by A28, A31, A35, A36; :: thesis:
thus (Comput (P,s,((4 * (k + 1)) + 2))) . (dl. 1) > 0 by A28, A31, A35, A36, A37; :: thesis:
thus (Comput (P,s,((4 * (k + 1)) + 1))) . (dl. 1) = N - (k + 1) by A31, A35, A36; :: thesis:
thus (Comput (P,s,((4 * (k + 1)) + 2))) . (dl. 1) = N - (k + 1) by A31, A35, A36, A37; :: thesis:
thus (Comput (P,s,((4 * (k + 1)) + 4))) . (dl. 1) = (N - (k + 1)) - 1 by A41, A45; :: thesis:

end;

hereby :: thesis:

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

per cases by XXREAL_0:1;

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

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

end;

suppose N < k + 1 ; :: thesis:

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

end;

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

per cases by A49, XXREAL_0:1;

suppose k + 1 > N ; :: thesis:

then IC (Comput (P,s,((4 * k) + (4 + j)))) = 1 by A25, A48, 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 A25, NAT_1:16;
then IC (Comput (P,s,(((4 * k) + 3) + 1))) = 1 by A2, Th23;
hence IC (Comput (P,s,((4 * (k + 1)) + j))) = 1 by A2, Th18; :: thesis:

end;

A50: for k being Nat holds S₁[k] from NAT_1:sch 2(A21, A24);
set t = Comput (P,s,((4 * K) + 3));
set t1 = Comput (P,s,(((4 * K) + 3) + 1));
A51: K < N by A12, NAT_1:13;
then A52: IC (Comput (P,s,((4 * K) + 3))) = 4 by A50;
(Comput (P,s,((4 * K) + 3))) . (dl. 1) = (N - K) - 1 by A50, A51
.= 0 by A12 ;
then A53: IC (Comput (P,s,(((4 * K) + 3) + 1))) = 1 by A2, A52, Th23;
hence P halts_on s by A3, EXTPRO_1:30; :: thesis:
thus (Comput (P,s,1)) . (dl. 2) = A by A7, A10; :: thesis:
thus for k being Nat st 0 < k & k < N holds
IC (Comput (P,s,(4 * k))) = 5 by A50; :: 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 A50; :: thesis:
assume A54: N <> 0 ; :: thesis:
thus LifeSpan (P,s) = 4 * N by A3, A12, A52, A53, 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 A50, A54; :: thesis:

end;