let F be NAT -defined the InstructionsF 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 <%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 A1: Fusc_Program c= F ; :: thesis: for N being Element of NAT st N > 0 holds
for s being 0 -started State-consisting of <%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 <%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 A2: N > 0 ; :: thesis: for s being 0 -started State-consisting of <%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 6;
then A3: log (2,N) < [\(log (2,N))/] + 1 by XREAL_1:19;
N >= 0 + 1 by A2, NAT_1:13;
then log (2,N) >= log (2,1) by PRE_FF:10;
then log (2,N) >= 0 by POWER:51;
then [\(log (2,N))/] + 1 > 0 by A3;
then reconsider k = [\(log (2,N))/] as Element of NAT by INT_1:3, INT_1:7;
2 to_power (k + 1) > 2 to_power (log (2,N)) by A3, POWER:39;
then 2 to_power (k + 1) > N by A2, POWER:def 3;
then A4: 2 |^ (k + 1) > N by POWER:41;
let S be 0 -started State-consisting of <%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
A5: s = S ;
defpred S1[ 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))) ) );
A6: F . 0 = (dl. 1) =0_goto 8 by A1, Lm17;
A7: F . 7 = SCM-goto 0 by A1, Lm17;
A8: F . 1 = (dl. 4) := (dl. 0) by A1, Lm17;
A9: F . 4 = AddTo ((dl. 3),(dl. 2)) by A1, Lm17;
A10: F . 2 = Divide ((dl. 1),(dl. 4)) by A1, Lm17;
A11: F . 6 = AddTo ((dl. 2),(dl. 3)) by A1, Lm17;
A12: F . 3 = (dl. 4) =0_goto 6 by A1, Lm17;
A13: F . 5 = SCM-goto 0 by A1, Lm17;
A14: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A15: ( 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: S1[k + 1]
set t = 6 * k;
set t0 = Comput (F,s,(6 * k));
assume A16: 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:6;
then 2 to_power k <= 2 to_power (log (2,N)) by PRE_FF:8;
then 2 to_power k <= N by A2, POWER:def 3;
then A17: 2 |^ k <= N by POWER:41;
A18: k <= k + 1 by NAT_1:11;
then A19: (Comput (F,s,(6 * k))) . (dl. 1) is Element of NAT by A15, A16, XXREAL_0:2;
A20: (Comput (F,s,(6 * k))) . (dl. 1) = N div (2 |^ k) by A15, A16, A18, XXREAL_0:2;
A21: IC (Comput (F,s,(6 * k))) = 0 by A15, A16, A18, 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));
A22: ((6 * k) + 1) + 1 = (6 * k) + 2 ;
2 |^ k > 0 by NEWTON:83;
then (Comput (F,s,(6 * k))) . (dl. 1) <> 0 by A20, A17, PRE_FF:3;
then A23: IC (Comput (F,s,((6 * k) + 1))) = 0 + 1 by A6, A21, SCM_1:10;
then A24: IC (Comput (F,s,((6 * k) + 2))) = 1 + 1 by A8, A22, SCM_1:4;
A25: ((6 * k) + 2) + 1 = (6 * k) + 3 ;
then A26: IC (Comput (F,s,((6 * k) + 3))) = 2 + 1 by A10, A24, Lm14, SCM_1:8;
(Comput (F,s,((6 * k) + 1))) . (dl. 1) = (Comput (F,s,(6 * k))) . (dl. 1) by A6, A21, SCM_1:10;
then A27: (Comput (F,s,((6 * k) + 2))) . (dl. 1) = (Comput (F,s,(6 * k))) . (dl. 1) by A8, A23, A22, Lm14, SCM_1:4;
A28: ((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 10;
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 A29: 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 A15, A16, A18, XXREAL_0:2;
then A30: (Comput (F,s,((6 * k) + 1))) . (dl. 0) = 2 by A6, A21, SCM_1:10;
then (Comput (F,s,((6 * k) + 2))) . (dl. 0) = 2 by A8, A23, A22, Lm13, SCM_1:4;
then A31: (Comput (F,s,((6 * k) + 3))) . (dl. 0) = 2 by A10, A24, A25, Lm7, Lm13, Lm14, SCM_1:8;
A32: (Comput (F,s,((6 * k) + 2))) . (dl. 4) = 2 by A8, A23, A30, A22, SCM_1:4;
then A33: (Comput (F,s,((6 * k) + 3))) . (dl. 1) = ((Comput (F,s,(6 * k))) . (dl. 1)) div 2 by A10, A24, A27, A25, Lm14, SCM_1:8;
then A34: (Comput (F,s,((6 * k) + 3))) . (dl. 1) = N div ((2 |^ k) * 2) by A20, PRE_FF:5
.= N div (2 |^ (k + 1)) by NEWTON:6 ;
A35: (Comput (F,s,((6 * k) + 3))) . (dl. 4) = ((Comput (F,s,(6 * k))) . (dl. 1)) mod 2 by A10, A24, A32, A27, A25, Lm14, SCM_1:8;
set t6 = Comput (F,s,((6 * k) + 6));
set t5 = Comput (F,s,((6 * k) + 5));
set t4 = Comput (F,s,((6 * k) + 4));
A36: ((6 * k) + 3) + 1 = (6 * k) + 4 ;
(Comput (F,s,((6 * k) + 1))) . (dl. 3) = (Comput (F,s,(6 * k))) . (dl. 3) by A6, A21, SCM_1:10;
then (Comput (F,s,((6 * k) + 2))) . (dl. 3) = (Comput (F,s,(6 * k))) . (dl. 3) by A8, A23, A22, Lm16, SCM_1:4;
then A37: (Comput (F,s,((6 * k) + 3))) . (dl. 3) = (Comput (F,s,(6 * k))) . (dl. 3) by A10, A24, A25, Lm11, Lm14, Lm16, SCM_1:8;
A38: ((6 * k) + 5) + 1 = (6 * k) + 6 ;
(Comput (F,s,((6 * k) + 1))) . (dl. 2) = (Comput (F,s,(6 * k))) . (dl. 2) by A6, A21, SCM_1:10;
then (Comput (F,s,((6 * k) + 2))) . (dl. 2) = (Comput (F,s,(6 * k))) . (dl. 2) by A8, A23, A22, Lm15, SCM_1:4;
then A39: (Comput (F,s,((6 * k) + 3))) . (dl. 2) = (Comput (F,s,(6 * k))) . (dl. 2) by A10, A24, A25, Lm10, Lm14, Lm15, SCM_1:8;
A40: ((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 A41: (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 ;
A42: (Comput (F,s,((6 * k) + 4))) . (dl. 2) = (Comput (F,s,(6 * k))) . (dl. 2) by A12, A26, A39, A36, SCM_1:10;
A43: IC (Comput (F,s,((6 * k) + 4))) = 3 + 1 by A12, A26, A36, A41, SCM_1:10;
then A44: IC (Comput (F,s,((6 * k) + 5))) = 4 + 1 by A9, A40, SCM_1:5;
(Comput (F,s,((6 * k) + 4))) . (dl. 1) = (Comput (F,s,((6 * k) + 3))) . (dl. 1) by A12, A26, A36, SCM_1:10;
then A45: (Comput (F,s,((6 * k) + 5))) . (dl. 1) = (Comput (F,s,((6 * k) + 3))) . (dl. 1) by A9, A40, A43, Lm11, SCM_1:5;
then A46: (Comput (F,s,((6 * k) + 6))) . (dl. 1) = (Comput (F,s,((6 * k) + 3))) . (dl. 1) by A13, A38, A44, SCM_1:9;
then reconsider un = u . (dl. 1), tn = (Comput (F,s,(6 * k))) . (dl. 1) as Element of NAT by A29, A19, A33, PRE_FF:7;
A47: tn = ((((Comput (F,s,(6 * k))) . (dl. 1)) div 2) * 2) + (((Comput (F,s,(6 * k))) . (dl. 1)) mod 2) by A28
.= (2 * un) + 1 by A29, A33, A35, A41, A46, PRE_FF:6 ;
then A48: tn + 1 = 2 * (un + 1) ;
(Comput (F,s,((6 * k) + 4))) . (dl. 0) = 2 by A12, A26, A31, A36, SCM_1:10;
then (Comput (F,s,((6 * k) + 5))) . (dl. 0) = 2 by A9, A40, A43, Lm9, SCM_1:5;
hence ( IC u = 0 & u . (dl. 0) = 2 & u . (dl. 1) = N div (2 |^ (k + 1)) ) by A13, A29, A34, A38, A44, A45, SCM_1: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 A29, A19, A33, A46, PRE_FF:7; :: thesis: Fusc N = ((u . (dl. 2)) * (Fusc' (u . (dl. 1)))) + ((u . (dl. 3)) * (Fusc' ((u . (dl. 1)) + 1)))
A49: Fusc' (((Comput (F,s,(6 * k))) . (dl. 1)) + 1) = Fusc (tn + 1) by Def2
.= Fusc (un + 1) by A48, PRE_FF:15
.= Fusc' ((u . (dl. 1)) + 1) by Def2 ;
(Comput (F,s,((6 * k) + 4))) . (dl. 3) = (Comput (F,s,(6 * k))) . (dl. 3) by A12, A26, A37, A36, SCM_1:10;
then (Comput (F,s,((6 * k) + 5))) . (dl. 3) = ((Comput (F,s,(6 * k))) . (dl. 3)) + ((Comput (F,s,(6 * k))) . (dl. 2)) by A9, A40, A43, A42, SCM_1:5;
then A50: (Comput (F,s,((6 * k) + 6))) . (dl. 3) = ((Comput (F,s,(6 * k))) . (dl. 3)) + ((Comput (F,s,(6 * k))) . (dl. 2)) by A13, A38, A44, SCM_1:9;
A51: Fusc' ((Comput (F,s,(6 * k))) . (dl. 1)) = Fusc tn by Def2
.= (Fusc un) + (Fusc (un + 1)) by A47, PRE_FF:15
.= (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 A9, A40, A43, A42, Lm12, SCM_1:5;
then (Comput (F,s,((6 * k) + 6))) . (dl. 2) = (Comput (F,s,(6 * k))) . (dl. 2) by A13, A38, A44, SCM_1:9;
then (ta * (Fusc' tn)) + (tb * (Fusc' (tn + 1))) = ((u . (dl. 2)) * (Fusc' un)) + ((u . (dl. 3)) * (Fusc' (un + 1))) by A29, A50, A51, A49;
hence Fusc N = ((u . (dl. 2)) * (Fusc' (u . (dl. 1)))) + ((u . (dl. 3)) * (Fusc' ((u . (dl. 1)) + 1))) by A15, A16, A18, XXREAL_0:2; :: thesis: verum
end;
suppose A52: (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 A53: IC (Comput (F,s,((6 * k) + 4))) = 6 by A12, A26, A36, SCM_1:10;
then A54: IC (Comput (F,s,((6 * k) + 5))) = 6 + 1 by A11, A40, SCM_1:5;
(Comput (F,s,((6 * k) + 4))) . (dl. 1) = (Comput (F,s,((6 * k) + 3))) . (dl. 1) by A12, A26, A36, SCM_1:10;
then (Comput (F,s,((6 * k) + 5))) . (dl. 1) = (Comput (F,s,((6 * k) + 3))) . (dl. 1) by A11, A40, A53, Lm10, SCM_1:5;
then A55: (Comput (F,s,((6 * k) + 6))) . (dl. 1) = (Comput (F,s,((6 * k) + 3))) . (dl. 1) by A7, A38, A54, SCM_1:9;
then reconsider un = u . (dl. 1), tn = (Comput (F,s,(6 * k))) . (dl. 1) as Element of NAT by A29, A19, A33, PRE_FF:7;
A56: Fusc' (((Comput (F,s,(6 * k))) . (dl. 1)) + 1) = Fusc (tn + 1) by Def2
.= (Fusc un) + (Fusc (un + 1)) by A29, A33, A35, A28, A52, A55, PRE_FF:15
.= (Fusc un) + (Fusc' ((u . (dl. 1)) + 1)) by Def2
.= (Fusc' (u . (dl. 1))) + (Fusc' ((u . (dl. 1)) + 1)) by Def2 ;
A57: (Comput (F,s,((6 * k) + 4))) . (dl. 3) = (Comput (F,s,(6 * k))) . (dl. 3) by A12, A26, A37, A36, SCM_1:10;
then (Comput (F,s,((6 * k) + 5))) . (dl. 3) = (Comput (F,s,(6 * k))) . (dl. 3) by A11, A40, A53, Lm12, SCM_1:5;
then A58: (Comput (F,s,((6 * k) + 6))) . (dl. 3) = (Comput (F,s,(6 * k))) . (dl. 3) by A7, A38, A54, SCM_1:9;
(Comput (F,s,((6 * k) + 4))) . (dl. 0) = 2 by A12, A26, A31, A36, SCM_1:10;
then (Comput (F,s,((6 * k) + 5))) . (dl. 0) = 2 by A11, A40, A53, Lm8, SCM_1:5;
hence ( IC u = 0 & u . (dl. 0) = 2 & u . (dl. 1) = N div (2 |^ (k + 1)) & u . (dl. 1) is Element of NAT ) by A7, A29, A19, A33, A34, A38, A54, A55, PRE_FF:7, SCM_1:9; :: thesis: Fusc N = ((u . (dl. 2)) * (Fusc' (u . (dl. 1)))) + ((u . (dl. 3)) * (Fusc' ((u . (dl. 1)) + 1)))
A59: Fusc' ((Comput (F,s,(6 * k))) . (dl. 1)) = Fusc tn by Def2
.= Fusc un by A29, A33, A35, A28, A52, A55, PRE_FF:15
.= Fusc' (u . (dl. 1)) by Def2 ;
(Comput (F,s,((6 * k) + 4))) . (dl. 2) = (Comput (F,s,(6 * k))) . (dl. 2) by A12, A26, A39, A36, SCM_1:10;
then (Comput (F,s,((6 * k) + 5))) . (dl. 2) = ((Comput (F,s,(6 * k))) . (dl. 2)) + ((Comput (F,s,(6 * k))) . (dl. 3)) by A11, A40, A53, A57, SCM_1:5;
then A60: (Comput (F,s,((6 * k) + 6))) . (dl. 2) = ((Comput (F,s,(6 * k))) . (dl. 2)) + ((Comput (F,s,(6 * k))) . (dl. 3)) by A7, A38, A54, SCM_1:9;
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 A59, A56;
hence Fusc N = ((u . (dl. 2)) * (Fusc' (u . (dl. 1)))) + ((u . (dl. 3)) * (Fusc' ((u . (dl. 1)) + 1))) by A15, A16, A29, A18, A60, A58, 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)));
A61: s . (dl. 1) = N by A5, SCM_1:1;
A62: ( s . (dl. 2) = 1 & s . (dl. 3) = 0 ) by A5, SCM_1:1;
A63: S1[ 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 A64: u = s by EXTPRO_1:2;
hence ( IC u = 0 & u . (dl. 0) = 2 ) by A5, MEMSTR_0:def 12, SCM_1:1; :: 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 A61, A64, PRE_FF:2
.= N div (2 |^ 0) by NEWTON:4 ; :: 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 A5, A64, SCM_1:1; :: 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 A61, A62, A64, Def2; :: thesis: verum
end;
A65: for k being Nat holds S1[k] from NAT_1:sch 2(A63, A14);
 [\(log (2,N))/] <= log (2,N) by INT_1:def 6;
then A66: k + 1 <= (log (2,N)) + 1 by XREAL_1:6;
then A67: 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 A65;
A68: IC (Comput (F,s,(6 * (k + 1)))) = 0 by A65, A66;
then A69: (Comput (F,s,((6 * (k + 1)) + 1))) . (dl. 3) = (Comput (F,s,(6 * (k + 1)))) . (dl. 3) by A6, SCM_1:10;
(Comput (F,s,(6 * (k + 1)))) . (dl. 1) = N div (2 |^ (k + 1)) by A65, A66;
then A70: (Comput (F,s,(6 * (k + 1)))) . (dl. 1) = 0 by A4, PRE_FF:4;
then A71: IC (Comput (F,s,((6 * (k + 1)) + 1))) = 8 by A6, A68, SCM_1:10;
A72: F . (IC (Comput (F,s,(6 * (k + 1))))) <> halt SCM by A6, A68, SCM_1:12;
A73: F . 8 = halt SCM by A1, Lm17;
hence F halts_on S by A5, A71, EXTPRO_1:30; :: 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 A70, Def2, PRE_FF:15
.= ((Comput (F,s,(6 * (k + 1)))) . (dl. 3)) * (Fusc (0 + 1)) by A70, Def2
.= (Comput (F,s,(6 * (k + 1)))) . (dl. 3) by PRE_FF:15 ;
hence (Result (F,S)) . (dl. 3) = Fusc N by A5, A73, A67, A71, A69, EXTPRO_1:7; :: thesis: LifeSpan (F,S) = (6 * ([\(log (2,N))/] + 1)) + 1
F . (IC (Comput (F,s,((6 * (k + 1)) + 1)))) = halt SCM by A71, A1, Lm17;
hence LifeSpan (F,S) = (6 * ([\(log (2,N))/] + 1)) + 1 by A5, A72, EXTPRO_1:33; :: thesis: verum