:: FIB_NUM  semantic presentation begin  






theorem :: FIB_NUM:1 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "m"))  ($#k3_int_2 :::"gcd"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "m"))  ($#k3_int_2 :::"gcd"::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Set (Var "m")) ")" )))) ; 
 
theorem :: FIB_NUM:2 (Bool  "for" (Set (Var "k")) "," (Set (Var "m")) "," (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Set (Var "k"))  ($#k3_int_2 :::"gcd"::: )  (Set (Var "m")))  ($#r1_hidden :::"="::: )  (Num 1))) "holds"  (Bool (Set (Set (Var "k"))  ($#k3_int_2 :::"gcd"::: )  (Set  "(" (Set (Var "m"))  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "k"))  ($#k3_int_2 :::"gcd"::: )  (Set (Var "n"))))) ; 
 
theorem :: FIB_NUM:3 (Bool  "for" (Set (Var "s")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "s"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "ex" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Num 1)  ($#k13_complex1 :::"/"::: )  (Set (Var "n")))) & (Bool (Set (Num 1)  ($#k13_complex1 :::"/"::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s")))  ")" ))) ; 
 scheme  :: FIB_NUM:sch 1 FibInd{ P1[   ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool P1[(Set (Var "k"))]))
 provided
(Bool P1[(Set   ($#k6_numbers :::"0"::: )  )])
 and  
(Bool P1[(Num 1)])
 and  
(Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool P1[(Set (Var "k"))]) & (Bool P1[(Set (Set (Var "k"))  ($#k1_nat_1 :::"+"::: )  (Num 1))])) "holds"  (Bool P1[(Set (Set (Var "k"))  ($#k1_nat_1 :::"+"::: )  (Num 2))]))
 proof 


end; scheme  :: FIB_NUM:sch 2 BinInd{ P1[  ($#m1_hidden :::"Nat":::) ","   ($#m1_hidden :::"Nat":::)] } : 
(Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool P1[(Set (Var "m")) "," (Set (Var "n"))]))
 provided
(Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool P1[(Set (Var "m")) "," (Set (Var "n"))])) "holds"  (Bool P1[(Set (Var "n")) "," (Set (Var "m"))]))
 and  
(Bool  "for" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool  "("   "for" (Set (Var "m")) "," (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "k"))) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "k")))) "holds"  (Bool P1[(Set (Var "m")) "," (Set (Var "n"))])  ")" )) "holds"  (Bool  "for" (Set (Var "m")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k")))) "holds"  (Bool P1[(Set (Var "k")) "," (Set (Var "m"))])))
 proof 


end; 
theorem :: FIB_NUM:4 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k1_pre_ff :::"Fib"::: )  (Set  "(" (Set (Var "m"))  ($#k1_nat_1 :::"+"::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k1_pre_ff :::"Fib"::: )  (Set (Var "n")) ")" )  ($#k4_nat_1 :::"*"::: )  (Set  "("  ($#k1_pre_ff :::"Fib"::: )  (Set (Var "m")) ")" ) ")" )  ($#k2_nat_1 :::"+"::: )  (Set  "(" (Set  "("  ($#k1_pre_ff :::"Fib"::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )  ($#k4_nat_1 :::"*"::: )  (Set  "("  ($#k1_pre_ff :::"Fib"::: )  (Set  "(" (Set (Var "m"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ) ")" )))) ; 
 
theorem :: FIB_NUM:5 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set  "("  ($#k1_pre_ff :::"Fib"::: )  (Set (Var "m")) ")" )  ($#k3_int_2 :::"gcd"::: )  (Set  "("  ($#k1_pre_ff :::"Fib"::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_pre_ff :::"Fib"::: )  (Set  "(" (Set (Var "m"))  ($#k3_int_2 :::"gcd"::: )  (Set (Var "n")) ")" )))) ; 
 begin  






theorem :: FIB_NUM:6 (Bool  "for" (Set (Var "x")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k1_quin_1 :::"delta"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "x"))  ($#k3_square_1 :::"^2"::: )  ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "x")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "("  ($#k6_square_1 :::"sqrt"::: )  (Set  "("  ($#k1_quin_1 :::"delta"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")"  ")" ) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a")) ")" ))) "or" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k6_square_1 :::"sqrt"::: )  (Set  "("  ($#k1_quin_1 :::"delta"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")"  ")" ) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a")) ")" )))  ")" )  ")" )) ; 
 definitionfunc  :::"tau":::  ->   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   equals :: FIB_NUM:def 1 (Set (Set  "(" (Num 1)  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Num 5) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 2)); end; 




:: deftheorem    defines :::"tau"::: FIB_NUM:def 1 :  (Bool (Set   ($#k1_fib_num :::"tau"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 1)  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Num 5) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 2))); 
 definitionfunc  :::"tau_bar":::  ->   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   equals :: FIB_NUM:def 2 (Set (Set  "(" (Num 1)  ($#k6_xcmplx_0 :::"-"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Num 5) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 2)); end; 




:: deftheorem    defines :::"tau_bar"::: FIB_NUM:def 2 :  (Bool (Set   ($#k2_fib_num :::"tau_bar"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 1)  ($#k6_xcmplx_0 :::"-"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Num 5) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 2))); 
 
theorem :: FIB_NUM:7 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k1_pre_ff :::"Fib"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  ($#k1_fib_num :::"tau"::: ) )  ($#k3_power :::"to_power"::: )  (Set (Var "n")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  ($#k2_fib_num :::"tau_bar"::: ) )  ($#k3_power :::"to_power"::: )  (Set (Var "n")) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Num 5) ")" )))) ; 
 
theorem :: FIB_NUM:8 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "holds" (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set  "("  ($#k1_pre_ff :::"Fib"::: )  (Set (Var "n")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Set  ($#k1_fib_num :::"tau"::: ) )  ($#k3_power :::"to_power"::: )  (Set (Var "n")) ")" )  ($#k13_complex1 :::"/"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Num 5) ")" ) ")" ) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Num 1))) ; 
 






theorem :: FIB_NUM:9 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool (Set (Var "g")) "is"   ($#v2_relat_1 :::"non-zero"::: )  )) "holds"  (Bool (Set (Set  "(" (Set (Var "f"))  ($#k52_valued_1 :::"/""::: )  (Set (Var "g")) ")" )  ($#k20_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "g"))  ($#k52_valued_1 :::"/""::: )  (Set (Var "h")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k52_valued_1 :::"/""::: )  (Set (Var "h"))))) ; 
 
theorem :: FIB_NUM:10 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set (Set  "(" (Set (Var "f"))  ($#k52_valued_1 :::"/""::: )  (Set (Var "g")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k13_complex1 :::"/"::: )  (Set  "(" (Set (Var "g"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" ))) & (Bool (Set (Set  "(" (Set (Var "f"))  ($#k52_valued_1 :::"/""::: )  (Set (Var "g")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set  "(" (Set (Var "g"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k5_xcmplx_0 :::"""::: )  ")" )))  ")" ))) ; 
 
theorem :: FIB_NUM:11 (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool  "("   "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "F"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_pre_ff :::"Fib"::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Set  "("  ($#k1_pre_ff :::"Fib"::: )  (Set (Var "n")) ")" )))  ")" )) "holds"  (Bool  "("  (Bool (Set (Var "F")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set (Var "F")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_fib_num :::"tau"::: )  ))  ")" )) ;