:: Two Programs for {\bf SCM}. Part I - Preliminaries :: by Grzegorz Bancerek and Piotr Rudnicki :: :: Received October 8, 1993 :: Copyright (c) 1993-2012 Association of Mizar Users begin :: Definition of fib definition let n be Nat; func Fib n -> Element of NAT means :Def1: :: PRE_FF:def 1 ex fib being Function of NAT,[:NAT,NAT:] st ( it = (fib . n) `1 & fib . 0 = [0,1] & ( for n being Nat holds fib . (n + 1) = [((fib . n) `2),(((fib . n) `1) + ((fib . n) `2))] ) ); existence ex b1 being Element of NAT ex fib being Function of NAT,[:NAT,NAT:] st ( b1 = (fib . n) `1 & fib . 0 = [0,1] & ( for n being Nat holds fib . (n + 1) = [((fib . n) `2),(((fib . n) `1) + ((fib . n) `2))] ) ) proofend; uniqueness for b1, b2 being Element of NAT st ex fib being Function of NAT,[:NAT,NAT:] st ( b1 = (fib . n) `1 & fib . 0 = [0,1] & ( for n being Nat holds fib . (n + 1) = [((fib . n) `2),(((fib . n) `1) + ((fib . n) `2))] ) ) & ex fib being Function of NAT,[:NAT,NAT:] st ( b2 = (fib . n) `1 & fib . 0 = [0,1] & ( for n being Nat holds fib . (n + 1) = [((fib . n) `2),(((fib . n) `1) + ((fib . n) `2))] ) ) holds b1 = b2 proofend; end; :: deftheorem Def1 defines Fib PRE_FF:def_1_:_ for n being Nat for b2 being Element of NAT holds ( b2 = Fib n iff ex fib being Function of NAT,[:NAT,NAT:] st ( b2 = (fib . n) `1 & fib . 0 = [0,1] & ( for n being Nat holds fib . (n + 1) = [((fib . n) `2),(((fib . n) `1) + ((fib . n) `2))] ) ) ); theorem :: PRE_FF:1 ( Fib 0 = 0 & Fib 1 = 1 & ( for n being Nat holds Fib ((n + 1) + 1) = (Fib n) + (Fib (n + 1)) ) ) proofend; :: Fusc function auxiliaries theorem :: PRE_FF:2 for i being Integer holds i div 1 = i proofend; theorem :: PRE_FF:3 for i, j being Integer st j > 0 & i div j = 0 holds i < j proofend; theorem :: PRE_FF:4 for i, j being Integer st 0 <= i & i < j holds i div j = 0 proofend; theorem :: PRE_FF:5 for i, j, k being Integer st k > 0 holds (i div j) div k = i div (j * k) proofend; theorem :: PRE_FF:6 for i being Integer holds ( i mod 2 = 0 or i mod 2 = 1 ) proofend; theorem :: PRE_FF:7 for i being Integer st i is Element of NAT holds i div 2 is Element of NAT proofend; theorem Th8: :: PRE_FF:8 for a, b, c being real number st a <= b & c > 1 holds c to_power a <= c to_power b proofend; theorem Th9: :: PRE_FF:9 for r, s being real number st r >= s holds [\r/] >= [\s/] proofend; theorem Th10: :: PRE_FF:10 for a, b, c being real number st a > 1 & b > 0 & c >= b holds log (a,c) >= log (a,b) proofend; theorem Th11: :: PRE_FF:11 for n being Nat st n > 0 holds [\(log (2,(2 * n)))/] + 1 <> [\(log (2,((2 * n) + 1)))/] proofend; theorem Th12: :: PRE_FF:12 for n being Nat st n > 0 holds [\(log (2,(2 * n)))/] + 1 >= [\(log (2,((2 * n) + 1)))/] proofend; theorem Th13: :: PRE_FF:13 for n being Nat st n > 0 holds [\(log (2,(2 * n)))/] = [\(log (2,((2 * n) + 1)))/] proofend; theorem :: PRE_FF:14 for n being Nat st n > 0 holds [\(log (2,n))/] + 1 = [\(log (2,((2 * n) + 1)))/] proofend; :: Fusc sequence definition let f be Function of NAT,(NAT *); let n be Element of NAT ; :: original:. redefine funcf . n -> FinSequence of NAT ; coherence f . n is FinSequence of NAT proofend; end; defpred S1[ Nat, FinSequence of NAT , set ] means ( ( for k being Nat st $1 + 2 = 2 * k holds $3 = $2 ^ <*($2 /. k)*> ) & ( for k being Nat st $1 + 2 = (2 * k) + 1 holds $3 = $2 ^ <*(($2 /. k) + ($2 /. (k + 1)))*> ) ); Lm1: for n being Element of NAT for x being Element of NAT * ex y being Element of NAT * st S1[n,x,y] proofend; defpred S2[ Nat, FinSequence of NAT , set ] means ( ( for k being Element of NAT st $1 + 2 = 2 * k holds $3 = $2 ^ <*($2 /. k)*> ) & ( for k being Element of NAT st $1 + 2 = (2 * k) + 1 holds $3 = $2 ^ <*(($2 /. k) + ($2 /. (k + 1)))*> ) ); Lm2: for n being Nat for x, y1, y2 being Element of NAT * st S2[n,x,y1] & S2[n,x,y2] holds y1 = y2 proofend; reconsider single1 = <*1*> as Element of NAT * by FINSEQ_1:def_11; consider fusc being Function of NAT,(NAT *) such that Lm3: fusc . 0 = single1 and Lm4: for n being Element of NAT holds S1[n,fusc . n,fusc . (n + 1)] from RECDEF_1:sch_2(Lm1); Lm5: for n being Nat holds S1[n,fusc . n,fusc . (n + 1)] proofend; definition let n be Nat; func Fusc n -> Element of NAT means :Def2: :: PRE_FF:def 2 it = 0 if n = 0 otherwise ex l being Element of NAT ex fusc being Function of NAT,(NAT *) st ( l + 1 = n & it = (fusc . l) /. n & fusc . 0 = <*1*> & ( for n being Nat holds ( ( for k being Nat st n + 2 = 2 * k holds fusc . (n + 1) = (fusc . n) ^ <*((fusc . n) /. k)*> ) & ( for k being Nat st n + 2 = (2 * k) + 1 holds fusc . (n + 1) = (fusc . n) ^ <*(((fusc . n) /. k) + ((fusc . n) /. (k + 1)))*> ) ) ) ); consistency for b1 being Element of NAT holds verum ; existence ( ( n = 0 implies ex b1 being Element of NAT st b1 = 0 ) & ( not n = 0 implies ex b1, l being Element of NAT ex fusc being Function of NAT,(NAT *) st ( l + 1 = n & b1 = (fusc . l) /. n & fusc . 0 = <*1*> & ( for n being Nat holds ( ( for k being Nat st n + 2 = 2 * k holds fusc . (n + 1) = (fusc . n) ^ <*((fusc . n) /. k)*> ) & ( for k being Nat st n + 2 = (2 * k) + 1 holds fusc . (n + 1) = (fusc . n) ^ <*(((fusc . n) /. k) + ((fusc . n) /. (k + 1)))*> ) ) ) ) ) ) proofend; uniqueness for b1, b2 being Element of NAT holds ( ( n = 0 & b1 = 0 & b2 = 0 implies b1 = b2 ) & ( not n = 0 & ex l being Element of NAT ex fusc being Function of NAT,(NAT *) st ( l + 1 = n & b1 = (fusc . l) /. n & fusc . 0 = <*1*> & ( for n being Nat holds ( ( for k being Nat st n + 2 = 2 * k holds fusc . (n + 1) = (fusc . n) ^ <*((fusc . n) /. k)*> ) & ( for k being Nat st n + 2 = (2 * k) + 1 holds fusc . (n + 1) = (fusc . n) ^ <*(((fusc . n) /. k) + ((fusc . n) /. (k + 1)))*> ) ) ) ) & ex l being Element of NAT ex fusc being Function of NAT,(NAT *) st ( l + 1 = n & b2 = (fusc . l) /. n & fusc . 0 = <*1*> & ( for n being Nat holds ( ( for k being Nat st n + 2 = 2 * k holds fusc . (n + 1) = (fusc . n) ^ <*((fusc . n) /. k)*> ) & ( for k being Nat st n + 2 = (2 * k) + 1 holds fusc . (n + 1) = (fusc . n) ^ <*(((fusc . n) /. k) + ((fusc . n) /. (k + 1)))*> ) ) ) ) implies b1 = b2 ) ) proofend; end; :: deftheorem Def2 defines Fusc PRE_FF:def_2_:_ for n being Nat for b2 being Element of NAT holds ( ( n = 0 implies ( b2 = Fusc n iff b2 = 0 ) ) & ( not n = 0 implies ( b2 = Fusc n iff ex l being Element of NAT ex fusc being Function of NAT,(NAT *) st ( l + 1 = n & b2 = (fusc . l) /. n & fusc . 0 = <*1*> & ( for n being Nat holds ( ( for k being Nat st n + 2 = 2 * k holds fusc . (n + 1) = (fusc . n) ^ <*((fusc . n) /. k)*> ) & ( for k being Nat st n + 2 = (2 * k) + 1 holds fusc . (n + 1) = (fusc . n) ^ <*(((fusc . n) /. k) + ((fusc . n) /. (k + 1)))*> ) ) ) ) ) ) ); theorem Th15: :: PRE_FF:15 ( Fusc 0 = 0 & Fusc 1 = 1 & ( for n being Nat holds ( Fusc (2 * n) = Fusc n & Fusc ((2 * n) + 1) = (Fusc n) + (Fusc (n + 1)) ) ) ) proofend; :: Auxiliary functions specific for Fib and Fusc of little general interest theorem :: PRE_FF:16 for n being Nat st n <> 0 holds n < 2 * n proofend; theorem :: PRE_FF:17 for n being Nat holds n < (2 * n) + 1 proofend; theorem :: PRE_FF:18 for A, B being Nat holds B = (A * (Fusc 0)) + (B * (Fusc 1)) by Th15; theorem :: PRE_FF:19 for n, A, B, N being Nat st Fusc N = (A * (Fusc ((2 * n) + 1))) + (B * (Fusc (((2 * n) + 1) + 1))) holds Fusc N = (A * (Fusc n)) + ((B + A) * (Fusc (n + 1))) proofend; theorem :: PRE_FF:20 for n, A, B, N being Nat st Fusc N = (A * (Fusc (2 * n))) + (B * (Fusc ((2 * n) + 1))) holds Fusc N = ((A + B) * (Fusc n)) + (B * (Fusc (n + 1))) proofend;