:: FIB_FUSC semantic presentation

begin

Lm1:  0 = [\(log (2,1))/]
proof
thus  0 = [\0/] by INT_1:25
.= [\(log (2,1))/] by POWER:51 ; ::_thesis: verum
end;

Lm2:  for nn9 being Element of NAT st nn9 > 0 holds
( [\(log (2,nn9))/] is Element of NAT & (6 * ([\(log (2,nn9))/] + 1)) + 1 > 0 )
proof
let nn9 be Element of NAT ; ::_thesis: ( nn9 > 0 implies ( [\(log (2,nn9))/] is Element of NAT & (6 * ([\(log (2,nn9))/] + 1)) + 1 > 0 ) )
assume  nn9 > 0 ; ::_thesis: ( [\(log (2,nn9))/] is Element of NAT & (6 * ([\(log (2,nn9))/] + 1)) + 1 > 0 )
then A1: nn9 >= 0 + 1 by NAT_1:13;
 log (2,1) = 0 by POWER:51;
then  log (2,nn9) >= 0 by A1, PRE_FF:10;
then  [\(log (2,nn9))/] >= [\0/] by PRE_FF:9;
then  [\(log (2,nn9))/] >= 0 by INT_1:25;
then reconsider F = [\(log (2,nn9))/] as Element of NAT by INT_1:3;
 F is Element of NAT ;
hence  [\(log (2,nn9))/] is Element of NAT ; ::_thesis: (6 * ([\(log (2,nn9))/] + 1)) + 1 > 0
 (6 * F) + (6 * 1) >= 0 by NAT_1:12;
hence  (6 * ([\(log (2,nn9))/] + 1)) + 1 > 0 by NAT_1:13; ::_thesis: verum
end;

Lm3:  for nn, nn9 being Element of NAT st nn = (2 * nn9) + 1 & nn9 > 0 holds
6 + ((6 * ([\(log (2,nn9))/] + 1)) + 1) = (6 * ([\(log (2,nn))/] + 1)) + 1
proof
let nn, nn9 be Element of NAT ; ::_thesis: ( nn = (2 * nn9) + 1 & nn9 > 0 implies 6 + ((6 * ([\(log (2,nn9))/] + 1)) + 1) = (6 * ([\(log (2,nn))/] + 1)) + 1 )
assume A1: ( nn = (2 * nn9) + 1 & nn9 > 0 ) ; ::_thesis: 6 + ((6 * ([\(log (2,nn9))/] + 1)) + 1) = (6 * ([\(log (2,nn))/] + 1)) + 1
set F = [\(log (2,nn9))/];
thus 6 + ((6 * ([\(log (2,nn9))/] + 1)) + 1) = (6 * (1 + ([\(log (2,nn9))/] + 1))) + 1
.= (6 * ([\(log (2,nn))/] + 1)) + 1 by A1, PRE_FF:14 ; ::_thesis: verum
end;

Lm4:  for n being Element of NAT st n > 0 holds
( log (2,(2 * n)) = 1 + (log (2,n)) & log (2,(2 * n)) = (log (2,n)) + 1 )
proof
let n be Element of NAT ; ::_thesis: ( n > 0 implies ( log (2,(2 * n)) = 1 + (log (2,n)) & log (2,(2 * n)) = (log (2,n)) + 1 ) )
assume  n > 0 ; ::_thesis: ( log (2,(2 * n)) = 1 + (log (2,n)) & log (2,(2 * n)) = (log (2,n)) + 1 )
hence  log (2,(2 * n)) = (log (2,2)) + (log (2,n)) by POWER:53
.= 1 + (log (2,n)) by POWER:52 ;
::_thesis: log (2,(2 * n)) = (log (2,n)) + 1
hence  log (2,(2 * n)) = (log (2,n)) + 1 ; ::_thesis: verum
end;

Lm5:  for nn, nn9 being Element of NAT st nn = 2 * nn9 & nn9 > 0 holds
6 + ((6 * ([\(log (2,nn9))/] + 1)) + 1) = (6 * ([\(log (2,nn))/] + 1)) + 1
proof
let nn, nn9 be Element of NAT ; ::_thesis: ( nn = 2 * nn9 & nn9 > 0 implies 6 + ((6 * ([\(log (2,nn9))/] + 1)) + 1) = (6 * ([\(log (2,nn))/] + 1)) + 1 )
assume A1: ( nn = 2 * nn9 & nn9 > 0 ) ; ::_thesis: 6 + ((6 * ([\(log (2,nn9))/] + 1)) + 1) = (6 * ([\(log (2,nn))/] + 1)) + 1
set F = [\(log (2,nn9))/];
thus 6 + ((6 * ([\(log (2,nn9))/] + 1)) + 1) = (6 * (1 + ([\(log (2,nn9))/] + 1))) + 1
.= (6 * (1 + [\((log (2,nn9)) + 1)/])) + 1 by INT_1:28
.= (6 * ([\(log (2,nn))/] + 1)) + 1 by A1, Lm4 ; ::_thesis: verum
end;

Lm6:  for N being Element of NAT st N <> 0 holds
(6 * N) - 4 > 0
proof
let N be Element of NAT ; ::_thesis: ( N <> 0 implies (6 * N) - 4 > 0 )
assume  N <> 0 ; ::_thesis: (6 * N) - 4 > 0
then consider L being Nat such that
A1: N = L + 1 by NAT_1:6;
reconsider L = L as Element of NAT by ORDINAL1:def_12;
 (6 * L) + 2 <> 0 by NAT_1:7;
hence  (6 * N) - 4 > 0 by A1, NAT_1:3; ::_thesis: verum
end;

Lm7:  dl. 0 <> dl. 1
by AMI_3:10;

Lm8:  dl. 0 <> dl. 2
by AMI_3:10;

Lm9:  dl. 0 <> dl. 3
by AMI_3:10;

Lm10:  dl. 1 <> dl. 2
by AMI_3:10;

Lm11:  dl. 1 <> dl. 3
by AMI_3:10;

Lm12:  dl. 2 <> dl. 3
by AMI_3:10;

Lm13:  dl. 0 <> dl. 4
by AMI_3:10;

Lm14:  dl. 1 <> dl. 4
by AMI_3:10;

Lm15:  dl. 2 <> dl. 4
by AMI_3:10;

Lm16:  dl. 3 <> dl. 4
by AMI_3:10;

definition
func Fib_Program  ->  XFinSequence of  equals :: FIB_FUSC:def 1
(((((((<%((dl. 1) >0_goto 2)%> ^ <%(halt SCM)%>) ^ <%((dl. 3) := (dl. 0))%>) ^ <%(SubFrom ((dl. 1),(dl. 0)))%>) ^ <%((dl. 1) =0_goto 1)%>) ^ <%((dl. 4) := (dl. 2))%>) ^ <%((dl. 2) := (dl. 3))%>) ^ <%(AddTo ((dl. 3),(dl. 4)))%>) ^ <%(SCM-goto 3)%>;
coherence
 (((((((<%((dl. 1) >0_goto 2)%> ^ <%(halt SCM)%>) ^ <%((dl. 3) := (dl. 0))%>) ^ <%(SubFrom ((dl. 1),(dl. 0)))%>) ^ <%((dl. 1) =0_goto 1)%>) ^ <%((dl. 4) := (dl. 2))%>) ^ <%((dl. 2) := (dl. 3))%>) ^ <%(AddTo ((dl. 3),(dl. 4)))%>) ^ <%(SCM-goto 3)%> is XFinSequence of ;
