let F be NAT -defined the InstructionsF of SCM -valued total Function; :: thesis:
assume A1: 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 <%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 ) );
A2: 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 A3: for n9 being Nat st n9 < nn holds
for N, A, B being Element of NAT
for s being 0 -started State-consisting of <%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 12;
let N, A, B be Element of NAT ; :: thesis:
let s be 0 -started State-consisting of <%2,nn,A,B%>; :: thesis:
assume that
A4: N > 0 and
A5: Fusc N = (A * (Fusc nn)) + (B * (Fusc (nn + 1))) ; :: thesis:
A6: s . (dl. 1) = nn by SCM_1:1;
set s0 = Comput (F,s,0);
A7: F . 0 = (dl. 1) =0_goto 8 by A1, Lm17;
set s1 = Comput (F,s,(0 + 1));
A8: F . 8 = halt SCM by A1, Lm17;
A9: F . 3 = (dl. 4) =0_goto 6 by A1, Lm17;
A10: ( IC s = 0 & s = Comput (F,s,0) ) by EXTPRO_1:2, MEMSTR_0:def 12;
s . (dl. 2) = A by SCM_1:1;
then A11: (Comput (F,s,(0 + 1))) . (dl. 2) = A by A7, A10, SCM_1:10;
s . (dl. 0) = 2 by SCM_1:1;
then A12: (Comput (F,s,(0 + 1))) . (dl. 0) = 2 by A7, A10, SCM_1:10;
A13: F . 2 = Divide ((dl. 1),(dl. 4)) by A1, Lm17;
s . (dl. 3) = B by SCM_1:1;
then A14: (Comput (F,s,(0 + 1))) . (dl. 3) = B by A7, A10, SCM_1:10;

A15: now :: thesis:

assume A16: nn = 0 ; :: thesis:
then A17: F . (IC (Comput (F,s,(0 + 1)))) = halt SCM by A7, A8, A6, A10, SCM_1:10;
hence F halts_on s by EXTPRO_1:30; :: thesis:
thus (Result (F,s)) . (dl. 3) = (Comput (F,s,(0 + 1))) . (dl. 3) by A17, EXTPRO_1:7
.= Fusc N by A5, A14, A16, PRE_FF:18 ; :: thesis:

hereby :: thesis:

assume nn = 0 ; :: thesis:
halt SCM <> (dl. 1) =0_goto 8 by SCM_1:12;
hence LifeSpan (F,s) = 1 by A7, A10, A17, EXTPRO_1:33; :: thesis:

end;

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

end;

A18: F . 1 = (dl. 4) := (dl. 0) by A1, Lm17;
A19: F . 5 = SCM-goto 0 by A1, Lm17;
A20: F . 4 = AddTo ((dl. 3),(dl. 2)) by A1, Lm17;
A21: F . 7 = SCM-goto 0 by A1, Lm17;
A22: F . 6 = AddTo ((dl. 2),(dl. 3)) by A1, Lm17;
A23: (Comput (F,s,(0 + 1))) . (dl. 1) = nn by A7, A6, A10, SCM_1:10;

A24: now :: thesis:

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));
A25: nn mod 2 = nn - ((nn div 2) * 2) by INT_1:def 10;
assume A26: nn > 0 ; :: thesis:
then A27: IC (Comput (F,s,(0 + 1))) = 0 + 1 by A7, A6, A10, SCM_1:10;
then A28: IC (Comput (F,s,(1 + 1))) = 1 + 1 by A18, SCM_1:4;
then A29: IC (Comput (F,s,(2 + 1))) = 2 + 1 by A13, Lm14, SCM_1:8;
(Comput (F,s,(1 + 1))) . (dl. 2) = A by A18, A11, A27, Lm15, SCM_1:4;
then A30: (Comput (F,s,(2 + 1))) . (dl. 2) = A by A13, A28, Lm10, Lm14, Lm15, SCM_1:8;
(Comput (F,s,(1 + 1))) . (dl. 0) = 2 by A18, A12, A27, Lm13, SCM_1:4;
then A31: (Comput (F,s,(2 + 1))) . (dl. 0) = 2 by A13, A28, Lm7, Lm13, Lm14, SCM_1:8;
(Comput (F,s,(1 + 1))) . (dl. 3) = B by A18, A14, A27, Lm16, SCM_1:4;
then A32: (Comput (F,s,(2 + 1))) . (dl. 3) = B by A13, A28, Lm11, Lm14, Lm16, SCM_1:8;
A33: ( (Comput (F,s,(1 + 1))) . (dl. 4) = 2 & (Comput (F,s,(1 + 1))) . (dl. 1) = nn ) by A18, A12, A23, A27, Lm14, SCM_1:4;
then A34: (Comput (F,s,(2 + 1))) . (dl. 1) = n2 div 2 by A13, A28, Lm14, SCM_1:8;
then reconsider nn9 = (Comput (F,s,(2 + 1))) . (dl. 1) as Element of NAT by PRE_FF:7;
A35: (Comput (F,s,(2 + 1))) . (dl. 4) = nn mod 2 by A13, A28, A33, Lm14, SCM_1:8;

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

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

then A37: IC (Comput (F,s,(3 + 1))) = 3 + 1 by A9, A29, SCM_1:10;
then A38: IC (Comput (F,s,(4 + 1))) = 4 + 1 by A20, SCM_1:5;
A39: (Comput (F,s,(3 + 1))) . (dl. 2) = A by A9, A29, A30, SCM_1:10;
then (Comput (F,s,(4 + 1))) . (dl. 2) = A by A20, A37, Lm12, SCM_1:5;
then A40: (Comput (F,s,(5 + 1))) . (dl. 2) = A by A19, A38, SCM_1:9;
(Comput (F,s,(3 + 1))) . (dl. 3) = B by A9, A29, A32, SCM_1:10;
then A41: (Comput (F,s,(4 + 1))) . (dl. 3) = B + A by A20, A37, A39, SCM_1:5;
A42: (Comput (F,s,(2 + 1))) . (dl. 4) = 1 by A35, A36, PRE_FF:6;
(Comput (F,s,(3 + 1))) . (dl. 1) = (Comput (F,s,(2 + 1))) . (dl. 1) by A9, A29, SCM_1:10;
then (Comput (F,s,(4 + 1))) . (dl. 1) = (Comput (F,s,(2 + 1))) . (dl. 1) by A20, A37, Lm11, SCM_1:5;
then A43: (Comput (F,s,(5 + 1))) . (dl. 1) = (Comput (F,s,(2 + 1))) . (dl. 1) by A19, A38, SCM_1:9;
(Comput (F,s,(3 + 1))) . (dl. 0) = 2 by A9, A29, A31, SCM_1:10;
then (Comput (F,s,(4 + 1))) . (dl. 0) = 2 by A20, A37, Lm9, SCM_1:5;
then A44: (Comput (F,s,(5 + 1))) . (dl. 0) = 2 by A19, A38, SCM_1:9;
( IC (Comput (F,s,(5 + 1))) = 0 & (Comput (F,s,(5 + 1))) . (dl. 3) = (Comput (F,s,(4 + 1))) . (dl. 3) ) by A19, A38, SCM_1:9;
then A45: Comput (F,s,(5 + 1)) is 0 -started State-consisting of <%2,nn9,A,(B + A)%> by A41, A44, A43, A40, MEMSTR_0:def 12, SCM_1:13;
A46: (nn mod 2) + ((nn div 2) * 2) = nn by A25;
then A47: nn9 < nn by A34, A35, A42, PRE_FF:17;
A48: Fusc N = (A * (Fusc nn9)) + ((B + A) * (Fusc (nn9 + 1))) by A5, A34, A35, A42, A46, PRE_FF:19;
then A49: ( nn9 > 0 implies LifeSpan (F,(Comput (F,s,(5 + 1)))) = (6 * ([\(log (2,nn9))/] + 1)) + 1 ) by A3, A4, A45, A47;
A50: F halts_on Comput (F,s,(5 + 1)) by A3, A4, A45, A47, A48;
hence F halts_on s by EXTPRO_1:22; :: thesis:
(Result (F,(Comput (F,s,(5 + 1))))) . (dl. 3) = Fusc N by A3, A4, A45, A47, A48;
hence (Result (F,s)) . (dl. 3) = Fusc N by A50, EXTPRO_1:35; :: thesis:
thus ( nn = 0 implies LifeSpan (F,s) = 1 ) by A26; :: thesis:
A51: ( nn9 = 0 implies LifeSpan (F,(Comput (F,s,(5 + 1)))) = 1 ) by A3, A4, A34, A35, A25, A42, A45, A48;
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 A34, A35, A25, A42, A50, A51, Lm1, EXTPRO_1:34; :: thesis:

end;

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

then A53: nn9 > 0 ;
then reconsider m = [\(log (2,nn9))/] as Element of NAT by Lm2;
thus LifeSpan (F,s) = 6 + ((6 * (m + 1)) + 1) by A50, A49, A52, EXTPRO_1:34
.= (6 * ([\(log (2,nn))/] + 1)) + 1 by A34, A35, A42, A46, A53, Lm3 ; :: thesis:

end;

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

then A55: IC (Comput (F,s,(3 + 1))) = 6 by A9, A29, SCM_1:10;
then A56: IC (Comput (F,s,(4 + 1))) = 6 + 1 by A22, SCM_1:5;
(Comput (F,s,(3 + 1))) . (dl. 0) = 2 by A9, A29, A31, SCM_1:10;
then (Comput (F,s,(4 + 1))) . (dl. 0) = 2 by A22, A55, Lm8, SCM_1:5;
then A57: (Comput (F,s,(5 + 1))) . (dl. 0) = 2 by A21, A56, SCM_1:9;
A58: (Comput (F,s,(3 + 1))) . (dl. 3) = B by A9, A29, A32, SCM_1:10;
then (Comput (F,s,(4 + 1))) . (dl. 3) = B by A22, A55, Lm12, SCM_1:5;
then A59: (Comput (F,s,(5 + 1))) . (dl. 3) = B by A21, A56, SCM_1:9;
(Comput (F,s,(3 + 1))) . (dl. 1) = (Comput (F,s,(2 + 1))) . (dl. 1) by A9, A29, SCM_1:10;
then (Comput (F,s,(4 + 1))) . (dl. 1) = (Comput (F,s,(2 + 1))) . (dl. 1) by A22, A55, Lm10, SCM_1:5;
then A60: (Comput (F,s,(5 + 1))) . (dl. 1) = (Comput (F,s,(2 + 1))) . (dl. 1) by A21, A56, SCM_1:9;
(Comput (F,s,(3 + 1))) . (dl. 2) = A by A9, A29, A30, SCM_1:10;
then A61: (Comput (F,s,(4 + 1))) . (dl. 2) = A + B by A22, A55, A58, SCM_1:5;
reconsider nn9 = (Comput (F,s,(2 + 1))) . (dl. 1) as Element of NAT by A34, 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 A21, A56, SCM_1:9;
then A62: Comput (F,s,(5 + 1)) is 0 -started State-consisting of <%2,nn9,(A + B),B%> by A61, A57, A60, A59, MEMSTR_0:def 12, SCM_1:13;
A63: ( nn9 < nn & Fusc N = ((A + B) * (Fusc nn9)) + (B * (Fusc (nn9 + 1))) ) by A5, A26, A34, A35, A25, A54, PRE_FF:16, PRE_FF:20;
then A64: F halts_on Comput (F,s,(5 + 1)) by A3, A4, A62;
hence F halts_on s by EXTPRO_1:22; :: thesis:
(Result (F,(Comput (F,s,(5 + 1))))) . (dl. 3) = Fusc N by A3, A4, A62, A63;
hence (Result (F,s)) . (dl. 3) = Fusc N by A64, EXTPRO_1:35; :: thesis:
thus ( nn = 0 implies LifeSpan (F,s) = 1 ) by A26; :: thesis:
A65: ( nn9 > 0 implies LifeSpan (F,(Comput (F,s,(5 + 1)))) = (6 * ([\(log (2,nn9))/] + 1)) + 1 ) by A3, A4, A62, A63;
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 A13, A26, A28, A33, A34, A25, A54, Lm14, SCM_1:8; :: thesis:

end;

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

then A67: nn9 > 0 ;
then reconsider m = [\(log (2,nn9))/] as Element of NAT by Lm2;
thus LifeSpan (F,s) = 6 + ((6 * (m + 1)) + 1) by A64, A65, A66, EXTPRO_1:34
.= (6 * ([\(log (2,nn))/] + 1)) + 1 by A34, A35, A25, A54, A67, Lm5 ; :: thesis:

end;

thus ( 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 A15, A24; :: thesis:

end;

for n being Nat holds S₁[n] from NAT_1:sch 4(A2);
hence for n, N, A, B being Element of NAT
for s being 0 -started State-consisting of <%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: