fib_fusc.miz



    begin

    

     Lm1: 0 = [\( log (2,1))/]

    proof

      

      thus 0 = [\ 0 /] by INT_1: 25

      .= [\( log (2,1))/] by POWER: 51;

    end;

    

     Lm2: for nn9 be 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 ;

      hence thesis;

    end;

    

     Lm3: for nn,nn9 be 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 be 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 be 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 be Nat st N <> 0 holds ((6 * N) - 4) > 0

    proof

      let N be Nat;

      assume N <> 0 ;

      then

      consider L be 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 ;

      hence thesis by A1;

    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

      :: FIB_FUSC:def1

      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 -definedthe InstructionsF of SCM -valued Function;

    

     Lm17: for I1,I2,I3,I4,I5,I6,I7,I8,I9 be 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 CARD_1: 57, ENUMSET1:def 7;

      (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_FUSC:1

     Fib_Program c= F implies for N be Element of NAT , s be 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[ Nat] means $1 < N implies for u be 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 be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat such that

         A15: k < N implies for u be 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 be Nat holds P[k] from NAT_1:sch 2( 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: 7, PRE_FF: 1;

      end;

        suppose ex k be Nat st N = (k + 1);

        then

        consider k be 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;

        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: 7

        .= ( Fib N) by A7, A44, A47, A46, SCM_1: 10;

      end;

    end;

    definition

      let i be Integer;

      :: FIB_FUSC:def2

      func Fusc' i -> Element of NAT means

      : Def2: (ex n be Element of NAT st i = n & it = ( Fusc n)) or not i is 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 not i is Element of NAT ;

          hence thesis;

        end;

      end;

      uniqueness ;

    end

    definition

      :: FIB_FUSC:def3

      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 :: FIB_FUSC:2

     Fusc_Program c= F implies for N be Element of NAT st N > 0 holds for s be 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

      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;

      then

      reconsider k 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 %>;

      consider s be State of SCM such that

       A5: s = S;

      defpred P[ Nat] means $1 <= (( log (2,N)) + 1) implies for u be 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 be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        assume

         A15: k <= (( log (2,N)) + 1) implies for u be 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 be Nat holds P[k] from NAT_1:sch 2( A63, A14);

       [\( log (2,N))/] <= ( log (2,N)) by INT_1:def 6;

      then

       A66: (k + 1) <= (( log (2,N)) + 1) by XREAL_1: 6;

      then

       A67: ( Fusc N) = (((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, 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: 7;

      (F . ( IC h)) = ( halt SCM ) by A71, A1, Lm17;

      hence thesis by A5, A72, EXTPRO_1: 33;

    end;

    theorem :: FIB_FUSC:3

     Fib_Program c= F implies for N be Nat, k,Fk,Fk1 be Nat, s be 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 be 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[ Nat] means for k,Fk,Fk1 be 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 be 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 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 Nat;

        assume

         A3: P[N];

        let k,Fk,Fk1 be Nat, s be 3 -started State-consisting of <%1, (N + 1), Fk, Fk1%>;

        assume that (N + 1) > 0 and

         A4: Fk = ( Fib k) and

         A5: Fk1 = ( Fib (k + 1));

        

         A6: (F . 3) = ( SubFrom (n,C1)) by A1, Lm17;

        set s0 = ( Comput (F,s, 0 ));

        set s1 = ( Comput (F,s,( 0 + 1)));

        

         A7: (F . 1) = ( halt SCM ) by A1, Lm17;

        

         A8: ( IC s) = 3 & s = s0 by EXTPRO_1: 2, MEMSTR_0:def 12;

        

        then

         A9: ( IC s1) = (3 + 1) by A6, SCM_1: 6

        .= 4;

        set s2 = ( Comput (F,s,(1 + 1)));

        

         A10: (F . 4) = (n =0_goto 1) by A1, Lm17;

        (s . FC) = Fk1 by SCM_1: 1;

        then (s1 . FC) = Fk1 by A6, A8, Lm11, SCM_1: 6;

        then

         A11: (s2 . FC) = Fk1 by A10, A9, SCM_1: 10;

        

         A12: (F . 7) = ( AddTo (FC,AUX)) by A1, Lm17;

        (s . FP) = Fk by SCM_1: 1;

        then (s1 . FP) = Fk by A6, A8, Lm10, SCM_1: 6;

        then

         A13: (s2 . FP) = Fk by A10, A9, SCM_1: 10;

        

         A14: (F . 6) = (FP := FC) by A1, Lm17;

        

         A15: (s . C1) = 1 by SCM_1: 1;

        then (s1 . C1) = 1 by A6, A8, Lm7, SCM_1: 6;

        then

         A16: (s2 . C1) = 1 by A10, A9, SCM_1: 10;

        (s . n) = (N + 1) by SCM_1: 1;

        

        then

         A17: (s1 . n) = ((N + 1) - 1) by A6, A15, A8, SCM_1: 6

        .= N;

        then

         A18: (s2 . n) = N by A10, A9, SCM_1: 10;

        

         A19: (F . 5) = (AUX := FP) by A1, Lm17;

        

         A20: (F . 8) = ( SCM-goto 3) by A1, Lm17;

        per cases ;

          suppose

           A21: N = 0 ;

          then

           A22: (F . ( IC s2)) = ( halt SCM ) by A7, A10, A17, A9, SCM_1: 10;

          hence F halts_on s by EXTPRO_1: 30;

          (F . ( IC s1)) <> ( halt SCM ) by A10, A9, SCM_1: 12;

          hence ( LifeSpan (F,s)) = ((6 * (N + 1)) - 4) by A21, A22, EXTPRO_1: 32;

          reconsider m = k as Element of NAT by ORDINAL1:def 12;

          take m;

          thus m = ((k + (N + 1)) - 1) by A21;

          thus thesis by A4, A5, A13, A11, A22, EXTPRO_1: 7;

        end;

          suppose

           A23: N > 0 ;

          then

           A24: ((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)));

          

           A25: ( IC s2) = (4 + 1) by A10, A17, A9, A23, SCM_1: 10;

          then

           A26: ( IC s3) = (5 + 1) by A19, SCM_1: 4;

          then

           A27: ( IC s4) = (6 + 1) by A14, SCM_1: 4;

          then

           A28: ( IC s5) = (7 + 1) by A12, SCM_1: 5;

          

           A29: (s3 . FC) = ( Fib (k + 1)) by A5, A19, A11, A25, Lm16, SCM_1: 4;

          then

           A30: (s4 . FC) = ( Fib (k + 1)) by A14, A26, Lm12, SCM_1: 4;

          (s4 . FP) = ( Fib (k + 1)) by A14, A26, A29, SCM_1: 4;

          then (s5 . FP) = ( Fib (k + 1)) by A12, A27, Lm12, SCM_1: 5;

          then

           A31: (s6 . FP) = ( Fib (k + 1)) by A20, A28, SCM_1: 9;

          (s3 . C1) = 1 by A19, A16, A25, Lm13, SCM_1: 4;

          then (s4 . C1) = 1 by A14, A26, Lm8, SCM_1: 4;

          then (s5 . C1) = 1 by A12, A27, Lm9, SCM_1: 5;

          then

           A32: (s6 . C1) = 1 by A20, A28, SCM_1: 9;

          (s3 . AUX) = ( Fib k) by A4, A19, A13, A25, SCM_1: 4;

          then

           A33: (s4 . AUX) = ( Fib k) by A14, A26, Lm15, SCM_1: 4;

          (s5 . FC) = ((s4 . AUX) + (s4 . FC)) by A12, A27, SCM_1: 5

          .= ( Fib ((k + 1) + 1)) by A30, A33, PRE_FF: 1;

          then

           A34: (s6 . FC) = ( Fib ((k + 1) + 1)) by A20, A28, SCM_1: 9;

          (s3 . n) = N by A19, A18, A25, Lm14, SCM_1: 4;

          then (s4 . n) = N by A14, A26, Lm10, SCM_1: 4;

          then (s5 . n) = N by A12, A27, Lm11, SCM_1: 5;

          then

           A35: (s6 . n) = N by A20, A28, SCM_1: 9;

          ( IC s6) = 3 by A20, A28, SCM_1: 9;

          then

           A36: s6 is 3 -started State-consisting of <%1, N, Fk1, Fk2%> by A5, A32, A35, A31, A34, MEMSTR_0:def 12, SCM_1: 13;

          then

          consider m be Element of NAT such that

           A37: m = (((k + 1) + N) - 1) and (( Result (F,s6)) . ( dl. 2)) = ( Fib m) and (( Result (F,s6)) . ( dl. 3)) = ( Fib (m + 1)) by A3, A5, A23;

          F halts_on s6 by A3, A5, A23, A36;

          hence F halts_on s by EXTPRO_1: 22;

          ( LifeSpan (F,s6)) = ((6 * N) - 4) by A3, A5, A23, A36;

          

          hence ( LifeSpan (F,s)) = (6 + ((6 * N) - 4)) by A3, A5, A23, A36, A24, EXTPRO_1: 34

          .= ((6 * (N + 1)) - 4);

          take m;

          thus m = ((k + (N + 1)) - 1) by A37;

          ex m be 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, A5, A23, A36;

          hence thesis by A37, A3, A5, A23, A36, EXTPRO_1: 35;

        end;

      end;

      

       A38: P[ 0 ];

      thus for N be Nat holds P[N] from NAT_1:sch 2( A38, A2);

    end;

    theorem :: FIB_FUSC:4

    

     Th4: Fusc_Program c= F implies for n be Element of NAT , N,A,B be Element of NAT , s be 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

      assume

       A1: Fusc_Program c= F;

      defpred P[ Nat] means for N,A,B be Element of NAT , s be 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 be Nat st for n be 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 be Nat st n9 < nn holds for N,A,B be Element of NAT , s be 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));

        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%>;

        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: 7

          .= ( 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)%> 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 ;

                then

                reconsider m = [\( log (2,nn9))/] as Element of NAT by Lm2;

                

                thus ( LifeSpan (F,s)) = (6 + ((6 * (m + 1)) + 1)) by A50, A49, A52, EXTPRO_1: 34

                .= ((6 * ( [\( log (2,nn))/] + 1)) + 1) by A34, A35, A42, A46, A53, Lm3;

              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%> 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 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 ;

                then

                reconsider m = [\( log (2,nn9))/] as Element of NAT by Lm2;

                

                thus ( LifeSpan (F,s)) = (6 + ((6 * (m + 1)) + 1)) by A64, A65, A66, EXTPRO_1: 34

                .= ((6 * ( [\( log (2,nn))/] + 1)) + 1) by A34, A35, A25, A54, A67, Lm5;

              end;

            end;

          end;

        end;

        thus thesis by A15, A24;

      end;

      for n be Nat holds P[n] from NAT_1:sch 4( A2);

      hence thesis;

    end;

    theorem :: FIB_FUSC:5

     Fusc_Program c= F implies for N be Element of NAT st N > 0 holds for s be 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

      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;