end;

:: deftheorem  defines Fib_Program FIB_FUSC:def_1_:_
 Fib_Program = (((((((<%((dl. 1) >0_goto 2)%> ^ <%(halt SCM)%>) ^ <%((dl. 3) := (dl. 0))%>) ^ <%(SubFrom ((dl. 1),(dl. 0)))%>) ^ <%((dl. 1) =0_goto 1)%>) ^ <%((dl. 4) := (dl. 2))%>) ^ <%((dl. 2) := (dl. 3))%>) ^ <%(AddTo ((dl. 3),(dl. 4)))%>) ^ <%(SCM-goto 3)%>;

 Lm17:  for F being NAT -defined the InstructionsF of SCM -valued total Function
for I1, I2, I3, I4, I5, I6, I7, I8, I9 being Instruction of SCM st (((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%> c= F holds
( F . 0 = I1 & F . 1 = I2 & F . 2 = I3 & F . 3 = I4 & F . 4 = I5 & F . 5 = I6 & F . 6 = I7 & F . 7 = I8 & F . 8 = I9 )
proof
let F be NAT -defined the InstructionsF of SCM -valued total Function; ::_thesis: for I1, I2, I3, I4, I5, I6, I7, I8, I9 being Instruction of SCM st (((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%> c= F holds
( F . 0 = I1 & F . 1 = I2 & F . 2 = I3 & F . 3 = I4 & F . 4 = I5 & F . 5 = I6 & F . 6 = I7 & F . 7 = I8 & F . 8 = I9 )
let I1, I2, I3, I4, I5, I6, I7, I8, I9 be Instruction of SCM; ::_thesis: ( (((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%> c= F implies ( F . 0 = I1 & F . 1 = I2 & F . 2 = I3 & F . 3 = I4 & F . 4 = I5 & F . 5 = I6 & F . 6 = I7 & F . 7 = I8 & F . 8 = I9 ) )
assume A1: (((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%> c= F ; ::_thesis: ( F . 0 = I1 & F . 1 = I2 & F . 2 = I3 & F . 3 = I4 & F . 4 = I5 & F . 5 = I6 & F . 6 = I7 & F . 7 = I8 & F . 8 = I9 )
set I = (((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%>;
A2: ( ((((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%>) . 2 = I3 & ((((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%>) . 3 = I4 ) by AFINSQ_1:50;
A3: ( ((((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%>) . 6 = I7 & ((((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%>) . 7 = I8 ) by AFINSQ_1:50;
A4: ( ((((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%>) . 4 = I5 & ((((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%>) . 5 = I6 ) by AFINSQ_1:50;
A5: ( ((((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%>) . 8 = I9 & len ((((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%>) = 9 ) by AFINSQ_1:50;
 len ((((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%>) = 9 by AFINSQ_1:50;
then A6: ( 0 in dom ((((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%>) & 1 in dom ((((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%>) & 2 in dom ((((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%>) & 3 in dom ((((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%>) & 4 in dom ((((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%>) & 5 in dom ((((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%>) & 6 in dom ((((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%>) & 7 in dom ((((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%>) & 8 in dom ((((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%>) ) by ENUMSET1:def_7, CARD_1:57;
 ( ((((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%>) . 0 = I1 & ((((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%>) . 1 = I2 ) by AFINSQ_1:50;
hence  ( F . 0 = I1 & F . 1 = I2 & F . 2 = I3 & F . 3 = I4 & F . 4 = I5 & F . 5 = I6 & F . 6 = I7 & F . 7 = I8 & F . 8 = I9 ) by A2, A4, A3, A5, A6, A1, GRFUNC_1:2; ::_thesis: verum
end;

theorem :: FIB_FUSC:1
for F being NAT -defined the InstructionsF of SCM -valued total Function st Fib_Program c= F holds
for N being Element of NAT
for s being 0 -started State-consisting of <%1,N,0,0%> holds
( F halts_on s & ( N = 0 implies LifeSpan (F,s) = 1 ) & ( N > 0 implies LifeSpan (F,s) = (6 * N) - 2 ) & (Result (F,s)) . (dl. 3) = Fib N )
proof
let F be NAT -defined the InstructionsF of SCM -valued total Function; ::_thesis: ( Fib_Program c= F implies for N being Element of NAT
for s being 0 -started State-consisting of <%1,N,0,0%> holds
( F halts_on s & ( N = 0 implies LifeSpan (F,s) = 1 ) & ( N > 0 implies LifeSpan (F,s) = (6 * N) - 2 ) & (Result (F,s)) . (dl. 3) = Fib N ) )
assume A1: Fib_Program c= F ; ::_thesis: for N being Element of NAT
for s being 0 -started State-consisting of <%1,N,0,0%> holds
( F halts_on s & ( N = 0 implies LifeSpan (F,s) = 1 ) & ( N > 0 implies LifeSpan (F,s) = (6 * N) - 2 ) & (Result (F,s)) . (dl. 3) = Fib N )
let N be Element of NAT ; ::_thesis: for s being 0 -started State-consisting of <%1,N,0,0%> holds
( F halts_on s & ( N = 0 implies LifeSpan (F,s) = 1 ) & ( N > 0 implies LifeSpan (F,s) = (6 * N) - 2 ) & (Result (F,s)) . (dl. 3) = Fib N )
let s be 0 -started State-consisting of <%1,N,0,0%>; ::_thesis: ( F halts_on s & ( N = 0 implies LifeSpan (F,s) = 1 ) & ( N > 0 implies LifeSpan (F,s) = (6 * N) - 2 ) & (Result (F,s)) . (dl. 3) = Fib N )
set C1 = dl. 0;
set n = dl. 1;
set FP = dl. 2;
set FC = 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;
A2: ( IC s = 0 & F . 0 = (dl. 1) >0_goto 2 ) by A1, Lm17, MEMSTR_0:def_12;
set s1 = Comput (F,s,(0 + 1));
set s0 = Comput (F,s,0);
A3: s = Comput (F,s,0) by EXTPRO_1:2;
 s . (dl. 0) = 1 by SCM_1:1;
then A4: (Comput (F,s,(0 + 1))) . (dl. 0) = 1 by A2, A3, SCM_1:11;
A5: F . 3 = SubFrom ((dl. 1),(dl. 0)) by A1, Lm17;
 s . (dl. 2) = 0 by SCM_1:1;
then A6: (Comput (F,s,(0 + 1))) . (dl. 2) = 0 by A2, A3, SCM_1:11;
A7: F . 4 = (dl. 1) =0_goto 1 by A1, Lm17;
 s . (dl. 3) = 0 by SCM_1:1;
then A8: (Comput (F,s,(0 + 1))) . (dl. 3) = 0 by A2, A3, SCM_1:11;
A9: F . 6 = (dl. 2) := (dl. 3) by A1, Lm17;
defpred S1[ Element of NAT ] means ( $1 < N implies for u being State of SCM st u = Comput (F,s,((6 * $1) + 3)) holds
( u . (dl. 0) = 1 & u . (dl. 1) = (N - 1) - $1 & u . (dl. 2) = Fib $1 & u . (dl. 3) = Fib ($1 + 1) & IC u = 4 ) );
A10: F . 2 = (dl. 3) := (dl. 0) by A1, Lm17;
A11: F . 7 = AddTo ((dl. 3),(dl. 4)) by A1, Lm17;
A12: F . 8 = SCM-goto 3 by A1, Lm17;
A13: F . 5 = (dl. 4) := (dl. 2) by A1, Lm17;
A14: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume that
A15: ( k < N implies for u being State of SCM st u = Comput (F,s,((6 * k) + 3)) holds
( u . (dl. 0) = 1 & u . (dl. 1) = (N - 1) - k & u . (dl. 2) = Fib k & u . (dl. 3) = Fib (k + 1) & IC u = 4 ) ) and
A16: k + 1 < N ; ::_thesis: for u being State of SCM st u = Comput (F,s,((6 * (k + 1)) + 3)) holds
( u . (dl. 0) = 1 & u . (dl. 1) = (N - 1) - (k + 1) & u . (dl. 2) = Fib (k + 1) & u . (dl. 3) = Fib ((k + 1) + 1) & IC u = 4 )
set b = (6 * k) + 3;
set s5 = Comput (F,s,(((6 * k) + 3) + 1));
set s6 = Comput (F,s,((((6 * k) + 3) + 1) + 1));
set s7 = Comput (F,s,(((((6 * k) + 3) + 1) + 1) + 1));
set s8 = Comput (F,s,((((((6 * k) + 3) + 1) + 1) + 1) + 1));
set s9 = Comput (F,s,(((((((6 * k) + 3) + 1) + 1) + 1) + 1) + 1));
set s10 = Comput (F,s,((((((((6 * k) + 3) + 1) + 1) + 1) + 1) + 1) + 1));
set s4 = Comput (F,s,((6 * k) + 3));
A17: IC (Comput (F,s,((6 * k) + 3))) = 4 by A15, A16, NAT_1:13;
let t be State of SCM; ::_thesis: ( t = Comput (F,s,((6 * (k + 1)) + 3)) implies ( t . (dl. 0) = 1 & t . (dl. 1) = (N - 1) - (k + 1) & t . (dl. 2) = Fib (k + 1) & t . (dl. 3) = Fib ((k + 1) + 1) & IC t = 4 ) )
assume A18: t = Comput (F,s,((6 * (k + 1)) + 3)) ; ::_thesis: ( t . (dl. 0) = 1 & t . (dl. 1) = (N - 1) - (k + 1) & t . (dl. 2) = Fib (k + 1) & t . (dl. 3) = Fib ((k + 1) + 1) & IC t = 4 )
A19: (Comput (F,s,((6 * k) + 3))) . (dl. 1) = (N - 1) - k by A15, A16, NAT_1:13;
then  (Comput (F,s,((6 * k) + 3))) . (dl. 1) <> 0 by A16;
then A20: IC (Comput (F,s,(((6 * k) + 3) + 1))) = 4 + 1 by A7, A17, SCM_1:10;
then A21: IC (Comput (F,s,((((6 * k) + 3) + 1) + 1))) = 5 + 1 by A13, SCM_1:4;
then A22: IC (Comput (F,s,(((((6 * k) + 3) + 1) + 1) + 1))) = 6 + 1 by A9, SCM_1:4;
then A23: IC (Comput (F,s,((((((6 * k) + 3) + 1) + 1) + 1) + 1))) = 7 + 1 by A11, SCM_1:5;
then A24: IC (Comput (F,s,(((((((6 * k) + 3) + 1) + 1) + 1) + 1) + 1))) = 3 by A12, SCM_1:9;
then A25: IC (Comput (F,s,((((((((6 * k) + 3) + 1) + 1) + 1) + 1) + 1) + 1))) = 3 + 1 by A5, SCM_1:6;
 (Comput (F,s,((6 * k) + 3))) . (dl. 0) = 1 by A15, A16, NAT_1:13;
then  (Comput (F,s,(((6 * k) + 3) + 1))) . (dl. 0) = 1 by A7, A17, SCM_1:10;
then  (Comput (F,s,((((6 * k) + 3) + 1) + 1))) . (dl. 0) = 1 by A13, A20, Lm13, SCM_1:4;
then  (Comput (F,s,(((((6 * k) + 3) + 1) + 1) + 1))) . (dl. 0) = 1 by A9, A21, Lm8, SCM_1:4;
then  (Comput (F,s,((((((6 * k) + 3) + 1) + 1) + 1) + 1))) . (dl. 0) = 1 by A11, A22, Lm9, SCM_1:5;
then A26: (Comput (F,s,(((((((6 * k) + 3) + 1) + 1) + 1) + 1) + 1))) . (dl. 0) = 1 by A12, A23, SCM_1:9;
 (Comput (F,s,((6 * k) + 3))) . (dl. 3) = Fib (k + 1) by A15, A16, NAT_1:13;
then  (Comput (F,s,(((6 * k) + 3) + 1))) . (dl. 3) = Fib (k + 1) by A7, A17, SCM_1:10;
then A27: (Comput (F,s,((((6 * k) + 3) + 1) + 1))) . (dl. 3) = Fib (k + 1) by A13, A20, Lm16, SCM_1:4;
then A28: (Comput (F,s,(((((6 * k) + 3) + 1) + 1) + 1))) . (dl. 3) = Fib (k + 1) by A9, A21, Lm12, SCM_1:4;
 (Comput (F,s,((6 * k) + 3))) . (dl. 2) = Fib k by A15, A16, NAT_1:13;
then  (Comput (F,s,(((6 * k) + 3) + 1))) . (dl. 2) = Fib k by A7, A17, SCM_1:10;
then  (Comput (F,s,((((6 * k) + 3) + 1) + 1))) . (dl. 4) = Fib k by A13, A20, SCM_1:4;
then A29: (Comput (F,s,(((((6 * k) + 3) + 1) + 1) + 1))) . (dl. 4) = Fib k by A9, A21, Lm15, SCM_1:4;
(Comput (F,s,((((((6 * k) + 3) + 1) + 1) + 1) + 1))) . (dl. 3) = ((Comput (F,s,(((((6 * k) + 3) + 1) + 1) + 1))) . (dl. 4)) + ((Comput (F,s,(((((6 * k) + 3) + 1) + 1) + 1))) . (dl. 3)) by A11, A22, SCM_1:5
.= Fib ((k + 1) + 1) by A28, A29, PRE_FF:1 ;
then A30: (Comput (F,s,(((((((6 * k) + 3) + 1) + 1) + 1) + 1) + 1))) . (dl. 3) = Fib ((k + 1) + 1) by A12, A23, SCM_1:9;
 (Comput (F,s,(((((6 * k) + 3) + 1) + 1) + 1))) . (dl. 2) = Fib (k + 1) by A9, A21, A27, SCM_1:4;
then  (Comput (F,s,((((((6 * k) + 3) + 1) + 1) + 1) + 1))) . (dl. 2) = Fib (k + 1) by A11, A22, Lm12, SCM_1:5;
then A31: (Comput (F,s,(((((((6 * k) + 3) + 1) + 1) + 1) + 1) + 1))) . (dl. 2) = Fib (k + 1) by A12, A23, SCM_1:9;
 (Comput (F,s,(((6 * k) + 3) + 1))) . (dl. 1) = (N - 1) - k by A7, A19, A17, SCM_1:10;
then  (Comput (F,s,((((6 * k) + 3) + 1) + 1))) . (dl. 1) = (N - 1) - k by A13, A20, Lm14, SCM_1:4;
then  (Comput (F,s,(((((6 * k) + 3) + 1) + 1) + 1))) . (dl. 1) = (N - 1) - k by A9, A21, Lm10, SCM_1:4;
then  (Comput (F,s,((((((6 * k) + 3) + 1) + 1) + 1) + 1))) . (dl. 1) = (N - 1) - k by A11, A22, Lm11, SCM_1:5;
then  (Comput (F,s,(((((((6 * k) + 3) + 1) + 1) + 1) + 1) + 1))) . (dl. 1) = (N - 1) - k by A12, A23, SCM_1:9;
then  (Comput (F,s,((((((((6 * k) + 3) + 1) + 1) + 1) + 1) + 1) + 1))) . (dl. 1) = ((N - 1) - k) - 1 by A5, A24, A26, SCM_1:6;
hence  ( t . (dl. 0) = 1 & t . (dl. 1) = (N - 1) - (k + 1) & t . (dl. 2) = Fib (k + 1) & t . (dl. 3) = Fib ((k + 1) + 1) & IC t = 4 ) by A5, A18, A24, A26, A31, A30, A25, Lm7, Lm10, Lm11, SCM_1:6; ::_thesis: verum
end;
A32: F . 1 = halt SCM by A1, Lm17;
A33: s . (dl. 1) = N by SCM_1:1;
then A34: (Comput (F,s,(0 + 1))) . (dl. 1) = N by A2, A3, SCM_1:11;
A35: S1[ 0 ]
proof
set s3 = Comput (F,s,(2 + 1));
set s2 = Comput (F,s,(1 + 1));
assume  0 < N ; ::_thesis: for u being State of SCM st u = Comput (F,s,((6 * 0) + 3)) holds
( u . (dl. 0) = 1 & u . (dl. 1) = (N - 1) - 0 & u . (dl. 2) = Fib 0 & u . (dl. 3) = Fib (0 + 1) & IC u = 4 )
then A36: IC (Comput (F,s,(0 + 1))) = 2 by A2, A33, A3, SCM_1:11;
then A37: ( (Comput (F,s,(1 + 1))) . (dl. 3) = 1 & (Comput (F,s,(1 + 1))) . (dl. 0) = 1 ) by A10, A4, A8, SCM_1:4;
let t be State of SCM; ::_thesis: ( t = Comput (F,s,((6 * 0) + 3)) implies ( t . (dl. 0) = 1 & t . (dl. 1) = (N - 1) - 0 & t . (dl. 2) = Fib 0 & t . (dl. 3) = Fib (0 + 1) & IC t = 4 ) )
assume A38: t = Comput (F,s,((6 * 0) + 3)) ; ::_thesis: ( t . (dl. 0) = 1 & t . (dl. 1) = (N - 1) - 0 & t . (dl. 2) = Fib 0 & t . (dl. 3) = Fib (0 + 1) & IC t = 4 )
A39: ( (Comput (F,s,(1 + 1))) . (dl. 1) = N & (Comput (F,s,(1 + 1))) . (dl. 2) = 0 ) by A10, A34, A6, A36, Lm11, Lm12, SCM_1:4;
A40: IC (Comput (F,s,(1 + 1))) = 2 + 1 by A10, A36, SCM_1:4;
then  IC (Comput (F,s,(2 + 1))) = 3 + 1 by A5, SCM_1:6;
hence  ( t . (dl. 0) = 1 & t . (dl. 1) = (N - 1) - 0 & t . (dl. 2) = Fib 0 & t . (dl. 3) = Fib (0 + 1) & IC t = 4 ) by A5, A38, A37, A39, A40, Lm7, Lm10, Lm11, PRE_FF:1, SCM_1:6; ::_thesis: verum
end;
A41: for k being Element of NAT holds S1[k] from NAT_1:sch_1(A35, A14);
percases ( N = 0 or ex k being Nat st N = k + 1 ) by NAT_1:6;
supposeA42: N = 0 ; ::_thesis: ( F halts_on s & ( N = 0 implies LifeSpan (F,s) = 1 ) & ( N > 0 implies LifeSpan (F,s) = (6 * N) - 2 ) & (Result (F,s)) . (dl. 3) = Fib N )
then A43: F . (IC (Comput (F,s,(0 + 1)))) = halt SCM by A2, A32, A33, A3, SCM_1:11;
hence  F halts_on s by EXTPRO_1:30; ::_thesis: ( ( N = 0 implies LifeSpan (F,s) = 1 ) & ( N > 0 implies LifeSpan (F,s) = (6 * N) - 2 ) & (Result (F,s)) . (dl. 3) = Fib N )
hereby  ::_thesis: ( ( N > 0 implies LifeSpan (F,s) = (6 * N) - 2 ) & (Result (F,s)) . (dl. 3) = Fib N )
assume  N = 0 ; ::_thesis: LifeSpan (F,s) = 1
 halt SCM <> (dl. 1) >0_goto 2 by SCM_1:12;
hence  LifeSpan (F,s) = 1 by A2, A3, A43, EXTPRO_1:33; ::_thesis: verum
end;
thus  ( N > 0 implies LifeSpan (F,s) = (6 * N) - 2 ) by A42; ::_thesis: (Result (F,s)) . (dl. 3) = Fib N
thus  (Result (F,s)) . (dl. 3) = Fib N by A8, A42, A43, EXTPRO_1:31, PRE_FF:1; ::_thesis: verum
end;
suppose ex k being Nat st N = k + 1 ; ::_thesis: ( F halts_on s & ( N = 0 implies LifeSpan (F,s) = 1 ) & ( N > 0 implies LifeSpan (F,s) = (6 * N) - 2 ) & (Result (F,s)) . (dl. 3) = Fib N )
then consider k being Nat such that
A44: N = k + 1 ;
reconsider k = k as Element of NAT by ORDINAL1:def_12;
set r = Comput (F,s,((6 * k) + 3));
A45: k < N by A44, NAT_1:13;
then A46: IC (Comput (F,s,((6 * k) + 3))) = 4 by A41;
A47: (Comput (F,s,((6 * k) + 3))) . (dl. 3) = Fib (k + 1) by A41, A45;
set t = Comput (F,s,(((6 * k) + 3) + 1));
(Comput (F,s,((6 * k) + 3))) . (dl. 1) = (k + (1 - 1)) - k by A41, A44, A45
.= 0 ;
then A48: IC (Comput (F,s,(((6 * k) + 3) + 1))) = 1 by A7, A46, SCM_1:10;
hence  F halts_on s by A32, EXTPRO_1:30; ::_thesis: ( ( N = 0 implies LifeSpan (F,s) = 1 ) & ( N > 0 implies LifeSpan (F,s) = (6 * N) - 2 ) & (Result (F,s)) . (dl. 3) = Fib N )
thus  ( N = 0 implies LifeSpan (F,s) = 1 ) by A44, NAT_1:5; ::_thesis: ( ( N > 0 implies LifeSpan (F,s) = (6 * N) - 2 ) & (Result (F,s)) . (dl. 3) = Fib N )
thus  ( N > 0 implies LifeSpan (F,s) = (6 * N) - 2 ) by A32, A44, A46, A48, EXTPRO_1:33; ::_thesis: (Result (F,s)) . (dl. 3) = Fib N
thus (Result (F,s)) . (dl. 3) = (Comput (F,s,(((6 * k) + 3) + 1))) . (dl. 3) by A32, A48, EXTPRO_1:31
.= Fib N by A7, A44, A47, A46, SCM_1:10 ; ::_thesis: verum
end;
end;
end;

definition
let i be Integer;
func Fusc' i ->  Element of NAT  means :Def2: :: FIB_FUSC:def 2
( ex n being Element of NAT st
( i = n & it = Fusc n ) or ( i is not Element of NAT & it = 0 ) );
existence
 ex b1 being Element of NAT st
( ex n being Element of NAT st
( i = n & b1 = Fusc n ) or ( i is not Element of NAT & b1 = 0 ) )
proof
percases ( i is Element of NAT or not i is Element of NAT ) ;
suppose i is Element of NAT ; ::_thesis: ex b1 being Element of NAT st
( ex n being Element of NAT st
( i = n & b1 = Fusc n ) or ( i is not Element of NAT & b1 = 0 ) )
then reconsider n = i as Element of NAT ;
take  Fusc n ; ::_thesis: ( ex n being Element of NAT st
( i = n & Fusc n = Fusc n ) or ( i is not Element of NAT & Fusc n = 0 ) )
thus  ( ex n being Element of NAT st
( i = n & Fusc n = Fusc n ) or ( i is not Element of NAT & Fusc n = 0 ) ) ; ::_thesis: verum
end;
suppose i is not Element of NAT ; ::_thesis: ex b1 being Element of NAT st
( ex n being Element of NAT st
( i = n & b1 = Fusc n ) or ( i is not Element of NAT & b1 = 0 ) )
hence  ex b1 being Element of NAT st
( ex n being Element of NAT st
( i = n & b1 = Fusc n ) or ( i is not Element of NAT & b1 = 0 ) ) ; ::_thesis: verum
end;
end;
end;
uniqueness
 for b1, b2 being Element of NAT st ( ex n being Element of NAT st
( i = n & b1 = Fusc n ) or ( i is not Element of NAT & b1 = 0 ) ) & ( ex n being Element of NAT st
( i = n & b2 = Fusc n ) or ( i is not Element of NAT & b2 = 0 ) ) holds
b1 = b2 ;
end;

:: deftheorem Def2 defines Fusc' FIB_FUSC:def_2_:_
 for i being Integer
for b2 being Element of NAT holds
( b2 = Fusc' i iff ( ex n being Element of NAT st
( i = n & b2 = Fusc n ) or ( i is not Element of NAT & b2 = 0 ) ) );

definition
func Fusc_Program  ->  XFinSequence of  equals :: FIB_FUSC:def 3
(((((((<%((dl. 1) =0_goto 8)%> ^ <%((dl. 4) := (dl. 0))%>) ^ <%(Divide ((dl. 1),(dl. 4)))%>) ^ <%((dl. 4) =0_goto 6)%>) ^ <%(AddTo ((dl. 3),(dl. 2)))%>) ^ <%(SCM-goto 0)%>) ^ <%(AddTo ((dl. 2),(dl. 3)))%>) ^ <%(SCM-goto 0)%>) ^ <%(halt SCM)%>;
coherence
 (((((((<%((dl. 1) =0_goto 8)%> ^ <%((dl. 4) := (dl. 0))%>) ^ <%(Divide ((dl. 1),(dl. 4)))%>) ^ <%((dl. 4) =0_goto 6)%>) ^ <%(AddTo ((dl. 3),(dl. 2)))%>) ^ <%(SCM-goto 0)%>) ^ <%(AddTo ((dl. 2),(dl. 3)))%>) ^ <%(SCM-goto 0)%>) ^ <%(halt SCM)%> is XFinSequence of ;
end;

:: deftheorem  defines Fusc_Program FIB_FUSC:def_3_:_
 Fusc_Program = (((((((<%((dl. 1) =0_goto 8)%> ^ <%((dl. 4) := (dl. 0))%>) ^ <%(Divide ((dl. 1),(dl. 4)))%>) ^ <%((dl. 4) =0_goto 6)%>) ^ <%(AddTo ((dl. 3),(dl. 2)))%>) ^ <%(SCM-goto 0)%>) ^ <%(AddTo ((dl. 2),(dl. 3)))%>) ^ <%(SCM-goto 0)%>) ^ <%(halt SCM)%>;

theorem :: FIB_FUSC:2
for F being NAT -defined the InstructionsF of SCM -valued total Function st Fusc_Program c= F holds
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 )
proof
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, XXREAL_0:2;
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[ 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))) ) );
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 Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of 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 ;
percases ( (Comput (F,s,((6 * k) + 3))) . (dl. 4) <> 0 or (Comput (F,s,((6 * k) + 3))) . (dl. 4) = 0 ) ;
supposeA41: (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;
supposeA52: (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 Element of NAT holds S1[k] from NAT_1:sch_1(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, NAT_1:2, 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:31; ::_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
end;

theorem :: FIB_FUSC:3
for F being NAT -defined the InstructionsF of SCM -valued total Function st Fib_Program c= F holds
for N, k, Fk, Fk1 being Element of NAT
for s being 3 -started State-consisting of <%1,N,Fk,Fk1%> st N > 0 & Fk = Fib k & Fk1 = Fib (k + 1) holds
( F halts_on s & LifeSpan (F,s) = (6 * N) - 4 & ex m being Element of NAT st
( m = (k + N) - 1 & (Result (F,s)) . (dl. 2) = Fib m & (Result (F,s)) . (dl. 3) = Fib (m + 1) ) )
proof
let F be NAT -defined the InstructionsF of SCM -valued total Function; ::_thesis: ( Fib_Program c= F implies for N, k, Fk, Fk1 being Element of NAT
for s being 3 -started State-consisting of <%1,N,Fk,Fk1%> st N > 0 & Fk = Fib k & Fk1 = Fib (k + 1) holds
( F halts_on s & LifeSpan (F,s) = (6 * N) - 4 & ex m being Element of NAT st
( m = (k + N) - 1 & (Result (F,s)) . (dl. 2) = Fib m & (Result (F,s)) . (dl. 3) = Fib (m + 1) ) ) )
assume A1: Fib_Program c= F ; ::_thesis: for N, k, Fk, Fk1 being Element of NAT
for s being 3 -started State-consisting of <%1,N,Fk,Fk1%> st N > 0 & Fk = Fib k & Fk1 = Fib (k + 1) holds
( F halts_on s & LifeSpan (F,s) = (6 * N) - 4 & ex m being Element of NAT st
( m = (k + N) - 1 & (Result (F,s)) . (dl. 2) = Fib m & (Result (F,s)) . (dl. 3) = Fib (m + 1) ) )
defpred S1[ Element of NAT ] means  for k, Fk, Fk1 being Element of NAT
for s being 3 -started State-consisting of <%1,$1,Fk,Fk1%> st $1 > 0 & Fk = Fib k & Fk1 = Fib (k + 1) holds
( F halts_on s & LifeSpan (F,s) = (6 * $1) - 4 & ex m being Element of NAT st
( m = (k + $1) - 1 & (Result (F,s)) . (dl. 2) = Fib m & (Result (F,s)) . (dl. 3) = Fib (m + 1) ) );
A2: for N being Element of NAT st S1[N] holds
S1[N + 1]
proof
set C1 = dl. 0;
set n = dl. 1;
set FP = dl. 2;
set FC = dl. 3;
set AUX = dl. 4;
let N be Element of NAT ; ::_thesis: ( S1[N] implies S1[N + 1] )
assume A3: S1[N] ; ::_thesis: S1[N + 1]
A4: N >= 0 by NAT_1:2;
let k, Fk, Fk1 be Element of NAT ; ::_thesis: for s being 3 -started State-consisting of <%1,(N + 1),Fk,Fk1%> st N + 1 > 0 & Fk = Fib k & Fk1 = Fib (k + 1) holds
( F halts_on s & LifeSpan (F,s) = (6 * (N + 1)) - 4 & ex m being Element of NAT st
( m = (k + (N + 1)) - 1 & (Result (F,s)) . (dl. 2) = Fib m & (Result (F,s)) . (dl. 3) = Fib (m + 1) ) )
let s be 3 -started State-consisting of <%1,(N + 1),Fk,Fk1%>; ::_thesis: ( N + 1 > 0 & Fk = Fib k & Fk1 = Fib (k + 1) implies ( F halts_on s & LifeSpan (F,s) = (6 * (N + 1)) - 4 & ex m being Element of NAT st
( m = (k + (N + 1)) - 1 & (Result (F,s)) . (dl. 2) = Fib m & (Result (F,s)) . (dl. 3) = Fib (m + 1) ) ) )
assume that
 N + 1 > 0 and
A5: Fk = Fib k and
A6: Fk1 = Fib (k + 1) ; ::_thesis: ( F halts_on s & LifeSpan (F,s) = (6 * (N + 1)) - 4 & ex m being Element of NAT st
( m = (k + (N + 1)) - 1 & (Result (F,s)) . (dl. 2) = Fib m & (Result (F,s)) . (dl. 3) = Fib (m + 1) ) )
A7: F . 3 = SubFrom ((dl. 1),(dl. 0)) by A1, Lm17;
set s0 = Comput (F,s,0);
set s1 = Comput (F,s,(0 + 1));
A8: F . 1 = halt SCM by A1, Lm17;
A9: ( IC s = 3 & s = Comput (F,s,0) ) by EXTPRO_1:2, MEMSTR_0:def_12;
then A10: IC (Comput (F,s,(0 + 1))) = 3 + 1 by A7, SCM_1:6
.= 4 ;
set s2 = Comput (F,s,(1 + 1));
A11: F . 4 = (dl. 1) =0_goto 1 by A1, Lm17;
 s . (dl. 3) = Fk1 by SCM_1:1;
then  (Comput (F,s,(0 + 1))) . (dl. 3) = Fk1 by A7, A9, Lm11, SCM_1:6;
then A12: (Comput (F,s,(1 + 1))) . (dl. 3) = Fk1 by A11, A10, SCM_1:10;
A13: F . 7 = AddTo ((dl. 3),(dl. 4)) by A1, Lm17;
 s . (dl. 2) = Fk by SCM_1:1;
then  (Comput (F,s,(0 + 1))) . (dl. 2) = Fk by A7, A9, Lm10, SCM_1:6;
then A14: (Comput (F,s,(1 + 1))) . (dl. 2) = Fk by A11, A10, SCM_1:10;
A15: F . 6 = (dl. 2) := (dl. 3) by A1, Lm17;
A16: s . (dl. 0) = 1 by SCM_1:1;
then  (Comput (F,s,(0 + 1))) . (dl. 0) = 1 by A7, A9, Lm7, SCM_1:6;
then A17: (Comput (F,s,(1 + 1))) . (dl. 0) = 1 by A11, A10, SCM_1:10;
 s . (dl. 1) = N + 1 by SCM_1:1;
then A18: (Comput (F,s,(0 + 1))) . (dl. 1) = (N + 1) - 1 by A7, A16, A9, SCM_1:6
.= N ;
then A19: (Comput (F,s,(1 + 1))) . (dl. 1) = N by A11, A10, SCM_1:10;
A20: F . 5 = (dl. 4) := (dl. 2) by A1, Lm17;
A21: F . 8 = SCM-goto 3 by A1, Lm17;
percases ( N = 0 or N > 0 ) by A4, XXREAL_0:1;
supposeA22: N = 0 ; ::_thesis: ( F halts_on s & LifeSpan (F,s) = (6 * (N + 1)) - 4 & ex m being Element of NAT st
( m = (k + (N + 1)) - 1 & (Result (F,s)) . (dl. 2) = Fib m & (Result (F,s)) . (dl. 3) = Fib (m + 1) ) )
then A23: F . (IC (Comput (F,s,(1 + 1)))) = halt SCM by A8, A11, A18, A10, SCM_1:10;
hence  F halts_on s by EXTPRO_1:30; ::_thesis: ( LifeSpan (F,s) = (6 * (N + 1)) - 4 & ex m being Element of NAT st
( m = (k + (N + 1)) - 1 & (Result (F,s)) . (dl. 2) = Fib m & (Result (F,s)) . (dl. 3) = Fib (m + 1) ) )
 F . (IC (Comput (F,s,(0 + 1)))) <> halt SCM by A11, A10, SCM_1:12;
hence  LifeSpan (F,s) = (6 * (N + 1)) - 4 by A22, A23, EXTPRO_1:32; ::_thesis: ex m being Element of NAT st
( m = (k + (N + 1)) - 1 & (Result (F,s)) . (dl. 2) = Fib m & (Result (F,s)) . (dl. 3) = Fib (m + 1) )
take m = k; ::_thesis: ( m = (k + (N + 1)) - 1 & (Result (F,s)) . (dl. 2) = Fib m & (Result (F,s)) . (dl. 3) = Fib (m + 1) )
thus  m = (k + (N + 1)) - 1 by A22; ::_thesis: ( (Result (F,s)) . (dl. 2) = Fib m & (Result (F,s)) . (dl. 3) = Fib (m + 1) )
thus  ( (Result (F,s)) . (dl. 2) = Fib m & (Result (F,s)) . (dl. 3) = Fib (m + 1) ) by A5, A6, A14, A12, A23, EXTPRO_1:31; ::_thesis: verum
end;
supposeA24: N > 0 ; ::_thesis: ( F halts_on s & LifeSpan (F,s) = (6 * (N + 1)) - 4 & ex m being Element of NAT st
( m = (k + (N + 1)) - 1 & (Result (F,s)) . (dl. 2) = Fib m & (Result (F,s)) . (dl. 3) = Fib (m + 1) ) )
then A25: (6 * N) - 4 > 0 by Lm6;
set Fk2 = Fib ((k + 1) + 1);
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));
A26: IC (Comput (F,s,(1 + 1))) = 4 + 1 by A11, A18, A10, A24, SCM_1:10;
then A27: IC (Comput (F,s,(2 + 1))) = 5 + 1 by A20, SCM_1:4;
then A28: IC (Comput (F,s,(3 + 1))) = 6 + 1 by A15, SCM_1:4;
then A29: IC (Comput (F,s,(4 + 1))) = 7 + 1 by A13, SCM_1:5;
A30: (Comput (F,s,(2 + 1))) . (dl. 3) = Fib (k + 1) by A6, A20, A12, A26, Lm16, SCM_1:4;
then A31: (Comput (F,s,(3 + 1))) . (dl. 3) = Fib (k + 1) by A15, A27, Lm12, SCM_1:4;
 (Comput (F,s,(3 + 1))) . (dl. 2) = Fib (k + 1) by A15, A27, A30, SCM_1:4;
then  (Comput (F,s,(4 + 1))) . (dl. 2) = Fib (k + 1) by A13, A28, Lm12, SCM_1:5;
then A32: (Comput (F,s,(5 + 1))) . (dl. 2) = Fib (k + 1) by A21, A29, SCM_1:9;
 (Comput (F,s,(2 + 1))) . (dl. 0) = 1 by A20, A17, A26, Lm13, SCM_1:4;
then  (Comput (F,s,(3 + 1))) . (dl. 0) = 1 by A15, A27, Lm8, SCM_1:4;
then  (Comput (F,s,(4 + 1))) . (dl. 0) = 1 by A13, A28, Lm9, SCM_1:5;
then A33: (Comput (F,s,(5 + 1))) . (dl. 0) = 1 by A21, A29, SCM_1:9;
 (Comput (F,s,(2 + 1))) . (dl. 4) = Fib k by A5, A20, A14, A26, SCM_1:4;
then A34: (Comput (F,s,(3 + 1))) . (dl. 4) = Fib k by A15, A27, Lm15, SCM_1:4;
(Comput (F,s,(4 + 1))) . (dl. 3) = ((Comput (F,s,(3 + 1))) . (dl. 4)) + ((Comput (F,s,(3 + 1))) . (dl. 3)) by A13, A28, SCM_1:5
.= Fib ((k + 1) + 1) by A31, A34, PRE_FF:1 ;
then A35: (Comput (F,s,(5 + 1))) . (dl. 3) = Fib ((k + 1) + 1) by A21, A29, SCM_1:9;
 (Comput (F,s,(2 + 1))) . (dl. 1) = N by A20, A19, A26, Lm14, SCM_1:4;
then  (Comput (F,s,(3 + 1))) . (dl. 1) = N by A15, A27, Lm10, SCM_1:4;
then  (Comput (F,s,(4 + 1))) . (dl. 1) = N by A13, A28, Lm11, SCM_1:5;
then A36: (Comput (F,s,(5 + 1))) . (dl. 1) = N by A21, A29, SCM_1:9;
 IC (Comput (F,s,(5 + 1))) = 3 by A21, A29, SCM_1:9;
then A37: Comput (F,s,(5 + 1)) is 3 -started State-consisting of <%1,N,Fk1,(Fib ((k + 1) + 1))%> by A6, A33, A36, A32, A35, MEMSTR_0:def_12, SCM_1:13;
then consider m being Element of NAT  such that
A38: m = ((k + 1) + N) - 1 and
 (Result (F,(Comput (F,s,(5 + 1))))) . (dl. 2) = Fib m and
 (Result (F,(Comput (F,s,(5 + 1))))) . (dl. 3) = Fib (m + 1) by A3, A6, A24;
 F halts_on Comput (F,s,(5 + 1)) by A3, A6, A24, A37;
hence  F halts_on s by EXTPRO_1:22; ::_thesis: ( LifeSpan (F,s) = (6 * (N + 1)) - 4 & ex m being Element of NAT st
( m = (k + (N + 1)) - 1 & (Result (F,s)) . (dl. 2) = Fib m & (Result (F,s)) . (dl. 3) = Fib (m + 1) ) )
 LifeSpan (F,(Comput (F,s,(5 + 1)))) = (6 * N) - 4 by A3, A6, A24, A37;
hence  LifeSpan (F,s) = 6 + ((6 * N) - 4) by A3, A6, A24, A37, A25, EXTPRO_1:34
.= (6 * (N + 1)) - 4 ;
::_thesis: ex m being Element of NAT st
( m = (k + (N + 1)) - 1 & (Result (F,s)) . (dl. 2) = Fib m & (Result (F,s)) . (dl. 3) = Fib (m + 1) )
take  m ; ::_thesis: ( m = (k + (N + 1)) - 1 & (Result (F,s)) . (dl. 2) = Fib m & (Result (F,s)) . (dl. 3) = Fib (m + 1) )
thus  m = (k + (N + 1)) - 1 by A38; ::_thesis: ( (Result (F,s)) . (dl. 2) = Fib m & (Result (F,s)) . (dl. 3) = Fib (m + 1) )
 ex m being Element of NAT st
( m = ((k + 1) + N) - 1 & (Result (F,(Comput (F,s,(5 + 1))))) . (dl. 2) = Fib m & (Result (F,(Comput (F,s,(5 + 1))))) . (dl. 3) = Fib (m + 1) ) by A3, A6, A24, A37;
hence  ( (Result (F,s)) . (dl. 2) = Fib m & (Result (F,s)) . (dl. 3) = Fib (m + 1) ) by A38, A3, A6, A24, A37, EXTPRO_1:35; ::_thesis: verum
end;
end;
end;
A40: S1[ 0 ] ;
thus  for N being Element of NAT holds S1[N] from NAT_1:sch_1(A40, A2); ::_thesis: verum
end;

theorem Th4: :: FIB_FUSC:4
for F being NAT -defined the InstructionsF of SCM -valued total Function st Fusc_Program c= F holds
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 ) )
proof
let F be NAT -defined the InstructionsF of SCM -valued total Function; ::_thesis: ( Fusc_Program c= F implies 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 ) ) )
assume A1: Fusc_Program c= F ; ::_thesis: 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 ) )
defpred S1[ 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
S1[n] ) holds
S1[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: ( ( for n being Nat st n < nn holds
S1[n] ) implies S1[nn] )
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: S1[nn]
reconsider n2 = nn as Element of NAT by ORDINAL1:def_12;
let N, A, B be Element of NAT ; ::_thesis: for s being 0 -started State-consisting of <%2,nn,A,B%> st N > 0 & Fusc N = (A * (Fusc nn)) + (B * (Fusc (nn + 1))) holds
( 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 ) )
let s be 0 -started State-consisting of <%2,nn,A,B%>; ::_thesis: ( N > 0 & Fusc N = (A * (Fusc nn)) + (B * (Fusc (nn + 1))) implies ( 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 ) ) )
assume that
A4: N > 0 and
A5: Fusc N = (A * (Fusc nn)) + (B * (Fusc (nn + 1))) ; ::_thesis: ( 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 ) )
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:_(_nn_=_0_implies_(_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_)_)_)
assume A16: nn = 0 ; ::_thesis: ( 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 ) )
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: ( (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 ) )
thus (Result (F,s)) . (dl. 3) = (Comput (F,s,(0 + 1))) . (dl. 3) by A17, EXTPRO_1:31
.= Fusc N by A5, A14, A16, PRE_FF:18 ; ::_thesis: ( ( nn = 0 implies LifeSpan (F,s) = 1 ) & ( nn > 0 implies LifeSpan (F,s) = (6 * ([\(log (2,nn))/] + 1)) + 1 ) )
hereby  ::_thesis: ( nn > 0 implies LifeSpan (F,s) = (6 * ([\(log (2,nn))/] + 1)) + 1 )
assume  nn = 0 ; ::_thesis: LifeSpan (F,s) = 1
 halt SCM <> (dl. 1) =0_goto 8 by SCM_1:12;
hence  LifeSpan (F,s) = 1 by A7, A10, A17, EXTPRO_1:33; ::_thesis: verum
end;
thus  ( nn > 0 implies LifeSpan (F,s) = (6 * ([\(log (2,nn))/] + 1)) + 1 ) by A16; ::_thesis: verum
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:_(_nn_>_0_implies_(_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_)_)_)
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: ( 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 ) )
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;
percases ( (Comput (F,s,(2 + 1))) . (dl. 4) <> 0 or (Comput (F,s,(2 + 1))) . (dl. 4) = 0 ) ;
supposeA36: (Comput (F,s,(2 + 1))) . (dl. 4) <> 0 ; ::_thesis: ( 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 ) )
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,s)) . (dl. 3) = Fusc N & ( nn = 0 implies LifeSpan (F,s) = 1 ) & ( nn > 0 implies LifeSpan (F,s) = (6 * ([\(log (2,nn))/] + 1)) + 1 ) )
 (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: ( ( nn = 0 implies LifeSpan (F,s) = 1 ) & ( nn > 0 implies LifeSpan (F,s) = (6 * ([\(log (2,nn))/] + 1)) + 1 ) )
thus  ( nn = 0 implies LifeSpan (F,s) = 1 ) by A26; ::_thesis: ( nn > 0 implies LifeSpan (F,s) = (6 * ([\(log (2,nn))/] + 1)) + 1 )
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: verum
proof
assume  nn > 0 ; ::_thesis: LifeSpan (F,s) = (6 * ([\(log (2,nn))/] + 1)) + 1
percases ( nn9 = 0 or nn9 <> 0 ) ;
suppose nn9 = 0 ; ::_thesis: LifeSpan (F,s) = (6 * ([\(log (2,nn))/] + 1)) + 1
hence  LifeSpan (F,s) = (6 * ([\(log (2,nn))/] + 1)) + 1 by A34, A35, A25, A42, A50, A51, Lm1, EXTPRO_1:34; ::_thesis: verum
end;
supposeA52: nn9 <> 0 ; ::_thesis: LifeSpan (F,s) = (6 * ([\(log (2,nn))/] + 1)) + 1
then A53: nn9 > 0 by NAT_1:3;
then reconsider m = [\(log (2,nn9))/] as Element of NAT by Lm2;
 (6 * (m + 1)) + 1 > 0 by A53, Lm2;
hence  LifeSpan (F,s) = 6 + ((6 * (m + 1)) + 1) by A50, A49, A52, EXTPRO_1:34, NAT_1:3
.= (6 * ([\(log (2,nn))/] + 1)) + 1 by A34, A35, A42, A46, A53, Lm3 ;
::_thesis: verum
end;
end;
end;
end;
supposeA54: (Comput (F,s,(2 + 1))) . (dl. 4) = 0 ; ::_thesis: ( 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 ) )
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,s)) . (dl. 3) = Fusc N & ( nn = 0 implies LifeSpan (F,s) = 1 ) & ( nn > 0 implies LifeSpan (F,s) = (6 * ([\(log (2,nn))/] + 1)) + 1 ) )
 (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: ( ( nn = 0 implies LifeSpan (F,s) = 1 ) & ( nn > 0 implies LifeSpan (F,s) = (6 * ([\(log (2,nn))/] + 1)) + 1 ) )
thus  ( nn = 0 implies LifeSpan (F,s) = 1 ) by A26; ::_thesis: ( nn > 0 implies LifeSpan (F,s) = (6 * ([\(log (2,nn))/] + 1)) + 1 )
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: verum
proof
assume  nn > 0 ; ::_thesis: LifeSpan (F,s) = (6 * ([\(log (2,nn))/] + 1)) + 1
percases ( nn9 = 0 or nn9 <> 0 ) ;
suppose nn9 = 0 ; ::_thesis: LifeSpan (F,s) = (6 * ([\(log (2,nn))/] + 1)) + 1
hence  LifeSpan (F,s) = (6 * ([\(log (2,nn))/] + 1)) + 1 by A13, A26, A28, A33, A34, A25, A54, Lm14, SCM_1:8; ::_thesis: verum
end;
supposeA66: nn9 <> 0 ; ::_thesis: LifeSpan (F,s) = (6 * ([\(log (2,nn))/] + 1)) + 1
then A67: nn9 > 0 by NAT_1:3;
then reconsider m = [\(log (2,nn9))/] as Element of NAT by Lm2;
 (6 * (m + 1)) + 1 > 0 by A67, Lm2;
hence  LifeSpan (F,s) = 6 + ((6 * (m + 1)) + 1) by A64, A65, A66, EXTPRO_1:34, NAT_1:3
.= (6 * ([\(log (2,nn))/] + 1)) + 1 by A34, A35, A25, A54, A67, Lm5 ;
::_thesis: verum
end;
end;
end;
end;
end;
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 A15, A24, XXREAL_0:1; ::_thesis: verum
end;
 for n being Nat holds S1[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: verum
end;

theorem :: FIB_FUSC:5
for F being NAT -defined the InstructionsF of SCM -valued total Function st Fusc_Program c= F holds
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 & ( N = 0 implies LifeSpan (F,s) = 1 ) & ( N > 0 implies LifeSpan (F,s) = (6 * ([\(log (2,N))/] + 1)) + 1 ) )
proof
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 & ( N = 0 implies LifeSpan (F,s) = 1 ) & ( N > 0 implies LifeSpan (F,s) = (6 * ([\(log (2,N))/] + 1)) + 1 ) ) )
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 & ( N = 0 implies LifeSpan (F,s) = 1 ) & ( N > 0 implies 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 & ( N = 0 implies LifeSpan (F,s) = 1 ) & ( N > 0 implies LifeSpan (F,s) = (6 * ([\(log (2,N))/] + 1)) + 1 ) ) )
 Fusc N = (1 * (Fusc N)) + (0 * (Fusc (N + 1))) ;
hence  ( 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 & ( N = 0 implies LifeSpan (F,s) = 1 ) & ( N > 0 implies LifeSpan (F,s) = (6 * ([\(log (2,N))/] + 1)) + 1 ) ) ) by A1, Th4; ::_thesis: verum
end;