:: Two Programs for {\bf SCM}. Part II - Proofs
::  by Grzegorz Bancerek and Piotr Rudnicki
::
:: Received October 8, 1993
:: Copyright (c) 1993-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, CARD_1, INT_1, POWER, SUBSET_1, XXREAL_0, RELAT_1,
      ARYTM_3, ARYTM_1, NAT_1, AMI_3, AFINSQ_1, AMI_1, ORDINAL4, GRAPHSP,
      SCM_1, FINSEQ_1, MSUALG_1, FUNCT_1, PRE_FF, FSM_1, NEWTON, FIB_FUSC,
      EXTPRO_1, PARTFUN1, TARSKI;
 notations ENUMSET1, XCMPLX_0, SUBSET_1, NUMBERS, INT_1, ORDINAL1, NAT_1,
      NEWTON, POWER, RELAT_1, FUNCT_1, PARTFUN1, AFINSQ_1, FINSEQ_1, MEMSTR_0,
      COMPOS_1, EXTPRO_1, SCM_1, AMI_3, PRE_FF, XXREAL_0;
 constructors REAL_1, NEWTON, POWER, PRE_FF, SCM_1, ENUMSET1, PRE_POLY;
 registrations XREAL_0, INT_1, AMI_3, ORDINAL1, AFINSQ_1, SCM_1, PBOOLE,
      COMPOS_0;
 requirements REAL, NUMERALS, SUBSET, ARITHM, BOOLE;
 theorems NAT_1, INT_1, POWER, NEWTON, SCM_1, PRE_FF, AMI_3, XREAL_1, XXREAL_0,
      ORDINAL1, EXTPRO_1, AFINSQ_1, GRFUNC_1, CARD_1, ENUMSET1, MEMSTR_0;
 schemes NAT_1;

begin

Lm1: 0 = [\ log(2, 1) /]
proof
  thus 0 = [\ 0 /] by INT_1:25
    .= [\ log(2, 1) /] by POWER:51;
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;
  assume nn9 > 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;
  6 * F + 6 * 1 >= 0 by NAT_1:12;
  hence thesis by NAT_1:13;
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 such that
A1: nn = 2*nn9+1 & nn9 > 0;
  set F = [\ log(2, nn9) /];
  thus 6 + (6 * (F+1)+1) = 6 * (1 + (F + 1)) + 1
    .= 6 * ([\ log(2, nn) /] + 1) + 1 by A1,PRE_FF:14;
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;
  assume n > 0;
  hence log (2,2*n) = log (2,2)+log (2, n) by POWER:53
    .= 1+log (2, n) by POWER:52;
  hence thesis;
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 such that
A1: nn = 2*nn9 & nn9 > 0;
  set F = [\ log(2, nn9) /];
  thus 6 + (6 * (F+1)+1) = 6 * (1 + (F + 1)) + 1
    .= 6 * (1 + [\ log(2, nn9)+1 /]) + 1 by INT_1:28
    .= 6 * ([\ log(2, nn) /] + 1) + 1 by A1,Lm4;
end;

Lm6: for N being Element of NAT st N <> 0 holds 6*N - 4 > 0
proof
  let N be Element of NAT;
  assume N<>0;
  then consider L being Nat such that
A1: N = L+1 by NAT_1:6;
  reconsider L as Element of NAT by ORDINAL1:def 12;
  6 * L + 2 <> 0 by NAT_1:7;
  hence thesis by A1,NAT_1:3;
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 the InstructionsF of SCM equals
  <% 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;
end;

reserve F for total
 NAT-defined (the InstructionsF of SCM)-valued Function;

Lm17:
  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 I1, I2, I3, I4, I5, I6, I7, I8, I9 be Instruction of SCM such that
A1:   <%I1%>^<%I2%>^<%I3%>^<%I4%>^<%I5%>^<%I6%>^<%I7%>^<%I8%>^<%I9%> c= F;
  set I = <%I1%>^<%I2%>^<%I3%>^<%I4%>^<%I5%>^<%I6%>^<%I7%>^<%I8%>^<%I9%>;
A2: I.2 = I3 & I.3 = I4 by AFINSQ_1:50;
A3: I.6 = I7 & I.7 = I8 by AFINSQ_1:50;
A4: I.4=I5 & I.5 = I6 by AFINSQ_1:50;
A5: I.8 = I9 & len I=9 by AFINSQ_1:50;
    len I = 9 by AFINSQ_1:50;
    then
A6: 0 in dom I & 1 in dom I & 2 in dom I & 3 in dom I &
    4 in dom I & 5 in dom I & 6 in dom I & 7 in dom I &
    8 in dom I by ENUMSET1:def 7,CARD_1:57;
  I.0 = I1 & I.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;
end;

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

:: Fusc

definition
  let i be Integer;
  func Fusc' i -> Element of NAT means
  :Def2:
  (ex n being Element of NAT st i = n & it = Fusc n) or
  i is not Element of NAT & it = 0;
  existence
  proof
    per cases;
    suppose
      i is Element of NAT;
      then reconsider n = i as Element of NAT;
      take Fusc n;
      thus thesis;
    end;
    suppose
      i is not Element of NAT;
      hence thesis;
    end;
  end;
  uniqueness;
