:: FIB_NUM3 semantic presentation begin theorem :: FIB_NUM3:1 (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Set (Var "a")) ($#k3_power :::"to_power"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: FIB_NUM3:2 (Bool "for" (Set (Var "a")) "being" ($#~v3_xxreal_0 "non" ($#v3_xxreal_0 :::"negative"::: ) ) ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set (Var "a")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a")))) ; theorem :: FIB_NUM3:3 (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "a")) ($#k3_power :::"to_power"::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "a")) ")" ) ($#k3_power :::"to_power"::: ) (Num 2)))) ; theorem :: FIB_NUM3:4 (Bool "for" (Set (Var "k")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set (Var "k")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "k")) ($#k1_nat_1 :::"+"::: ) (Num 2) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1)))) ; theorem :: FIB_NUM3:5 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k2_nat_1 :::"+"::: ) (Set (Var "b")) ")" ) ($#k13_newton :::"|^"::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k4_nat_1 :::"*"::: ) (Set (Var "a")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k4_nat_1 :::"*"::: ) (Set (Var "b")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k4_nat_1 :::"*"::: ) (Set (Var "b")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k4_nat_1 :::"*"::: ) (Set (Var "b")) ")" )))) ; theorem :: FIB_NUM3:6 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k3_power :::"to_power"::: ) (Set (Var "n")) ")" ) ($#k3_power :::"to_power"::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k3_power :::"to_power"::: ) (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ))))) ; theorem :: FIB_NUM3:7 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "b")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k3_power :::"to_power"::: ) (Num 2) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k3_power :::"to_power"::: ) (Num 2) ")" )))) ; theorem :: FIB_NUM3:8 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "b")) ")" ) ($#k3_power :::"to_power"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k3_power :::"to_power"::: ) (Set (Var "n")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k3_power :::"to_power"::: ) (Set (Var "n")) ")" ))))) ; registration cluster (Set ($#k1_fib_num :::"tau"::: ) ) -> ($#v2_xxreal_0 :::"positive"::: ) ; cluster (Set ($#k2_fib_num :::"tau_bar"::: ) ) -> ($#v3_xxreal_0 :::"negative"::: ) ; end; theorem :: FIB_NUM3:9 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set ($#k1_fib_num :::"tau"::: ) ) ($#k3_power :::"to_power"::: ) (Set (Var "n")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set ($#k1_fib_num :::"tau"::: ) ) ($#k3_power :::"to_power"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_fib_num :::"tau"::: ) ) ($#k3_power :::"to_power"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2) ")" )))) ; theorem :: FIB_NUM3:10 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set ($#k2_fib_num :::"tau_bar"::: ) ) ($#k3_power :::"to_power"::: ) (Set (Var "n")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set ($#k2_fib_num :::"tau_bar"::: ) ) ($#k3_power :::"to_power"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_fib_num :::"tau_bar"::: ) ) ($#k3_power :::"to_power"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2) ")" )))) ; begin definitionlet "n" be ($#m1_hidden :::"Nat":::); func :::"Lucas"::: "n" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: FIB_NUM3:def 1 (Bool "ex" (Set (Var "L")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k8_mcart_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k5_numbers :::"NAT"::: ) ) ($#k8_mcart_1 :::":]"::: ) ) "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "L")) ($#k8_nat_1 :::"."::: ) "n" ")" ) ($#k2_domain_1 :::"`1"::: ) )) & (Bool (Set (Set (Var "L")) ($#k3_funct_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Num 2) "," (Num 1) ($#k1_domain_1 :::"]"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "L")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set "(" (Set (Var "L")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k3_domain_1 :::"`2"::: ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set (Var "L")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k2_domain_1 :::"`1"::: ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "L")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k3_domain_1 :::"`2"::: ) ")" ) ")" ) ($#k1_domain_1 :::"]"::: ) )) ")" ) ")" )); end; :: deftheorem defines :::"Lucas"::: FIB_NUM3:def 1 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_fib_num3 :::"Lucas"::: ) (Set (Var "n")))) "iff" (Bool "ex" (Set (Var "L")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k8_mcart_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k5_numbers :::"NAT"::: ) ) ($#k8_mcart_1 :::":]"::: ) ) "st" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "L")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k2_domain_1 :::"`1"::: ) )) & (Bool (Set (Set (Var "L")) ($#k3_funct_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Num 2) "," (Num 1) ($#k1_domain_1 :::"]"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "L")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set "(" (Set (Var "L")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k3_domain_1 :::"`2"::: ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set (Var "L")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k2_domain_1 :::"`1"::: ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "L")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k3_domain_1 :::"`2"::: ) ")" ) ")" ) ($#k1_domain_1 :::"]"::: ) )) ")" ) ")" )) ")" ))); theorem :: FIB_NUM3:11 (Bool "(" (Bool (Set ($#k1_fib_num3 :::"Lucas"::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Num 2)) & (Bool (Set ($#k1_fib_num3 :::"Lucas"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k1_fib_num3 :::"Lucas"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_fib_num3 :::"Lucas"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k1_fib_num3 :::"Lucas"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))) ")" ) ")" ) ; theorem :: FIB_NUM3:12 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k1_fib_num3 :::"Lucas"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_fib_num3 :::"Lucas"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k1_fib_num3 :::"Lucas"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )))) ; theorem :: FIB_NUM3:13 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" ($#k1_fib_num3 :::"Lucas"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k1_fib_num3 :::"Lucas"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_fib_num3 :::"Lucas"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 3) ")" )))) ; theorem :: FIB_NUM3:14 (Bool (Set ($#k1_fib_num3 :::"Lucas"::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Num 3)) ; theorem :: FIB_NUM3:15 (Bool (Set ($#k1_fib_num3 :::"Lucas"::: ) (Num 3)) ($#r1_hidden :::"="::: ) (Num 4)) ; theorem :: FIB_NUM3:16 (Bool (Set ($#k1_fib_num3 :::"Lucas"::: ) (Num 4)) ($#r1_hidden :::"="::: ) (Num 7)) ; theorem :: FIB_NUM3:17 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k1_fib_num3 :::"Lucas"::: ) (Set (Var "k"))) ($#r1_xxreal_0 :::">="::: ) (Set (Var "k")))) ; theorem :: FIB_NUM3:18 (Bool "for" (Set (Var "m")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k1_fib_num3 :::"Lucas"::: ) (Set "(" (Set (Var "m")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_xxreal_0 :::">="::: ) (Set ($#k1_fib_num3 :::"Lucas"::: ) (Set (Var "m"))))) ; registrationlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set ($#k1_fib_num3 :::"Lucas"::: ) "n") -> ($#v2_xxreal_0 :::"positive"::: ) ; end; theorem :: FIB_NUM3:19 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Num 2) ($#k4_nat_1 :::"*"::: ) (Set "(" ($#k1_fib_num3 :::"Lucas"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_fib_num3 :::"Lucas"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k1_fib_num3 :::"Lucas"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ) ")" )))) ; theorem :: FIB_NUM3:20 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k1_fib_num3 :::"Lucas"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_pre_ff :::"Fib"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k1_pre_ff :::"Fib"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2) ")" ) ")" )))) ; theorem :: FIB_NUM3:21 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k1_fib_num3 :::"Lucas"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k1_fib_num :::"tau"::: ) ) ($#k3_power :::"to_power"::: ) (Set (Var "n")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set ($#k2_fib_num :::"tau_bar"::: ) ) ($#k3_power :::"to_power"::: ) (Set (Var "n")) ")" )))) ; theorem :: FIB_NUM3:22 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set "(" ($#k1_fib_num3 :::"Lucas"::: ) (Set (Var "n")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k1_fib_num3 :::"Lucas"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Num 5) ($#k4_nat_1 :::"*"::: ) (Set "(" ($#k1_pre_ff :::"Fib"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )))) ; theorem :: FIB_NUM3:23 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" ($#k1_fib_num3 :::"Lucas"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 3) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set "(" ($#k1_fib_num3 :::"Lucas"::: ) (Set (Var "n")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Num 5) ($#k4_nat_1 :::"*"::: ) (Set "(" ($#k1_pre_ff :::"Fib"::: ) (Set (Var "n")) ")" )))) ; theorem :: FIB_NUM3:24 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" ($#k1_fib_num3 :::"Lucas"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k1_pre_ff :::"Fib"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k4_nat_1 :::"*"::: ) (Set "(" ($#k1_pre_ff :::"Fib"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )))) ; theorem :: FIB_NUM3:25 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Num 3) ($#k4_nat_1 :::"*"::: ) (Set "(" ($#k1_pre_ff :::"Fib"::: ) (Set (Var "n")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k1_fib_num3 :::"Lucas"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k4_nat_1 :::"*"::: ) (Set "(" ($#k1_pre_ff :::"Fib"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2) ")" ) ")" )))) ; theorem :: FIB_NUM3:26 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Num 2) ($#k4_nat_1 :::"*"::: ) (Set "(" ($#k1_fib_num3 :::"Lucas"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Set (Var "m")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_fib_num3 :::"Lucas"::: ) (Set (Var "n")) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" ($#k1_fib_num3 :::"Lucas"::: ) (Set (Var "m")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Set "(" (Num 5) ($#k4_nat_1 :::"*"::: ) (Set "(" ($#k1_pre_ff :::"Fib"::: ) (Set (Var "n")) ")" ) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" ($#k1_pre_ff :::"Fib"::: ) (Set (Var "m")) ")" ) ")" )))) ; theorem :: FIB_NUM3:27 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k1_fib_num3 :::"Lucas"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" ($#k1_fib_num3 :::"Lucas"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_fib_num3 :::"Lucas"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) ($#k13_newton :::"|^"::: ) (Num 2) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" ($#k1_fib_num3 :::"Lucas"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k13_newton :::"|^"::: ) (Num 2) ")" )))) ; theorem :: FIB_NUM3:28 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k1_pre_ff :::"Fib"::: ) (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_pre_ff :::"Fib"::: ) (Set (Var "n")) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" ($#k1_fib_num3 :::"Lucas"::: ) (Set (Var "n")) ")" )))) ; theorem :: FIB_NUM3:29 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Num 2) ($#k4_nat_1 :::"*"::: ) (Set "(" ($#k1_pre_ff :::"Fib"::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_fib_num3 :::"Lucas"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" ($#k1_pre_ff :::"Fib"::: ) (Set (Var "n")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Set "(" ($#k1_fib_num3 :::"Lucas"::: ) (Set (Var "n")) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" ($#k1_pre_ff :::"Fib"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" )))) ; theorem :: FIB_NUM3:30 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" (Num 5) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set "(" ($#k1_pre_ff :::"Fib"::: ) (Set (Var "n")) ")" ) ($#k13_newton :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" ($#k1_fib_num3 :::"Lucas"::: ) (Set (Var "n")) ")" ) ($#k13_newton :::"|^"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set (Num 4) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ($#k3_power :::"to_power"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )))) ; theorem :: FIB_NUM3:31 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k1_pre_ff :::"Fib"::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_pre_ff :::"Fib"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" ($#k1_fib_num3 :::"Lucas"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" ($#k1_pre_ff :::"Fib"::: ) (Set (Var "n")) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" ($#k1_fib_num3 :::"Lucas"::: ) (Set (Var "n")) ")" ) ")" )))) ; begin definitionlet "a", "b" be ($#m1_hidden :::"Nat":::); :: original: :::"["::: redefine func :::"[":::"a" "," "b":::"]"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k8_mcart_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k5_numbers :::"NAT"::: ) ) ($#k8_mcart_1 :::":]"::: ) ); end; definitionlet "a", "b", "n" be ($#m1_hidden :::"Nat":::); func :::"GenFib"::: "(" "a" "," "b" "," "n" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: FIB_NUM3:def 2 (Bool "ex" (Set (Var "L")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k8_mcart_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k5_numbers :::"NAT"::: ) ) ($#k8_mcart_1 :::":]"::: ) ) "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "L")) ($#k8_nat_1 :::"."::: ) "n" ")" ) ($#k2_domain_1 :::"`1"::: ) )) & (Bool (Set (Set (Var "L")) ($#k3_funct_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k2_fib_num3 :::"["::: ) "a" "," "b" ($#k2_fib_num3 :::"]"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "L")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_fib_num3 :::"["::: ) (Set "(" (Set "(" (Set (Var "L")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k3_domain_1 :::"`2"::: ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set (Var "L")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k2_domain_1 :::"`1"::: ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "L")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k3_domain_1 :::"`2"::: ) ")" ) ")" ) ($#k2_fib_num3 :::"]"::: ) )) ")" ) ")" )); end; :: deftheorem defines :::"GenFib"::: FIB_NUM3:def 2 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k3_fib_num3 :::"GenFib"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "n")) ")" )) "iff" (Bool "ex" (Set (Var "L")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k8_mcart_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k5_numbers :::"NAT"::: ) ) ($#k8_mcart_1 :::":]"::: ) ) "st" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "L")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k2_domain_1 :::"`1"::: ) )) & (Bool (Set (Set (Var "L")) ($#k3_funct_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k2_fib_num3 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_fib_num3 :::"]"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "L")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_fib_num3 :::"["::: ) (Set "(" (Set "(" (Set (Var "L")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k3_domain_1 :::"`2"::: ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set (Var "L")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k2_domain_1 :::"`1"::: ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "L")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k3_domain_1 :::"`2"::: ) ")" ) ")" ) ($#k2_fib_num3 :::"]"::: ) )) ")" ) ")" )) ")" ))); theorem :: FIB_NUM3:32 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set ($#k3_fib_num3 :::"GenFib"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set ($#k3_fib_num3 :::"GenFib"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Num 1) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k3_fib_num3 :::"GenFib"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set "(" (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_fib_num3 :::"GenFib"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "n")) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k3_fib_num3 :::"GenFib"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ))) ")" ) ")" )) ; theorem :: FIB_NUM3:33 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set "(" ($#k3_fib_num3 :::"GenFib"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set "(" (Set (Var "k")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k3_fib_num3 :::"GenFib"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set "(" (Set "(" (Set (Var "k")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ($#k13_newton :::"|^"::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k3_fib_num3 :::"GenFib"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set "(" (Set (Var "k")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ($#k13_newton :::"|^"::: ) (Num 2) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set "(" ($#k3_fib_num3 :::"GenFib"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set "(" (Set (Var "k")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" ($#k3_fib_num3 :::"GenFib"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set "(" (Set "(" (Set (Var "k")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Set "(" ($#k3_fib_num3 :::"GenFib"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set "(" (Set "(" (Set (Var "k")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ($#k13_newton :::"|^"::: ) (Num 2) ")" ))))) ; theorem :: FIB_NUM3:34 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" ($#k3_fib_num3 :::"GenFib"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "n")) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k3_fib_num3 :::"GenFib"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_fib_num3 :::"GenFib"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ))) ; theorem :: FIB_NUM3:35 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" ($#k3_fib_num3 :::"GenFib"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k3_fib_num3 :::"GenFib"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_fib_num3 :::"GenFib"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 3) ")" ) ")" ))) ; theorem :: FIB_NUM3:36 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k3_fib_num3 :::"GenFib"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k3_fib_num3 :::"GenFib"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_fib_num3 :::"GenFib"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 4) ")" ) ")" ))) ; theorem :: FIB_NUM3:37 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k3_fib_num3 :::"GenFib"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_pre_ff :::"Fib"::: ) (Set (Var "n"))))) ; theorem :: FIB_NUM3:38 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k3_fib_num3 :::"GenFib"::: ) "(" (Num 2) "," (Num 1) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_fib_num3 :::"Lucas"::: ) (Set (Var "n"))))) ; theorem :: FIB_NUM3:39 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k3_fib_num3 :::"GenFib"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "n")) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k3_fib_num3 :::"GenFib"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k4_nat_1 :::"*"::: ) (Set "(" ($#k3_fib_num3 :::"GenFib"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ")" )))) ; theorem :: FIB_NUM3:40 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k3_fib_num3 :::"GenFib"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "n")) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k3_fib_num3 :::"GenFib"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 4) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Num 3) ($#k4_nat_1 :::"*"::: ) (Set "(" ($#k3_fib_num3 :::"GenFib"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ")" )))) ; theorem :: FIB_NUM3:41 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k3_fib_num3 :::"GenFib"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ) ")" ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k3_fib_num3 :::"GenFib"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "n")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k4_nat_1 :::"*"::: ) (Set "(" ($#k3_fib_num3 :::"GenFib"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" )))) ; theorem :: FIB_NUM3:42 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k3_fib_num3 :::"GenFib"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k3_fib_num3 :::"GenFib"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" ($#k1_pre_ff :::"Fib"::: ) (Set "(" (Set (Var "n")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Set "(" ($#k3_fib_num3 :::"GenFib"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Num 1) ")" ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" ($#k1_pre_ff :::"Fib"::: ) (Set (Var "n")) ")" ) ")" )))) ; theorem :: FIB_NUM3:43 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set "(" ($#k1_pre_ff :::"Fib"::: ) (Set (Var "m")) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" ($#k1_fib_num3 :::"Lucas"::: ) (Set (Var "n")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Set "(" ($#k1_fib_num3 :::"Lucas"::: ) (Set (Var "m")) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" ($#k1_pre_ff :::"Fib"::: ) (Set (Var "n")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_fib_num3 :::"GenFib"::: ) "(" (Set "(" ($#k1_pre_ff :::"Fib"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) "," (Set "(" ($#k1_fib_num3 :::"Lucas"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) "," (Set "(" (Set (Var "n")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "m")) ")" ) ")" ))) ; theorem :: FIB_NUM3:44 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k1_fib_num3 :::"Lucas"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k1_fib_num3 :::"Lucas"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k4_nat_1 :::"*"::: ) (Set "(" ($#k1_fib_num3 :::"Lucas"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" )))) ; theorem :: FIB_NUM3:45 (Bool "for" (Set (Var "a")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k3_fib_num3 :::"GenFib"::: ) "(" (Set (Var "a")) "," (Set (Var "a")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k3_fib_num3 :::"GenFib"::: ) "(" (Set (Var "a")) "," (Set (Var "a")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" ($#k1_pre_ff :::"Fib"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k1_fib_num3 :::"Lucas"::: ) (Set (Var "n")) ")" ) ")" )))) ; theorem :: FIB_NUM3:46 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k3_fib_num3 :::"GenFib"::: ) "(" (Set (Var "b")) "," (Set "(" (Set (Var "a")) ($#k2_nat_1 :::"+"::: ) (Set (Var "b")) ")" ) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_fib_num3 :::"GenFib"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))) ; theorem :: FIB_NUM3:47 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" ($#k3_fib_num3 :::"GenFib"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" ($#k3_fib_num3 :::"GenFib"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "n")) ")" ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" ($#k3_fib_num3 :::"GenFib"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ($#k13_newton :::"|^"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ($#k3_power :::"to_power"::: ) (Set (Var "n")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k3_fib_num3 :::"GenFib"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Num 2) ")" ")" ) ($#k13_newton :::"|^"::: ) (Num 2) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" ($#k3_fib_num3 :::"GenFib"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Num 1) ")" ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" ($#k3_fib_num3 :::"GenFib"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Num 3) ")" ")" ) ")" ) ")" )))) ; theorem :: FIB_NUM3:48 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "k")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k3_fib_num3 :::"GenFib"::: ) "(" (Set "(" ($#k3_fib_num3 :::"GenFib"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "k")) ")" ")" ) "," (Set "(" ($#k3_fib_num3 :::"GenFib"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_fib_num3 :::"GenFib"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Set (Var "k")) ")" ) ")" ))) ; theorem :: FIB_NUM3:49 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k3_fib_num3 :::"GenFib"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k4_nat_1 :::"*"::: ) (Set "(" ($#k1_pre_ff :::"Fib"::: ) (Set (Var "n")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k4_nat_1 :::"*"::: ) (Set "(" ($#k1_pre_ff :::"Fib"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" )))) ; theorem :: FIB_NUM3:50 (Bool "for" (Set (Var "b")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k3_fib_num3 :::"GenFib"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "b")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k4_nat_1 :::"*"::: ) (Set "(" ($#k1_pre_ff :::"Fib"::: ) (Set (Var "n")) ")" )))) ; theorem :: FIB_NUM3:51 (Bool "for" (Set (Var "a")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k3_fib_num3 :::"GenFib"::: ) "(" (Set (Var "a")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k4_nat_1 :::"*"::: ) (Set "(" ($#k1_pre_ff :::"Fib"::: ) (Set (Var "n")) ")" )))) ; theorem :: FIB_NUM3:52 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k3_fib_num3 :::"GenFib"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "n")) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k3_fib_num3 :::"GenFib"::: ) "(" (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "n")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_fib_num3 :::"GenFib"::: ) "(" (Set "(" (Set (Var "a")) ($#k2_nat_1 :::"+"::: ) (Set (Var "c")) ")" ) "," (Set "(" (Set (Var "b")) ($#k2_nat_1 :::"+"::: ) (Set (Var "d")) ")" ) "," (Set (Var "n")) ")" ))) ; theorem :: FIB_NUM3:53 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "k")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k3_fib_num3 :::"GenFib"::: ) "(" (Set "(" (Set (Var "k")) ($#k4_nat_1 :::"*"::: ) (Set (Var "a")) ")" ) "," (Set "(" (Set (Var "k")) ($#k4_nat_1 :::"*"::: ) (Set (Var "b")) ")" ) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "k")) ($#k4_nat_1 :::"*"::: ) (Set "(" ($#k3_fib_num3 :::"GenFib"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "n")) ")" ")" )))) ; theorem :: FIB_NUM3:54 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k3_fib_num3 :::"GenFib"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set ($#k2_fib_num :::"tau_bar"::: ) ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "b")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set ($#k1_fib_num :::"tau"::: ) ) ($#k3_power :::"to_power"::: ) (Set (Var "n")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set ($#k1_fib_num :::"tau"::: ) ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "b")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set ($#k2_fib_num :::"tau_bar"::: ) ) ($#k3_power :::"to_power"::: ) (Set (Var "n")) ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 5) ")" )))) ; theorem :: FIB_NUM3:55 (Bool "for" (Set (Var "a")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k3_fib_num3 :::"GenFib"::: ) "(" (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "a")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "a")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "a")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" ($#k1_pre_ff :::"Fib"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" )))) ;