let F be NAT -defined the Instructions of SCM -valued total Function; :: thesis:
assume Z: Fusc_Program c= F ; :: thesis:
defpred S₁[ Nat] means for N, A, B being Element of NAT
for s being 0 -started State-consisting of 0 ,((<*2*> ^ <*$1*>) ^ <*A*>) ^ <*B*> st N > 0 & Fusc N = (A * (Fusc $1)) + (B * (Fusc ($1 + 1))) holds
( F halts_on s & (Result (F,s)) . (dl. 3) = Fusc N & ( $1 = 0 implies LifeSpan (F,s) = 1 ) & ( $1 > 0 implies LifeSpan (F,s) = (6 * ([\(log (2,$1))/] + 1)) + 1 ) );
A1: for k being Nat st ( for n being Nat st n < k holds
S₁[n] ) holds
S₁[k]

proof

set c2 = dl. 0;
set n = dl. 1;
set a = dl. 2;
set b = dl. 3;
set aux = dl. 4;
let nn be Nat; :: thesis:
assume A2: for n9 being Nat st n9 < nn holds
for N, A, B being Element of NAT
for s being 0 -started State-consisting of 0 ,((<*2*> ^ <*n9*>) ^ <*A*>) ^ <*B*> st N > 0 & Fusc N = (A * (Fusc n9)) + (B * (Fusc (n9 + 1))) holds
( F halts_on s & (Result (F,s)) . (dl. 3) = Fusc N & ( n9 = 0 implies LifeSpan (F,s) = 1 ) & ( n9 > 0 implies LifeSpan (F,s) = (6 * ([\(log (2,n9))/] + 1)) + 1 ) ) ; :: thesis:
reconsider n2 = nn as Element of NAT by ORDINAL1:def 13;
let N, A, B be Element of NAT ; :: thesis:
let s be 0 -started State-consisting of 0 ,((<*2*> ^ <*nn*>) ^ <*A*>) ^ <*B*>; :: thesis:
assume that
A3: N > 0 and
A4: Fusc N = (A * (Fusc nn)) + (B * (Fusc (nn + 1))) ; :: thesis:
A5: s . (dl. 1) = nn by SCM_1:13;
set s0 = Comput (F,s,0);
A6: F . 0 = (dl. 1) =0_goto 8 by Z, L14;
set s1 = Comput (F,s,(0 + 1));
A7: F . 8 = halt SCM by Z, L14;
A8: F . 3 = (dl. 4) =0_goto 6 by Z, L14;
A9: ( IC s = 0 & s = Comput (F,s,0) ) by COMPOS_1:def 20, EXTPRO_1:3;
s . (dl. 2) = A by SCM_1:13;
then A10: (Comput (F,s,(0 + 1))) . (dl. 2) = A by A6, A9, SCM_1:24;
s . (dl. 0) = 2 by SCM_1:13;
then A11: (Comput (F,s,(0 + 1))) . (dl. 0) = 2 by A6, A9, SCM_1:24;
A12: F . 2 = Divide ((dl. 1),(dl. 4)) by Z, L14;
s . (dl. 3) = B by SCM_1:13;
then A13: (Comput (F,s,(0 + 1))) . (dl. 3) = B by A6, A9, SCM_1:24;

A14: now

assume A15: nn = 0 ; :: thesis:
then A16: F . (IC (Comput (F,s,(0 + 1)))) = halt SCM by A6, A7, A5, A9, SCM_1:24;
hence F halts_on s by EXTPRO_1:31; :: thesis:
thus (Result (F,s)) . (dl. 3) = (Comput (F,s,(0 + 1))) . (dl. 3) by A16, EXTPRO_1:32
.= Fusc N by A4, A13, A15, PRE_FF:20 ; :: thesis:

hereby :: thesis:

assume nn = 0 ; :: thesis:
halt SCM <> (dl. 1) =0_goto 8 by SCM_1:26;
hence LifeSpan (F,s) = 1 by A6, A9, A16, EXTPRO_1:34; :: thesis:

end;

thus ( nn > 0 implies LifeSpan (F,s) = (6 * ([\(log (2,nn))/] + 1)) + 1 ) by A15; :: thesis:

end;

