:: PRE_FF semantic presentation begin definitionlet "n" be ($#m1_hidden :::"Nat":::); func :::"Fib"::: "n" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: PRE_FF:def 1 (Bool "ex" (Set (Var "fib")) "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 "fib")) ($#k8_nat_1 :::"."::: ) "n" ")" ) ($#k2_domain_1 :::"`1"::: ) )) & (Bool (Set (Set (Var "fib")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k1_domain_1 :::"]"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "fib")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set "(" (Set (Var "fib")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k3_domain_1 :::"`2"::: ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set (Var "fib")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k2_domain_1 :::"`1"::: ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "fib")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k3_domain_1 :::"`2"::: ) ")" ) ")" ) ($#k1_domain_1 :::"]"::: ) )) ")" ) ")" )); end; :: deftheorem defines :::"Fib"::: PRE_FF: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_pre_ff :::"Fib"::: ) (Set (Var "n")))) "iff" (Bool "ex" (Set (Var "fib")) "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 "fib")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k2_domain_1 :::"`1"::: ) )) & (Bool (Set (Set (Var "fib")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k1_domain_1 :::"]"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "fib")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set "(" (Set (Var "fib")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k3_domain_1 :::"`2"::: ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set (Var "fib")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k2_domain_1 :::"`1"::: ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "fib")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k3_domain_1 :::"`2"::: ) ")" ) ")" ) ($#k1_domain_1 :::"]"::: ) )) ")" ) ")" )) ")" ))); theorem :: PRE_FF:1 (Bool "(" (Bool (Set ($#k1_pre_ff :::"Fib"::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k1_pre_ff :::"Fib"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k1_pre_ff :::"Fib"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k2_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 1) ")" ) ")" ))) ")" ) ")" ) ; theorem :: PRE_FF:2 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set (Set (Var "i")) ($#k5_int_1 :::"div"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "i")))) ; theorem :: PRE_FF:3 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "j")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "i")) ($#k5_int_1 :::"div"::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j")))) ; theorem :: PRE_FF:4 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j")))) "holds" (Bool (Set (Set (Var "i")) ($#k5_int_1 :::"div"::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: PRE_FF:5 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "i")) ($#k5_int_1 :::"div"::: ) (Set (Var "j")) ")" ) ($#k5_int_1 :::"div"::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k5_int_1 :::"div"::: ) (Set "(" (Set (Var "j")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "k")) ")" )))) ; theorem :: PRE_FF:6 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool "(" (Bool (Set (Set (Var "i")) ($#k6_int_1 :::"mod"::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set (Set (Var "i")) ($#k6_int_1 :::"mod"::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Num 1)) ")" )) ; theorem :: PRE_FF:7 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "i")) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ))) "holds" (Bool (Set (Set (Var "i")) ($#k5_int_1 :::"div"::: ) (Num 2)) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ))) ; theorem :: PRE_FF:8 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b"))) & (Bool (Set (Var "c")) ($#r1_xxreal_0 :::">"::: ) (Num 1))) "holds" (Bool (Set (Set (Var "c")) ($#k3_power :::"to_power"::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "c")) ($#k3_power :::"to_power"::: ) (Set (Var "b"))))) ; theorem :: PRE_FF:9 (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "s")))) "holds" (Bool (Set ($#k1_int_1 :::"[\"::: ) (Set (Var "r")) ($#k1_int_1 :::"/]"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set ($#k1_int_1 :::"[\"::: ) (Set (Var "s")) ($#k1_int_1 :::"/]"::: ) ))) ; theorem :: PRE_FF:10 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::">"::: ) (Num 1)) & (Bool (Set (Var "b")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "c")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "b")))) "holds" (Bool (Set ($#k5_power :::"log"::: ) "(" (Set (Var "a")) "," (Set (Var "c")) ")" ) ($#r1_xxreal_0 :::">="::: ) (Set ($#k5_power :::"log"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))) ; theorem :: PRE_FF:11 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set ($#k1_int_1 :::"[\"::: ) (Set "(" ($#k6_power :::"log"::: ) "(" (Num 2) "," (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ")" ")" ) ($#k1_int_1 :::"/]"::: ) ) ($#k2_xcmplx_0 :::"+"::: ) (Num 1)) ($#r1_hidden :::"<>"::: ) (Set ($#k1_int_1 :::"[\"::: ) (Set "(" ($#k6_power :::"log"::: ) "(" (Num 2) "," (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ($#k1_int_1 :::"/]"::: ) ))) ; theorem :: PRE_FF:12 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set ($#k1_int_1 :::"[\"::: ) (Set "(" ($#k6_power :::"log"::: ) "(" (Num 2) "," (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ")" ")" ) ($#k1_int_1 :::"/]"::: ) ) ($#k2_xcmplx_0 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::">="::: ) (Set ($#k1_int_1 :::"[\"::: ) (Set "(" ($#k6_power :::"log"::: ) "(" (Num 2) "," (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ($#k1_int_1 :::"/]"::: ) ))) ; theorem :: PRE_FF:13 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k1_int_1 :::"[\"::: ) (Set "(" ($#k6_power :::"log"::: ) "(" (Num 2) "," (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ")" ")" ) ($#k1_int_1 :::"/]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_int_1 :::"[\"::: ) (Set "(" ($#k6_power :::"log"::: ) "(" (Num 2) "," (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ($#k1_int_1 :::"/]"::: ) ))) ; theorem :: PRE_FF:14 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set ($#k1_int_1 :::"[\"::: ) (Set "(" ($#k5_power :::"log"::: ) "(" (Num 2) "," (Set (Var "n")) ")" ")" ) ($#k1_int_1 :::"/]"::: ) ) ($#k2_xcmplx_0 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k1_int_1 :::"[\"::: ) (Set "(" ($#k6_power :::"log"::: ) "(" (Num 2) "," (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ($#k1_int_1 :::"/]"::: ) ))) ; definitionlet "f" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ")" ); let "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); :: original: :::"."::: redefine func "f" :::"."::: "n" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); end; definitionlet "n" be ($#m1_hidden :::"Nat":::); func :::"Fusc"::: "n" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: PRE_FF:def 2 (Bool it ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) if (Bool "n" ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) otherwise (Bool "ex" (Set (Var "l")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )(Bool "ex" (Set (Var "fusc")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ")" ) "st" (Bool "(" (Bool (Set (Set (Var "l")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) "n") & (Bool it ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "fusc")) ($#k2_pre_ff :::"."::: ) (Set (Var "l")) ")" ) ($#k7_partfun1 :::"/."::: ) "n")) & (Bool (Set (Set (Var "fusc")) ($#k2_pre_ff :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "k"))))) "holds" (Bool (Set (Set (Var "fusc")) ($#k2_pre_ff :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "fusc")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set "(" (Set (Var "fusc")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "k")) ")" ) ($#k12_finseq_1 :::"*>"::: ) ))) ")" ) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "k")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1)))) "holds" (Bool (Set (Set (Var "fusc")) ($#k2_pre_ff :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "fusc")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "fusc")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "k")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "fusc")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "k")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k12_finseq_1 :::"*>"::: ) ))) ")" ) ")" ) ")" ) ")" ))); end; :: deftheorem defines :::"Fusc"::: PRE_FF:def 2 : (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 (Bool (Set (Var "n")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k3_pre_ff :::"Fusc"::: ) (Set (Var "n")))) "iff" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "n")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k3_pre_ff :::"Fusc"::: ) (Set (Var "n")))) "iff" (Bool "ex" (Set (Var "l")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )(Bool "ex" (Set (Var "fusc")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ")" ) "st" (Bool "(" (Bool (Set (Set (Var "l")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "fusc")) ($#k2_pre_ff :::"."::: ) (Set (Var "l")) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "n")))) & (Bool (Set (Set (Var "fusc")) ($#k2_pre_ff :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "k"))))) "holds" (Bool (Set (Set (Var "fusc")) ($#k2_pre_ff :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "fusc")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set "(" (Set (Var "fusc")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "k")) ")" ) ($#k12_finseq_1 :::"*>"::: ) ))) ")" ) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "k")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1)))) "holds" (Bool (Set (Set (Var "fusc")) ($#k2_pre_ff :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "fusc")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "fusc")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "k")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "fusc")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "k")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k12_finseq_1 :::"*>"::: ) ))) ")" ) ")" ) ")" ) ")" ))) ")" ) ")" ")" ))); theorem :: PRE_FF:15 (Bool "(" (Bool (Set ($#k3_pre_ff :::"Fusc"::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k3_pre_ff :::"Fusc"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set ($#k3_pre_ff :::"Fusc"::: ) (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_pre_ff :::"Fusc"::: ) (Set (Var "n")))) & (Bool (Set ($#k3_pre_ff :::"Fusc"::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_pre_ff :::"Fusc"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k3_pre_ff :::"Fusc"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))) ")" ) ")" ) ")" ) ; theorem :: PRE_FF:16 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n"))))) ; theorem :: PRE_FF:17 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1)))) ; theorem :: PRE_FF:18 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k3_nat_1 :::"*"::: ) (Set "(" ($#k3_pre_ff :::"Fusc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Set (Var "B")) ($#k3_nat_1 :::"*"::: ) (Set "(" ($#k3_pre_ff :::"Fusc"::: ) (Num 1) ")" ) ")" )))) ; theorem :: PRE_FF:19 (Bool "for" (Set (Var "n")) "," (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "N")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k3_pre_ff :::"Fusc"::: ) (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k3_nat_1 :::"*"::: ) (Set "(" ($#k3_pre_ff :::"Fusc"::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Set (Var "B")) ($#k3_nat_1 :::"*"::: ) (Set "(" ($#k3_pre_ff :::"Fusc"::: ) (Set "(" (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" )))) "holds" (Bool (Set ($#k3_pre_ff :::"Fusc"::: ) (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k3_nat_1 :::"*"::: ) (Set "(" ($#k3_pre_ff :::"Fusc"::: ) (Set (Var "n")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "B")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "A")) ")" ) ($#k3_nat_1 :::"*"::: ) (Set "(" ($#k3_pre_ff :::"Fusc"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" )))) ; theorem :: PRE_FF:20 (Bool "for" (Set (Var "n")) "," (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "N")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k3_pre_ff :::"Fusc"::: ) (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k3_nat_1 :::"*"::: ) (Set "(" ($#k3_pre_ff :::"Fusc"::: ) (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Set (Var "B")) ($#k3_nat_1 :::"*"::: ) (Set "(" ($#k3_pre_ff :::"Fusc"::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" )))) "holds" (Bool (Set ($#k3_pre_ff :::"Fusc"::: ) (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "A")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "B")) ")" ) ($#k3_nat_1 :::"*"::: ) (Set "(" ($#k3_pre_ff :::"Fusc"::: ) (Set (Var "n")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Set (Var "B")) ($#k3_nat_1 :::"*"::: ) (Set "(" ($#k3_pre_ff :::"Fusc"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" )))) ;