let F be NAT -defined the Instructions of SCM -valued total Function; :: thesis: ( Fusc_Program c= F implies for N being Element of NAT st N > 0 holds
for s being 0 -started State-consisting of 0 ,((<*2*> ^ <*N*>) ^ <*1*>) ^ <*0*> holds
( F halts_on s & (Result (F,s)) . (dl. 3) = Fusc N & LifeSpan (F,s) = (6 * ([\(log (2,N))/] + 1)) + 1 ) )
set c2 = dl. 0;
set n = dl. 1;
set a = dl. 2;
set b = dl. 3;
set aux = dl. 4;
set L6 = 6;
set L7 = 7;
set L8 = 8;
set L0 = 0 ;
set L1 = 1;
set L2 = 2;
set L3 = 3;
set L4 = 4;
set L5 = 5;
assume Z: Fusc_Program c= F ; :: thesis: for N being Element of NAT st N > 0 holds
for s being 0 -started State-consisting of 0 ,((<*2*> ^ <*N*>) ^ <*1*>) ^ <*0*> holds
( F halts_on s & (Result (F,s)) . (dl. 3) = Fusc N & LifeSpan (F,s) = (6 * ([\(log (2,N))/] + 1)) + 1 )
let N be Element of NAT ; :: thesis: ( N > 0 implies for s being 0 -started State-consisting of 0 ,((<*2*> ^ <*N*>) ^ <*1*>) ^ <*0*> holds
( F halts_on s & (Result (F,s)) . (dl. 3) = Fusc N & LifeSpan (F,s) = (6 * ([\(log (2,N))/] + 1)) + 1 ) )
assume A1: N > 0 ; :: thesis: for s being 0 -started State-consisting of 0 ,((<*2*> ^ <*N*>) ^ <*1*>) ^ <*0*> holds
( F halts_on s & (Result (F,s)) . (dl. 3) = Fusc N & LifeSpan (F,s) = (6 * ([\(log (2,N))/] + 1)) + 1 )
set k = [\(log (2,N))/];
(log (2,N)) - 1 < [\(log (2,N))/] by INT_1:def 4;
then A2: log (2,N) < [\(log (2,N))/] + 1 by XREAL_1:21;
N >= 0 + 1 by A1, NAT_1:13;
then log (2,N) >= log (2,1) by PRE_FF:12;
then log (2,N) >= 0 by POWER:59;
then [\(log (2,N))/] + 1 > 0 by A2, XXREAL_0:2;
then reconsider k = [\(log (2,N))/] as Element of NAT by INT_1:16, INT_1:20;
2 to_power (k + 1) > 2 to_power (log (2,N)) by A2, POWER:44;
then 2 to_power (k + 1) > N by A1, POWER:def 3;
then A3: 2 |^ (k + 1) > N by POWER:46;
let S be 0 -started State-consisting of 0 ,((<*2*> ^ <*N*>) ^ <*1*>) ^ <*0*>; :: thesis: ( F halts_on S & (Result (F,S)) . (dl. 3) = Fusc N & LifeSpan (F,S) = (6 * ([\(log (2,N))/] + 1)) + 1 )
consider s being State of SCM such that
A4: s = S ;
defpred S₁[ Element of NAT ] means ( $1 <= (log (2,N)) + 1 implies for u being State of SCM st u = Comput (F,s,(6 * $1)) holds
( IC u = 0 & u . (dl. 0) = 2 & u . (dl. 1) = N div (2 |^ $1) & u . (dl. 1) is Element of NAT & Fusc N = ((u . (dl. 2)) * (Fusc' (u . (dl. 1)))) + ((u . (dl. 3)) * (Fusc' ((u . (dl. 1)) + 1))) ) );
A5: F . 0 = (dl. 1) =0_goto 8 by Z, L14;
A6: F . 7 = SCM-goto 0 by Z, L14;
A7: F . 1 = (dl. 4) := (dl. 0) by Z, L14;
A8: F . 4 = AddTo ((dl. 3),(dl. 2)) by Z, L14;
A9: F . 2 = Divide ((dl. 1),(dl. 4)) by Z, L14;
A10: F . 6 = AddTo ((dl. 2),(dl. 3)) by Z, L14;
A11: F . 3 = (dl. 4) =0_goto 6 by Z, L14;
A12: F . 5 = SCM-goto 0 by Z, L14;
A13: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A14: ( k <= (log (2,N)) + 1 implies for u being State of SCM st u = Comput (F,s,(6 * k)) holds
( IC u = 0 & u . (dl. 0) = 2 & u . (dl. 1) = N div (2 |^ k) & u . (dl. 1) is Element of NAT & Fusc N = ((u . (dl. 2)) * (Fusc' (u . (dl. 1)))) + ((u . (dl. 3)) * (Fusc' ((u . (dl. 1)) + 1))) ) ) ; :: thesis: S₁[k + 1]
set t = 6 * k;
set t0 = Comput (F,s,(6 * k));
assume A15: k + 1 <= (log (2,N)) + 1 ; :: thesis: for u being State of SCM st u = Comput (F,s,(6 * (k + 1))) holds
( IC u = 0 & u . (dl. 0) = 2 & u . (dl. 1) = N div (2 |^ (k + 1)) & u . (dl. 1) is Element of NAT & Fusc N = ((u . (dl. 2)) * (Fusc' (u . (dl. 1)))) + ((u . (dl. 3)) * (Fusc' ((u . (dl. 1)) + 1))) )
then k <= log (2,N) by XREAL_1:8;
then 2 to_power k <= 2 to_power (log (2,N)) by PRE_FF:10;
then 2 to_power k <= N by A1, POWER:def 3;
then A16: 2 |^ k <= N by POWER:46;
A17: k <= k + 1 by NAT_1:11;
then A18: (Comput (F,s,(6 * k))) . (dl. 1) is Element of NAT by A14, A15, XXREAL_0:2;
A19: (Comput (F,s,(6 * k))) . (dl. 1) = N div (2 |^ k) by A14, A15, A17, XXREAL_0:2;
A20: IC (Comput (F,s,(6 * k))) = 0 by A14, A15, A17, XXREAL_0:2;
set t3 = Comput (F,s,((6 * k) + 3));
set t2 = Comput (F,s,((6 * k) + 2));
set t1 = Comput (F,s,((6 * k) + 1));
A21: ((6 * k) + 1) + 1 = (6 * k) + 2 ;
2 |^ k > 0 by NEWTON:102;
then (Comput (F,s,(6 * k))) . (dl. 1) <> 0 by A19, A16, PRE_FF:3;
then A22: IC (Comput (F,s,((6 * k) + 1))) = 0 + 1 by A5, A20, SCM_1:24;
then A23: IC (Comput (F,s,((6 * k) + 2))) = 1 + 1 by A7, A21, SCM_1:18;
A24: ((6 * k) + 2) + 1 = (6 * k) + 3 ;
then A25: IC (Comput (F,s,((6 * k) + 3))) = 2 + 1 by A9, A23, Lm14, SCM_1:22;
(Comput (F,s,((6 * k) + 1))) . (dl. 1) = (Comput (F,s,(6 * k))) . (dl. 1) by A5, A20, SCM_1:24;
then A26: (Comput (F,s,((6 * k) + 2))) . (dl. 1) = (Comput (F,s,(6 * k))) . (dl. 1) by A7, A22, A21, Lm14, SCM_1:18;
A27: ((Comput (F,s,(6 * k))) . (dl. 1)) mod 2 = ((Comput (F,s,(6 * k))) . (dl. 1)) - ((((Comput (F,s,(6 * k))) . (dl. 1)) div 2) * 2) by INT_1:def 8;
let u be State of SCM; :: thesis: ( u = Comput (F,s,(6 * (k + 1))) implies ( IC u = 0 & u . (dl. 0) = 2 & u . (dl. 1) = N div (2 |^ (k + 1)) & u . (dl. 1) is Element of NAT & Fusc N = ((u . (dl. 2)) * (Fusc' (u . (dl. 1)))) + ((u . (dl. 3)) * (Fusc' ((u . (dl. 1)) + 1))) ) )
assume A28: u = Comput (F,s,(6 * (k + 1))) ; :: thesis: ( IC u = 0 & u . (dl. 0) = 2 & u . (dl. 1) = N div (2 |^ (k + 1)) & u . (dl. 1) is Element of NAT & Fusc N = ((u . (dl. 2)) * (Fusc' (u . (dl. 1)))) + ((u . (dl. 3)) * (Fusc' ((u . (dl. 1)) + 1))) )
(Comput (F,s,(6 * k))) . (dl. 0) = 2 by A14, A15, A17, XXREAL_0:2;
then A29: (Comput (F,s,((6 * k) + 1))) . (dl. 0) = 2 by A5, A20, SCM_1:24;
then (Comput (F,s,((6 * k) + 2))) . (dl. 0) = 2 by A7, A22, A21, Lm13, SCM_1:18;
then A30: (Comput (F,s,((6 * k) + 3))) . (dl. 0) = 2 by A9, A23, A24, Lm7, Lm13, Lm14, SCM_1:22;
A31: (Comput (F,s,((6 * k) + 2))) . (dl. 4) = 2 by A7, A22, A29, A21, SCM_1:18;
then A32: (Comput (F,s,((6 * k) + 3))) . (dl. 1) = ((Comput (F,s,(6 * k))) . (dl. 1)) div 2 by A9, A23, A26, A24, Lm14, SCM_1:22;
then A33: (Comput (F,s,((6 * k) + 3))) . (dl. 1) = N div ((2 |^ k) * 2) by A19, PRE_FF:5
.= N div (2 |^ (k + 1)) by NEWTON:11 ;
A34: (Comput (F,s,((6 * k) + 3))) . (dl. 4) = ((Comput (F,s,(6 * k))) . (dl. 1)) mod 2 by A9, A23, A31, A26, A24, Lm14, SCM_1:22;
set t6 = Comput (F,s,((6 * k) + 6));
set t5 = Comput (F,s,((6 * k) + 5));
set t4 = Comput (F,s,((6 * k) + 4));
A35: ((6 * k) + 3) + 1 = (6 * k) + 4 ;
(Comput (F,s,((6 * k) + 1))) . (dl. 3) = (Comput (F,s,(6 * k))) . (dl. 3) by A5, A20, SCM_1:24;
then (Comput (F,s,((6 * k) + 2))) . (dl. 3) = (Comput (F,s,(6 * k))) . (dl. 3) by A7, A22, A21, Lm16, SCM_1:18;
then A36: (Comput (F,s,((6 * k) + 3))) . (dl. 3) = (Comput (F,s,(6 * k))) . (dl. 3) by A9, A23, A24, Lm11, Lm14, Lm16, SCM_1:22;
A37: ((6 * k) + 5) + 1 = (6 * k) + 6 ;
(Comput (F,s,((6 * k) + 1))) . (dl. 2) = (Comput (F,s,(6 * k))) . (dl. 2) by A5, A20, SCM_1:24;
then (Comput (F,s,((6 * k) + 2))) . (dl. 2) = (Comput (F,s,(6 * k))) . (dl. 2) by A7, A22, A21, Lm15, SCM_1:18;
then A38: (Comput (F,s,((6 * k) + 3))) . (dl. 2) = (Comput (F,s,(6 * k))) . (dl. 2) by A9, A23, A24, Lm10, Lm14, Lm15, SCM_1:22;
A39: ((6 * k) + 4) + 1 = (6 * k) + 5 ;

per cases ( (Comput (F,s,((6 * k) + 3))) . (dl. 4) <> 0 or (Comput (F,s,((6 * k) + 3))) . (dl. 4) = 0 ) ;

suppose A40: (Comput (F,s,((6 * k) + 3))) . (dl. 4) <> 0 ; :: thesis: ( IC u = 0 & u . (dl. 0) = 2 & u . (dl. 1) = N div (2 |^ (k + 1)) & u . (dl. 1) is Element of NAT & Fusc N = ((u . (dl. 2)) * (Fusc' (u . (dl. 1)))) + ((u . (dl. 3)) * (Fusc' ((u . (dl. 1)) + 1))) )

reconsider ta = (Comput (F,s,(6 * k))) . (dl. 2), tb = (Comput (F,s,(6 * k))) . (dl. 3) as Integer ;
A41: (Comput (F,s,((6 * k) + 4))) . (dl. 2) = (Comput (F,s,(6 * k))) . (dl. 2) by A11, A25, A38, A35, SCM_1:24;
A42: IC (Comput (F,s,((6 * k) + 4))) = 3 + 1 by A11, A25, A35, A40, SCM_1:24;
then A43: IC (Comput (F,s,((6 * k) + 5))) = 4 + 1 by A8, A39, SCM_1:19;
(Comput (F,s,((6 * k) + 4))) . (dl. 1) = (Comput (F,s,((6 * k) + 3))) . (dl. 1) by A11, A25, A35, SCM_1:24;
then A44: (Comput (F,s,((6 * k) + 5))) . (dl. 1) = (Comput (F,s,((6 * k) + 3))) . (dl. 1) by A8, A39, A42, Lm11, SCM_1:19;
then A45: (Comput (F,s,((6 * k) + 6))) . (dl. 1) = (Comput (F,s,((6 * k) + 3))) . (dl. 1) by A12, A37, A43, SCM_1:23;
then reconsider un = u . (dl. 1), tn = (Comput (F,s,(6 * k))) . (dl. 1) as Element of NAT by A28, A18, A32, PRE_FF:7;
A46: tn = ((((Comput (F,s,(6 * k))) . (dl. 1)) div 2) * 2) + (((Comput (F,s,(6 * k))) . (dl. 1)) mod 2) by A27
.= (2 * un) + 1 by A28, A32, A34, A40, A45, PRE_FF:6 ;
then A47: tn + 1 = 2 * (un + 1) ;
(Comput (F,s,((6 * k) + 4))) . (dl. 0) = 2 by A11, A25, A30, A35, SCM_1:24;
then (Comput (F,s,((6 * k) + 5))) . (dl. 0) = 2 by A8, A39, A42, Lm9, SCM_1:19;
hence ( IC u = 0 & u . (dl. 0) = 2 & u . (dl. 1) = N div (2 |^ (k + 1)) ) by A12, A28, A33, A37, A43, A44, SCM_1:23; :: thesis: ( u . (dl. 1) is Element of NAT & Fusc N = ((u . (dl. 2)) * (Fusc' (u . (dl. 1)))) + ((u . (dl. 3)) * (Fusc' ((u . (dl. 1)) + 1))) )
thus u . (dl. 1) is Element of NAT by A28, A18, A32, A45, PRE_FF:7; :: thesis: Fusc N = ((u . (dl. 2)) * (Fusc' (u . (dl. 1)))) + ((u . (dl. 3)) * (Fusc' ((u . (dl. 1)) + 1)))
A48: Fusc' (((Comput (F,s,(6 * k))) . (dl. 1)) + 1) = Fusc (tn + 1) by Def2
.= Fusc (un + 1) by A47, PRE_FF:17
.= Fusc' ((u . (dl. 1)) + 1) by Def2 ;
(Comput (F,s,((6 * k) + 4))) . (dl. 3) = (Comput (F,s,(6 * k))) . (dl. 3) by A11, A25, A36, A35, SCM_1:24;
then (Comput (F,s,((6 * k) + 5))) . (dl. 3) = ((Comput (F,s,(6 * k))) . (dl. 3)) + ((Comput (F,s,(6 * k))) . (dl. 2)) by A8, A39, A42, A41, SCM_1:19;
then A49: (Comput (F,s,((6 * k) + 6))) . (dl. 3) = ((Comput (F,s,(6 * k))) . (dl. 3)) + ((Comput (F,s,(6 * k))) . (dl. 2)) by A12, A37, A43, SCM_1:23;
A50: Fusc' ((Comput (F,s,(6 * k))) . (dl. 1)) = Fusc tn by Def2
.= (Fusc un) + (Fusc (un + 1)) by A46, PRE_FF:17
.= (Fusc' (u . (dl. 1))) + (Fusc (un + 1)) by Def2
.= (Fusc' (u . (dl. 1))) + (Fusc' ((u . (dl. 1)) + 1)) by Def2 ;
reconsider un = u . (dl. 1), tn = (Comput (F,s,(6 * k))) . (dl. 1) as Integer ;
(Comput (F,s,((6 * k) + 5))) . (dl. 2) = (Comput (F,s,(6 * k))) . (dl. 2) by A8, A39, A42, A41, Lm12, SCM_1:19;
then (Comput (F,s,((6 * k) + 6))) . (dl. 2) = (Comput (F,s,(6 * k))) . (dl. 2) by A12, A37, A43, SCM_1:23;
then (ta * (Fusc' tn)) + (tb * (Fusc' (tn + 1))) = ((u . (dl. 2)) * (Fusc' un)) + ((u . (dl. 3)) * (Fusc' (un + 1))) by A28, A49, A50, A48;
hence Fusc N = ((u . (dl. 2)) * (Fusc' (u . (dl. 1)))) + ((u . (dl. 3)) * (Fusc' ((u . (dl. 1)) + 1))) by A14, A15, A17, XXREAL_0:2; :: thesis: verum

end;

suppose A51: (Comput (F,s,((6 * k) + 3))) . (dl. 4) = 0 ; :: thesis: ( IC u = 0 & u . (dl. 0) = 2 & u . (dl. 1) = N div (2 |^ (k + 1)) & u . (dl. 1) is Element of NAT & Fusc N = ((u . (dl. 2)) * (Fusc' (u . (dl. 1)))) + ((u . (dl. 3)) * (Fusc' ((u . (dl. 1)) + 1))) )

then A52: IC (Comput (F,s,((6 * k) + 4))) = 6 by A11, A25, A35, SCM_1:24;
then A53: IC (Comput (F,s,((6 * k) + 5))) = 6 + 1 by A10, A39, SCM_1:19;
(Comput (F,s,((6 * k) + 4))) . (dl. 1) = (Comput (F,s,((6 * k) + 3))) . (dl. 1) by A11, A25, A35, SCM_1:24;
then (Comput (F,s,((6 * k) + 5))) . (dl. 1) = (Comput (F,s,((6 * k) + 3))) . (dl. 1) by A10, A39, A52, Lm10, SCM_1:19;
then A54: (Comput (F,s,((6 * k) + 6))) . (dl. 1) = (Comput (F,s,((6 * k) + 3))) . (dl. 1) by A6, A37, A53, SCM_1:23;
then reconsider un = u . (dl. 1), tn = (Comput (F,s,(6 * k))) . (dl. 1) as Element of NAT by A28, A18, A32, PRE_FF:7;
A55: Fusc' (((Comput (F,s,(6 * k))) . (dl. 1)) + 1) = Fusc (tn + 1) by Def2
.= (Fusc un) + (Fusc (un + 1)) by A28, A32, A34, A27, A51, A54, PRE_FF:17
.= (Fusc un) + (Fusc' ((u . (dl. 1)) + 1)) by Def2
.= (Fusc' (u . (dl. 1))) + (Fusc' ((u . (dl. 1)) + 1)) by Def2 ;
A56: (Comput (F,s,((6 * k) + 4))) . (dl. 3) = (Comput (F,s,(6 * k))) . (dl. 3) by A11, A25, A36, A35, SCM_1:24;
then (Comput (F,s,((6 * k) + 5))) . (dl. 3) = (Comput (F,s,(6 * k))) . (dl. 3) by A10, A39, A52, Lm12, SCM_1:19;
then A57: (Comput (F,s,((6 * k) + 6))) . (dl. 3) = (Comput (F,s,(6 * k))) . (dl. 3) by A6, A37, A53, SCM_1:23;
(Comput (F,s,((6 * k) + 4))) . (dl. 0) = 2 by A11, A25, A30, A35, SCM_1:24;
then (Comput (F,s,((6 * k) + 5))) . (dl. 0) = 2 by A10, A39, A52, Lm8, SCM_1:19;
hence ( IC u = 0 & u . (dl. 0) = 2 & u . (dl. 1) = N div (2 |^ (k + 1)) & u . (dl. 1) is Element of NAT ) by A6, A28, A18, A32, A33, A37, A53, A54, PRE_FF:7, SCM_1:23; :: thesis: Fusc N = ((u . (dl. 2)) * (Fusc' (u . (dl. 1)))) + ((u . (dl. 3)) * (Fusc' ((u . (dl. 1)) + 1)))
A58: Fusc' ((Comput (F,s,(6 * k))) . (dl. 1)) = Fusc tn by Def2
.= Fusc un by A28, A32, A34, A27, A51, A54, PRE_FF:17
.= Fusc' (u . (dl. 1)) by Def2 ;
(Comput (F,s,((6 * k) + 4))) . (dl. 2) = (Comput (F,s,(6 * k))) . (dl. 2) by A11, A25, A38, A35, SCM_1:24;
then (Comput (F,s,((6 * k) + 5))) . (dl. 2) = ((Comput (F,s,(6 * k))) . (dl. 2)) + ((Comput (F,s,(6 * k))) . (dl. 3)) by A10, A39, A52, A56, SCM_1:19;
then A59: (Comput (F,s,((6 * k) + 6))) . (dl. 2) = ((Comput (F,s,(6 * k))) . (dl. 2)) + ((Comput (F,s,(6 * k))) . (dl. 3)) by A6, A37, A53, SCM_1:23;
reconsider un = u . (dl. 1), tn = (Comput (F,s,(6 * k))) . (dl. 1), ta = (Comput (F,s,(6 * k))) . (dl. 2), tb = (Comput (F,s,(6 * k))) . (dl. 3) as Integer ;
(ta * (Fusc' tn)) + (tb * (Fusc' (tn + 1))) = ((ta + tb) * (Fusc' un)) + (tb * (Fusc' (un + 1))) by A58, A55;
hence Fusc N = ((u . (dl. 2)) * (Fusc' (u . (dl. 1)))) + ((u . (dl. 3)) * (Fusc' ((u . (dl. 1)) + 1))) by A14, A15, A28, A17, A59, A57, XXREAL_0:2; :: thesis: verum

end;

end;

end;

set h = Comput (F,s,((6 * (k + 1)) + 1));
set u = Comput (F,s,(6 * (k + 1)));
A60: s . (dl. 1) = N by A4, SCM_1:13;
A61: ( s . (dl. 2) = 1 & s . (dl. 3) = 0 ) by A4, SCM_1:13;
A62: S₁[ 0 ]

proof

assume 0 <= (log (2,N)) + 1 ; :: thesis: for u being State of SCM st u = Comput (F,s,(6 * 0)) holds
( IC u = 0 & u . (dl. 0) = 2 & u . (dl. 1) = N div (2 |^ 0) & u . (dl. 1) is Element of NAT & Fusc N = ((u . (dl. 2)) * (Fusc' (u . (dl. 1)))) + ((u . (dl. 3)) * (Fusc' ((u . (dl. 1)) + 1))) )
let u be State of SCM; :: thesis: ( u = Comput (F,s,(6 * 0)) implies ( IC u = 0 & u . (dl. 0) = 2 & u . (dl. 1) = N div (2 |^ 0) & u . (dl. 1) is Element of NAT & Fusc N = ((u . (dl. 2)) * (Fusc' (u . (dl. 1)))) + ((u . (dl. 3)) * (Fusc' ((u . (dl. 1)) + 1))) ) )
assume u = Comput (F,s,(6 * 0)) ; :: thesis: ( IC u = 0 & u . (dl. 0) = 2 & u . (dl. 1) = N div (2 |^ 0) & u . (dl. 1) is Element of NAT & Fusc N = ((u . (dl. 2)) * (Fusc' (u . (dl. 1)))) + ((u . (dl. 3)) * (Fusc' ((u . (dl. 1)) + 1))) )
then A63: u = s by EXTPRO_1:3;
hence ( IC u = 0 & u . (dl. 0) = 2 ) by A4, COMPOS_1:def 20, SCM_1:13; :: thesis: ( u . (dl. 1) = N div (2 |^ 0) & u . (dl. 1) is Element of NAT & Fusc N = ((u . (dl. 2)) * (Fusc' (u . (dl. 1)))) + ((u . (dl. 3)) * (Fusc' ((u . (dl. 1)) + 1))) )
thus u . (dl. 1) = N div 1 by A60, A63, PRE_FF:2
.= N div (2 |^ 0) by NEWTON:9 ; :: thesis: ( u . (dl. 1) is Element of NAT & Fusc N = ((u . (dl. 2)) * (Fusc' (u . (dl. 1)))) + ((u . (dl. 3)) * (Fusc' ((u . (dl. 1)) + 1))) )
thus u . (dl. 1) is Element of NAT by A4, A63, SCM_1:13; :: thesis: Fusc N = ((u . (dl. 2)) * (Fusc' (u . (dl. 1)))) + ((u . (dl. 3)) * (Fusc' ((u . (dl. 1)) + 1)))
thus Fusc N = ((u . (dl. 2)) * (Fusc' (u . (dl. 1)))) + ((u . (dl. 3)) * (Fusc' ((u . (dl. 1)) + 1))) by A60, A61, A63, Def2; :: thesis: verum

end;

A64: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A62, A13);
[\(log (2,N))/] <= log (2,N) by INT_1:def 4;
then A65: k + 1 <= (log (2,N)) + 1 by XREAL_1:8;
then A66: Fusc N = (((Comput (F,s,(6 * (k + 1)))) . (dl. 2)) * (Fusc' ((Comput (F,s,(6 * (k + 1)))) . (dl. 1)))) + (((Comput (F,s,(6 * (k + 1)))) . (dl. 3)) * (Fusc' (((Comput (F,s,(6 * (k + 1)))) . (dl. 1)) + 1))) by A64;
A67: IC (Comput (F,s,(6 * (k + 1)))) = 0 by A64, A65;
then A68: (Comput (F,s,((6 * (k + 1)) + 1))) . (dl. 3) = (Comput (F,s,(6 * (k + 1)))) . (dl. 3) by A5, SCM_1:24;
(Comput (F,s,(6 * (k + 1)))) . (dl. 1) = N div (2 |^ (k + 1)) by A64, A65;
then A69: (Comput (F,s,(6 * (k + 1)))) . (dl. 1) = 0 by A3, NAT_1:2, PRE_FF:4;
then A70: IC (Comput (F,s,((6 * (k + 1)) + 1))) = 8 by A5, A67, SCM_1:24;
A71: F . (IC (Comput (F,s,(6 * (k + 1))))) <> halt SCM by A5, A67, SCM_1:26;
A72: F . 8 = halt SCM by Z, L14;
hence F halts_on S by A4, A70, EXTPRO_1:31; :: thesis: ( (Result (F,S)) . (dl. 3) = Fusc N & LifeSpan (F,S) = (6 * ([\(log (2,N))/] + 1)) + 1 )
(((Comput (F,s,(6 * (k + 1)))) . (dl. 2)) * (Fusc' ((Comput (F,s,(6 * (k + 1)))) . (dl. 1)))) + (((Comput (F,s,(6 * (k + 1)))) . (dl. 3)) * (Fusc' (((Comput (F,s,(6 * (k + 1)))) . (dl. 1)) + 1))) = (((Comput (F,s,(6 * (k + 1)))) . (dl. 2)) * 0) + (((Comput (F,s,(6 * (k + 1)))) . (dl. 3)) * (Fusc' (((Comput (F,s,(6 * (k + 1)))) . (dl. 1)) + 1))) by A69, Def2, PRE_FF:17
.= ((Comput (F,s,(6 * (k + 1)))) . (dl. 3)) * (Fusc (0 + 1)) by A69, Def2
.= (Comput (F,s,(6 * (k + 1)))) . (dl. 3) by PRE_FF:17 ;
hence (Result (F,S)) . (dl. 3) = Fusc N by A4, A72, A66, A70, A68, EXTPRO_1:32; :: thesis: LifeSpan (F,S) = (6 * ([\(log (2,N))/] + 1)) + 1
F . (IC (Comput (F,s,((6 * (k + 1)) + 1)))) = halt SCM by A70, Z, L14;
hence LifeSpan (F,S) = (6 * ([\(log (2,N))/] + 1)) + 1 by A4, A71, EXTPRO_1:34; :: thesis: verum