A17: F . 1 = (dl. 4) := (dl. 0) by Z, L14;
A18: F . 5 = SCM-goto 0 by Z, L14;
A19: F . 4 = AddTo ((dl. 3),(dl. 2)) by Z, L14;
A20: F . 7 = SCM-goto 0 by Z, L14;
A21: F . 6 = AddTo ((dl. 2),(dl. 3)) by Z, L14;
A22: (Comput (F,s,(0 + 1))) . (dl. 1) = nn by A6, A5, A9, SCM_1:24;

A23: now

set s6 = Comput (F,s,(5 + 1));
set s5 = Comput (F,s,(4 + 1));
set s4 = Comput (F,s,(3 + 1));
set s3 = Comput (F,s,(2 + 1));
set s2 = Comput (F,s,(1 + 1));
A24: nn mod 2 = nn - ((nn div 2) * 2) by INT_1:def 8;
assume A25: nn > 0 ; :: thesis:
then A26: IC (Comput (F,s,(0 + 1))) = 0 + 1 by A6, A5, A9, SCM_1:24;
then A27: IC (Comput (F,s,(1 + 1))) = 1 + 1 by A17, SCM_1:18;
then A28: IC (Comput (F,s,(2 + 1))) = 2 + 1 by A12, Lm14, SCM_1:22;
(Comput (F,s,(1 + 1))) . (dl. 2) = A by A17, A10, A26, Lm15, SCM_1:18;
then A29: (Comput (F,s,(2 + 1))) . (dl. 2) = A by A12, A27, Lm10, Lm14, Lm15, SCM_1:22;
(Comput (F,s,(1 + 1))) . (dl. 0) = 2 by A17, A11, A26, Lm13, SCM_1:18;
then A30: (Comput (F,s,(2 + 1))) . (dl. 0) = 2 by A12, A27, Lm7, Lm13, Lm14, SCM_1:22;
(Comput (F,s,(1 + 1))) . (dl. 3) = B by A17, A13, A26, Lm16, SCM_1:18;
then A31: (Comput (F,s,(2 + 1))) . (dl. 3) = B by A12, A27, Lm11, Lm14, Lm16, SCM_1:22;
A32: ( (Comput (F,s,(1 + 1))) . (dl. 4) = 2 & (Comput (F,s,(1 + 1))) . (dl. 1) = nn ) by A17, A11, A22, A26, Lm14, SCM_1:18;
then A33: (Comput (F,s,(2 + 1))) . (dl. 1) = n2 div 2 by A12, A27, Lm14, SCM_1:22;
then reconsider nn9 = (Comput (F,s,(2 + 1))) . (dl. 1) as Element of NAT by PRE_FF:7;
A34: (Comput (F,s,(2 + 1))) . (dl. 4) = nn mod 2 by A12, A27, A32, Lm14, SCM_1:22;

per cases ) . (dl. 4) <> 0 or (Comput (F,s,(2 + 1))) . (dl. 4) = 0 ) ;

suppose A35: (Comput (F,s,(2 + 1))) . (dl. 4) <> 0 ; :: thesis:

then A36: IC (Comput (F,s,(3 + 1))) = 3 + 1 by A8, A28, SCM_1:24;
then A37: IC (Comput (F,s,(4 + 1))) = 4 + 1 by A19, SCM_1:19;
A38: (Comput (F,s,(3 + 1))) . (dl. 2) = A by A8, A28, A29, SCM_1:24;
then (Comput (F,s,(4 + 1))) . (dl. 2) = A by A19, A36, Lm12, SCM_1:19;
then A39: (Comput (F,s,(5 + 1))) . (dl. 2) = A by A18, A37, SCM_1:23;
(Comput (F,s,(3 + 1))) . (dl. 3) = B by A8, A28, A31, SCM_1:24;
then A40: (Comput (F,s,(4 + 1))) . (dl. 3) = B + A by A19, A36, A38, SCM_1:19;
A41: (Comput (F,s,(2 + 1))) . (dl. 4) = 1 by A34, A35, PRE_FF:6;
(Comput (F,s,(3 + 1))) . (dl. 1) = (Comput (F,s,(2 + 1))) . (dl. 1) by A8, A28, SCM_1:24;
then (Comput (F,s,(4 + 1))) . (dl. 1) = (Comput (F,s,(2 + 1))) . (dl. 1) by A19, A36, Lm11, SCM_1:19;
then A42: (Comput (F,s,(5 + 1))) . (dl. 1) = (Comput (F,s,(2 + 1))) . (dl. 1) by A18, A37, SCM_1:23;
(Comput (F,s,(3 + 1))) . (dl. 0) = 2 by A8, A28, A30, SCM_1:24;
then (Comput (F,s,(4 + 1))) . (dl. 0) = 2 by A19, A36, Lm9, SCM_1:19;
then A45: (Comput (F,s,(5 + 1))) . (dl. 0) = 2 by A18, A37, SCM_1:23;
( IC (Comput (F,s,(5 + 1))) = 0 & (Comput (F,s,(5 + 1))) . (dl. 3) = (Comput (F,s,(4 + 1))) . (dl. 3) ) by A18, A37, SCM_1:23;
then A49: Comput (F,s,(5 + 1)) is 0 -started State-consisting of 0 ,((<*2*> ^ <*nn9*>) ^ <*A*>) ^ <*(B + A)*> by A40, A45, A42, A39, COMPOS_1:def 20, SCM_1:30;
A50: (nn mod 2) + ((nn div 2) * 2) = nn by A24;
then A51: nn9 < nn by A33, A34, A41, PRE_FF:19;
A52: Fusc N = (A * (Fusc nn9)) + ((B + A) * (Fusc (nn9 + 1))) by A4, A33, A34, A41, A50, PRE_FF:21;
then A53: ( nn9 > 0 implies LifeSpan (F,(Comput (F,s,(5 + 1)))) = (6 * ([\(log (2,nn9))/] + 1)) + 1 ) by A2, A3, A49, A51;
A54: F halts_on Comput (F,s,(5 + 1)) by A2, A3, A49, A51, A52;
hence F halts_on s by EXTPRO_1:22; :: thesis:
(Result (F,(Comput (F,s,(5 + 1))))) . (dl. 3) = Fusc N by A2, A3, A49, A51, A52;
hence (Result (F,s)) . (dl. 3) = Fusc N by A54, EXTPRO_1:36; :: thesis:
thus ( nn = 0 implies LifeSpan (F,s) = 1 ) by A25; :: thesis:
A55: ( nn9 = 0 implies LifeSpan (F,(Comput (F,s,(5 + 1)))) = 1 ) by A2, A3, A33, A34, A24, A41, A49, A52;
thus ( nn > 0 implies LifeSpan (F,s) = (6 * ([\(log (2,nn))/] + 1)) + 1 ) :: thesis:

proof

assume nn > 0 ; :: thesis:

per cases ;

suppose nn9 = 0 ; :: thesis:

hence LifeSpan (F,s) = (6 * ([\(log (2,nn))/] + 1)) + 1 by A33, A34, A24, A41, A54, A55, Lm1, EXTPRO_1:35; :: thesis:

end;

suppose A56: nn9 <> 0 ; :: thesis:

then A57: nn9 > 0 by NAT_1:3;
then reconsider m = [\(log (2,nn9))/] as Element of NAT by Lm2;
(6 * (m + 1)) + 1 > 0 by A57, Lm2;
hence LifeSpan (F,s) = 6 + ((6 * (m + 1)) + 1) by A54, A53, A56, EXTPRO_1:35, NAT_1:3
.= (6 * ([\(log (2,nn))/] + 1)) + 1 by A33, A34, A41, A50, A57, Lm3 ;
:: thesis:

end;

suppose A58: (Comput (F,s,(2 + 1))) . (dl. 4) = 0 ; :: thesis:

then A59: IC (Comput (F,s,(3 + 1))) = 6 by A8, A28, SCM_1:24;
then A60: IC (Comput (F,s,(4 + 1))) = 6 + 1 by A21, SCM_1:19;
(Comput (F,s,(3 + 1))) . (dl. 0) = 2 by A8, A28, A30, SCM_1:24;
then (Comput (F,s,(4 + 1))) . (dl. 0) = 2 by A21, A59, Lm8, SCM_1:19;
then A61: (Comput (F,s,(5 + 1))) . (dl. 0) = 2 by A20, A60, SCM_1:23;
A63: (Comput (F,s,(3 + 1))) . (dl. 3) = B by A8, A28, A31, SCM_1:24;
then (Comput (F,s,(4 + 1))) . (dl. 3) = B by A21, A59, Lm12, SCM_1:19;
then A64: (Comput (F,s,(5 + 1))) . (dl. 3) = B by A20, A60, SCM_1:23;
(Comput (F,s,(3 + 1))) . (dl. 1) = (Comput (F,s,(2 + 1))) . (dl. 1) by A8, A28, SCM_1:24;
then (Comput (F,s,(4 + 1))) . (dl. 1) = (Comput (F,s,(2 + 1))) . (dl. 1) by A21, A59, Lm10, SCM_1:19;
then A65: (Comput (F,s,(5 + 1))) . (dl. 1) = (Comput (F,s,(2 + 1))) . (dl. 1) by A20, A60, SCM_1:23;
(Comput (F,s,(3 + 1))) . (dl. 2) = A by A8, A28, A29, SCM_1:24;
then A68: (Comput (F,s,(4 + 1))) . (dl. 2) = A + B by A21, A59, A63, SCM_1:19;
reconsider nn9 = (Comput (F,s,(2 + 1))) . (dl. 1) as Element of NAT by A33, PRE_FF:7;
( IC (Comput (F,s,(5 + 1))) = 0 & (Comput (F,s,(5 + 1))) . (dl. 2) = (Comput (F,s,(4 + 1))) . (dl. 2) ) by A20, A60, SCM_1:23;
then A71: Comput (F,s,(5 + 1)) is 0 -started State-consisting of 0 ,((<*2*> ^ <*nn9*>) ^ <*(A + B)*>) ^ <*B*> by A68, A61, A65, A64, COMPOS_1:def 20, SCM_1:30;
A72: ( nn9 < nn & Fusc N = ((A + B) * (Fusc nn9)) + (B * (Fusc (nn9 + 1))) ) by A4, A25, A33, A34, A24, A58, PRE_FF:18, PRE_FF:22;
then A73: F halts_on Comput (F,s,(5 + 1)) by A2, A3, A71;
hence F halts_on s by EXTPRO_1:22; :: thesis:
(Result (F,(Comput (F,s,(5 + 1))))) . (dl. 3) = Fusc N by A2, A3, A71, A72;
hence (Result (F,s)) . (dl. 3) = Fusc N by A73, EXTPRO_1:36; :: thesis:
thus ( nn = 0 implies LifeSpan (F,s) = 1 ) by A25; :: thesis:
A74: ( nn9 > 0 implies LifeSpan (F,(Comput (F,s,(5 + 1)))) = (6 * ([\(log (2,nn9))/] + 1)) + 1 ) by A2, A3, A71, A72;
thus ( nn > 0 implies LifeSpan (F,s) = (6 * ([\(log (2,nn))/] + 1)) + 1 ) :: thesis:

proof

assume nn > 0 ; :: thesis:

per cases ;

suppose nn9 = 0 ; :: thesis:

hence LifeSpan (F,s) = (6 * ([\(log (2,nn))/] + 1)) + 1 by A12, A25, A27, A32, A33, A24, A58, Lm14, SCM_1:22; :: thesis:

end;

suppose A75: nn9 <> 0 ; :: thesis:

then A76: nn9 > 0 by NAT_1:3;
then reconsider m = [\(log (2,nn9))/] as Element of NAT by Lm2;
(6 * (m + 1)) + 1 > 0 by A76, Lm2;
hence LifeSpan (F,s) = 6 + ((6 * (m + 1)) + 1) by A73, A74, A75, EXTPRO_1:35, NAT_1:3
.= (6 * ([\(log (2,nn))/] + 1)) + 1 by A33, A34, A24, A58, A76, Lm5 ;
:: thesis:

end;

nn >= 0 by NAT_1:2;
hence ( F halts_on s & (Result (F,s)) . (dl. 3) = Fusc N & ( nn = 0 implies LifeSpan (F,s) = 1 ) & ( nn > 0 implies LifeSpan (F,s) = (6 * ([\(log (2,nn))/] + 1)) + 1 ) ) by A14, A23, XXREAL_0:1; :: thesis:

end;

for n being Nat holds S₁[n] from NAT_1:sch 4(A1);
hence for n, N, A, B being Element of NAT
for s being 0 -started State-consisting of 0 ,((<*2*> ^ <*n*>) ^ <*A*>) ^ <*B*> st N > 0 & Fusc N = (A * (Fusc n)) + (B * (Fusc (n + 1))) holds
( F halts_on s & (Result (F,s)) . (dl. 3) = Fusc N & ( n = 0 implies LifeSpan (F,s) = 1 ) & ( n > 0 implies LifeSpan (F,s) = (6 * ([\(log (2,n))/] + 1)) + 1 ) ) ; :: thesis: