:: Two Programs for {\bf SCM}. Part II - Proofs
:: by Grzegorz Bancerek and Piotr Rudnicki
::
:: Received October 8, 1993
:: Copyright (c) 1993 Association of Mizar Users

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

proof end;

Lm2: for nn' being Element of NAT st nn' > 0 holds
( [\(log 2,nn')/] is Element of NAT & (6 * ([\(log 2,nn')/] + 1)) + 1 > 0 )

proof end;

Lm3: for nn, nn' being Element of NAT st nn = (2 * nn') + 1 & nn' > 0 holds
6 + ((6 * ([\(log 2,nn')/] + 1)) + 1) = (6 * ([\(log 2,nn)/] + 1)) + 1

proof 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 end;

Lm5: for nn, nn' being Element of NAT st nn = 2 * nn' & nn' > 0 holds
6 + ((6 * ([\(log 2,nn')/] + 1)) + 1) = (6 * ([\(log 2,nn)/] + 1)) + 1

proof end;

Lm6: for N being Element of NAT st N <> 0 holds
(6 * N) - 4 > 0

proof end;

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

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

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

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

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

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

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

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

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

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

definition

func Fib_Program -> FinSequence of the Instructions of SCM equals :: FIB_FUSC:def 1
(((((((<*((dl. 1) >0_goto (il. 2))*> ^ <*(halt SCM )*>) ^ <*((dl. 3) := (dl. 0 ))*>) ^ <*(SubFrom (dl. 1),(dl. 0 ))*>) ^ <*((dl. 1) =0_goto (il. 1))*>) ^ <*((dl. 4) := (dl. 2))*>) ^ <*((dl. 2) := (dl. 3))*>) ^ <*(AddTo (dl. 3),(dl. 4))*>) ^ <*(goto (il. 3))*>;
coherence
(((((((<*((dl. 1) >0_goto (il. 2))*> ^ <*(halt SCM )*>) ^ <*((dl. 3) := (dl. 0 ))*>) ^ <*(SubFrom (dl. 1),(dl. 0 ))*>) ^ <*((dl. 1) =0_goto (il. 1))*>) ^ <*((dl. 4) := (dl. 2))*>) ^ <*((dl. 2) := (dl. 3))*>) ^ <*(AddTo (dl. 3),(dl. 4))*>) ^ <*(goto (il. 3))*> is FinSequence of the Instructions of SCM ;

end;

:: deftheorem defines Fib_Program FIB_FUSC:def 1 :

Fib_Program = (((((((<*((dl. 1) >0_goto (il. 2))*> ^ <*(halt SCM )*>) ^ <*((dl. 3) := (dl. 0 ))*>) ^ <*(SubFrom (dl. 1),(dl. 0 ))*>) ^ <*((dl. 1) =0_goto (il. 1))*>) ^ <*((dl. 4) := (dl. 2))*>) ^ <*((dl. 2) := (dl. 3))*>) ^ <*(AddTo (dl. 3),(dl. 4))*>) ^ <*(goto (il. 3))*>;

theorem :: FIB_FUSC:1

for N being Element of NAT
for s being State-consisting of 0 , 0 , 0 , Fib_Program ,((<*1*> ^ <*N*>) ^ <*0 *>) ^ <*0 *> holds
( s is halting & ( N = 0 implies LifeSpan s = 1 ) & ( N > 0 implies LifeSpan s = (6 * N) - 2 ) & (Result s) . (dl. 3) = Fib N )

proof 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 b₁ being Element of NAT st
( ex n being Element of NAT st
( i = n & b₁ = Fusc n ) or ( i is not Element of NAT & b₁ = 0 ) )

proof end;

uniqueness
for b₁, b₂ being Element of NAT st ( ex n being Element of NAT st
( i = n & b₁ = Fusc n ) or ( i is not Element of NAT & b₁ = 0 ) ) & ( ex n being Element of NAT st
( i = n & b₂ = Fusc n ) or ( i is not Element of NAT & b₂ = 0 ) ) holds
b₁ = b₂ ;

end;

:: deftheorem Def2 defines Fusc' FIB_FUSC:def 2 :

for i being Integer
for b₂ being Element of NAT holds
( b₂ = Fusc' i iff ( ex n being Element of NAT st
( i = n & b₂ = Fusc n ) or ( i is not Element of NAT & b₂ = 0 ) ) );

definition

func Fusc_Program -> FinSequence of the Instructions of SCM equals :: FIB_FUSC:def 3
(((((((<*((dl. 1) =0_goto (il. 8))*> ^ <*((dl. 4) := (dl. 0 ))*>) ^ <*(Divide (dl. 1),(dl. 4))*>) ^ <*((dl. 4) =0_goto (il. 6))*>) ^ <*(AddTo (dl. 3),(dl. 2))*>) ^ <*(goto (il. 0 ))*>) ^ <*(AddTo (dl. 2),(dl. 3))*>) ^ <*(goto (il. 0 ))*>) ^ <*(halt SCM )*>;
coherence
(((((((<*((dl. 1) =0_goto (il. 8))*> ^ <*((dl. 4) := (dl. 0 ))*>) ^ <*(Divide (dl. 1),(dl. 4))*>) ^ <*((dl. 4) =0_goto (il. 6))*>) ^ <*(AddTo (dl. 3),(dl. 2))*>) ^ <*(goto (il. 0 ))*>) ^ <*(AddTo (dl. 2),(dl. 3))*>) ^ <*(goto (il. 0 ))*>) ^ <*(halt SCM )*> is FinSequence of the Instructions of SCM ;

end;

:: deftheorem defines Fusc_Program FIB_FUSC:def 3 :

Fusc_Program = (((((((<*((dl. 1) =0_goto (il. 8))*> ^ <*((dl. 4) := (dl. 0 ))*>) ^ <*(Divide (dl. 1),(dl. 4))*>) ^ <*((dl. 4) =0_goto (il. 6))*>) ^ <*(AddTo (dl. 3),(dl. 2))*>) ^ <*(goto (il. 0 ))*>) ^ <*(AddTo (dl. 2),(dl. 3))*>) ^ <*(goto (il. 0 ))*>) ^ <*(halt SCM )*>;

theorem :: FIB_FUSC:2

for N being Element of NAT st N > 0 holds
for s being State-consisting of 0 , 0 , 0 , Fusc_Program ,((<*2*> ^ <*N*>) ^ <*1*>) ^ <*0 *> holds
( s is halting & (Result s) . (dl. 3) = Fusc N & LifeSpan s = (6 * ([\(log 2,N)/] + 1)) + 1 )

proof end;

theorem :: FIB_FUSC:3

for N, k, Fk, Fk1 being Element of NAT
for s being State-consisting of 3, 0 , 0 , Fib_Program ,((<*1*> ^ <*N*>) ^ <*Fk*>) ^ <*Fk1*> st N > 0 & Fk = Fib k & Fk1 = Fib (k + 1) holds
( s is halting & LifeSpan s = (6 * N) - 4 & ex m being Element of NAT st
( m = (k + N) - 1 & (Result s) . (dl. 2) = Fib m & (Result s) . (dl. 3) = Fib (m + 1) ) )

proof end;

theorem :: FIB_FUSC:4

canceled;

theorem Th5: :: FIB_FUSC:5

for n, N, A, B being Element of NAT
for s being State-consisting of 0 , 0 , 0 , Fusc_Program ,((<*2*> ^ <*n*>) ^ <*A*>) ^ <*B*> st N > 0 & Fusc N = (A * (Fusc n)) + (B * (Fusc (n + 1))) holds
( s is halting & (Result s) . (dl. 3) = Fusc N & ( n = 0 implies LifeSpan s = 1 ) & ( n > 0 implies LifeSpan s = (6 * ([\(log 2,n)/] + 1)) + 1 ) )

proof end;

theorem :: FIB_FUSC:6

for N being Element of NAT st N > 0 holds
for s being State-consisting of 0 , 0 , 0 , Fusc_Program ,((<*2*> ^ <*N*>) ^ <*1*>) ^ <*0 *> holds
( s is halting & (Result s) . (dl. 3) = Fusc N & ( N = 0 implies LifeSpan s = 1 ) & ( N > 0 implies LifeSpan s = (6 * ([\(log 2,N)/] + 1)) + 1 ) )

proof end;