end;

definition
  func Fusc_Program -> XFinSequence of the InstructionsF of SCM equals
  <% 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;
end;

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

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

theorem Th4:
 Fusc_Program c= F implies
  for n being Element of NAT, N, A, B being Element of NAT,
      s being 0-started State-consisting of <%2,n,A,B%>
:::         <*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
 assume
A1: Fusc_Program c= F;
  defpred P[Nat] means for N, A, B being Element of NAT, s being
0-started State-consisting of  <%2,$1,A,B%>
:::<*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 P[n] holds P[k]
  proof
    set c2 = dl.0, n = dl.1, a = dl.2, b = dl.3, aux = dl.4;
    let nn be Nat;
    assume
A3: for n9 being Nat st n9 < nn holds for N, A, B being Element of NAT
, s being 0-started State-consisting of <%2,n9,A,B%>
:::<*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);
    reconsider n2 = nn as Element of NAT by ORDINAL1:def 12;
    let N, A, B be Element of NAT,
        s be 0-started State-consisting of <%2,nn,A,B%>;
:::<*2*>^<*nn*>^<*A*>^<*B*>;
    assume that
A4: N > 0 and
A5: Fusc N = A * Fusc nn + B * Fusc (nn+1);
A6: s.n = nn by SCM_1:1;
    set s0 = Comput(F,s,0);
A7: F.0 = n =0_goto 8 by A1,Lm17;
    set s1 = Comput(F,s,0+1);
A8: F.8 = halt SCM by A1,Lm17;
A9: F.3 = aux =0_goto 6 by A1,Lm17;
A10: IC s = 0 & s = s0 by EXTPRO_1:2,MEMSTR_0:def 12;
    s.a = A by SCM_1:1;
    then
A11: s1.a = A by A7,A10,SCM_1:10;
    s.c2 = 2 by SCM_1:1;
    then
A12: s1.c2 = 2 by A7,A10,SCM_1:10;
A13: F.2 = Divide(n, aux) by A1,Lm17;
    s.b = B by SCM_1:1;
    then
A14: s1.b = B by A7,A10,SCM_1:10;
A15: now
      assume
A16:  nn = 0;
      then
A17:  F.IC s1 = halt SCM by A7,A8,A6,A10,SCM_1:10;
      hence F halts_on s by EXTPRO_1:30;
      thus (Result(F,s)).b = s1.b by A17,EXTPRO_1:31
        .= Fusc N by A5,A14,A16,PRE_FF:18;
      hereby
        assume nn = 0;
        halt SCM <> n =0_goto 8 by SCM_1:12;
        hence LifeSpan(F,s) = 1 by A7,A10,A17,EXTPRO_1:33;
      end;
      thus nn>0 implies LifeSpan(F,s)=6 * ([\ log(2, nn) /] + 1)+1
by A16;
    end;
A18: F.1 = aux := c2 by A1,Lm17;
A19: F.5 = SCM-goto 0 by A1,Lm17;
A20: F.4 = AddTo(b, a) by A1,Lm17;
A21: F.7 = SCM-goto 0 by A1,Lm17;
A22: F.6 = AddTo(a, b) by A1,Lm17;
A23: s1.n = nn by A7,A6,A10,SCM_1:10;
A24: now
      set s6 = Comput(F,s,5+1);
      set s5 = Comput(F,s,4+1);
      set s4 = Comput(F,s,3+1);
      set s3 = Comput(F,s,2+1);
      set s2 = Comput(F,s,1+1);
A25:  nn mod 2 = nn - (nn div 2) * 2 by INT_1:def 10;
      assume
A26:  nn > 0;
      then
A27:  IC s1 = (0+1) by A7,A6,A10,SCM_1:10;
      then
A28:  IC s2 = (1+1) by A18,SCM_1:4;
      then
A29:  IC s3 = (2+1) by A13,Lm14,SCM_1:8;
      s2.a = A by A18,A11,A27,Lm15,SCM_1:4;
      then
A30:  s3.a =A by A13,A28,Lm10,Lm14,Lm15,SCM_1:8;
      s2.c2 = 2 by A18,A12,A27,Lm13,SCM_1:4;
      then
A31:  s3.c2 =2 by A13,A28,Lm7,Lm13,Lm14,SCM_1:8;
      s2.b = B by A18,A14,A27,Lm16,SCM_1:4;
      then
A32:  s3.b =B by A13,A28,Lm11,Lm14,Lm16,SCM_1:8;
A33:  s2.aux = 2 & s2.n = nn by A18,A12,A23,A27,Lm14,SCM_1:4;
      then
A34:  s3.n = n2 div 2 by A13,A28,Lm14,SCM_1:8;
      then reconsider nn9 = s3.n as Element of NAT by PRE_FF:7;
A35:  s3.aux = nn mod 2 by A13,A28,A33,Lm14,SCM_1:8;
      per cases;
      suppose
A36:    s3.aux <> 0;
        then
A37:    IC s4 = (3+1) by A9,A29,SCM_1:10;
        then
A38:    IC s5 = (4+1) by A20,SCM_1:5;
A39:    s4.a = A by A9,A29,A30,SCM_1:10;
        then s5.a = A by A20,A37,Lm12,SCM_1:5;
        then
A40:    s6.a = A by A19,A38,SCM_1:9;
        s4.b = B by A9,A29,A32,SCM_1:10;
        then
A41:    s5.b = B + A by A20,A37,A39,SCM_1:5;
A42:    s3.aux = 1 by A35,A36,PRE_FF:6;
        s4.n = s3.n by A9,A29,SCM_1:10;
        then s5.n = s3.n by A20,A37,Lm11,SCM_1:5;
        then
A43:    s6.n = s3.n by A19,A38,SCM_1:9;
        s4.c2 = 2 by A9,A29,A31,SCM_1:10;
        then s5.c2 = 2 by A20,A37,Lm9,SCM_1:5;
        then
A44:    s6.c2 = 2 by A19,A38,SCM_1:9;
        IC s6 = 0 & s6.b = s5.b by A19,A38,SCM_1:9;
        then
A45:    s6 is 0-started State-consisting of <%2,nn9,A,B+A%>
:::         <*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,s6) = 6 * ([\ log(2, nn9) /] +
1)+1 by A3,A4,A45,A47;
A50:    F halts_on s6 by A3,A4,A45,A47,A48;
        hence F halts_on s by EXTPRO_1:22;
        (Result(F,s6)).dl.3 = Fusc N by A3,A4,A45,A47,A48;
        hence (Result(F,s)).dl.3 = Fusc N by A50,EXTPRO_1:35;
        thus nn = 0 implies LifeSpan(F,s) = 1 by A26;
A51:    nn9 = 0 implies LifeSpan(F,s6) = 1 by A3,A4,A34,A35,A25,A42,A45,A48;
        thus nn > 0 implies LifeSpan(F,s) = 6 * ([\ log(2, nn) /]
+ 1)+1
        proof
          assume nn > 0;
          per cases;
          suppose
            nn9 = 0;
            hence thesis by A34,A35,A25,A42,A50,A51,Lm1,EXTPRO_1:34;
          end;
          suppose
A52:        nn9 <> 0;
            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;
          end;
        end;
      end;
      suppose
A54:    s3.aux = 0;
        then
A55:    IC s4 = 6 by A9,A29,SCM_1:10;
        then
A56:    IC s5 = (6+1) by A22,SCM_1:5;
        s4.c2 = 2 by A9,A29,A31,SCM_1:10;
        then s5.c2 = 2 by A22,A55,Lm8,SCM_1:5;
        then
A57:    s6.c2 = 2 by A21,A56,SCM_1:9;
A58:    s4.b = B by A9,A29,A32,SCM_1:10;
        then s5.b = B by A22,A55,Lm12,SCM_1:5;
        then
A59:    s6.b = B by A21,A56,SCM_1:9;
        s4.n = s3.n by A9,A29,SCM_1:10;
        then s5.n = s3.n by A22,A55,Lm10,SCM_1:5;
        then
A60:    s6.n = s3.n by A21,A56,SCM_1:9;
        s4.a = A by A9,A29,A30,SCM_1:10;
        then
A61:    s5.a = A + B by A22,A55,A58,SCM_1:5;
        reconsider nn9 = s3.n as Element of NAT by A34,PRE_FF:7;
        IC s6 = 0 & s6.a = s5.a by A21,A56,SCM_1:9;
        then
A62:    s6 is 0-started State-consisting of  <%2,nn9,A+B,B%>
:::            <*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,20;
        then
A64:    F halts_on s6 by A3,A4,A62;
        hence F halts_on s by EXTPRO_1:22;
        (Result(F,s6)).dl.3 = Fusc N by A3,A4,A62,A63;
        hence (Result(F,s)).dl.3 = Fusc N by A64,EXTPRO_1:35;
        thus nn = 0 implies LifeSpan(F,s) = 1 by A26;
A65:    nn9 > 0 implies LifeSpan(F,s6) = 6 * ([\ log(2, nn9) /] +
1)+1 by A3,A4,A62,A63;
        thus nn > 0 implies LifeSpan(F,s) = 6 * ([\ log(2, nn) /]
+ 1)+1
        proof
          assume nn > 0;
          per cases;
          suppose
            nn9 = 0;
            hence thesis by A13,A26,A28,A33,A34,A25,A54,Lm14,SCM_1:8;
          end;
          suppose
A66:        nn9 <> 0;
            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;
          end;
        end;
      end;
    end;
    nn >= 0 by NAT_1:2;
    hence thesis by A15,A24,XXREAL_0:1;
  end;
  for n being Nat holds P[n] from NAT_1:sch 4 ( A2 );
  hence thesis;
end;

theorem
 Fusc_Program c= F implies
  for N being Element of NAT st N > 0
  for s being 0-started State-consisting of <%2,N,1,0%>
:::     <*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
 assume
A1: Fusc_Program c= F;
  let N be Element of NAT;
  Fusc N = 1 * Fusc N + 0 * Fusc (N+1);
  hence thesis by A1,Th4;
end;