:: BINARI_3  semantic presentation begin  
theorem :: BINARI_3:1 (Bool  "for" (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "F")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "n")) "," (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  )  "holds" (Bool (Set   ($#k6_binarith :::"Absval"::: )  (Set (Var "F")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Num 2)  ($#k5_series_1 :::"to_power"::: )  (Set (Var "n")))))) ; 
 
theorem :: BINARI_3:2 (Bool  "for" (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "F1")) "," (Set (Var "F2")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "n")) "," (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  )  "st" (Bool (Bool (Set   ($#k6_binarith :::"Absval"::: )  (Set (Var "F1")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_binarith :::"Absval"::: )  (Set (Var "F2"))))) "holds"  (Bool (Set (Var "F1"))  ($#r1_hidden :::"="::: )  (Set (Var "F2"))))) ; 
 
theorem :: BINARI_3:3 (Bool  "for" (Set (Var "t1")) "," (Set (Var "t2")) "being"   ($#m1_hidden :::"FinSequence":::)  "st" (Bool (Bool (Set   ($#k3_finseq_5 :::"Rev"::: )  (Set (Var "t1")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_5 :::"Rev"::: )  (Set (Var "t2"))))) "holds"  (Bool (Set (Var "t1"))  ($#r1_hidden :::"="::: )  (Set (Var "t2")))) ; 
 
theorem :: BINARI_3:4 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k5_euclid :::"0*"::: )  (Set (Var "n")))  ($#r2_hidden :::"in"::: )  (Set (Set  ($#k6_margrel1 :::"BOOLEAN"::: ) )  ($#k3_finseq_2 :::"*"::: )  ))) ; 
 
theorem :: BINARI_3:5 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "y")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "n")) "," (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  )  "st" (Bool (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_euclid :::"0*"::: )  (Set (Var "n"))))) "holds"  (Bool (Set   ($#k3_binarith :::"'not'"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k5_finseq_2 :::"|->"::: )  (Num 1))))) ; 
 
theorem :: BINARI_3:6 (Bool  "for" (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "F")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "n")) "," (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  )  "st" (Bool (Bool (Set (Var "F"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_euclid :::"0*"::: )  (Set (Var "n"))))) "holds"  (Bool (Set   ($#k6_binarith :::"Absval"::: )  (Set (Var "F")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )))) ; 
 
theorem :: BINARI_3:7 (Bool  "for" (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "F")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "n")) "," (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  )  "st" (Bool (Bool (Set (Var "F"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_euclid :::"0*"::: )  (Set (Var "n"))))) "holds"  (Bool (Set   ($#k6_binarith :::"Absval"::: )  (Set  "("  ($#k3_binarith :::"'not'"::: )  (Set (Var "F")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 2)  ($#k5_series_1 :::"to_power"::: )  (Set (Var "n")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Num 1))))) ; 
 
theorem :: BINARI_3:8 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k4_finseq_5 :::"Rev"::: )  (Set  "("  ($#k5_euclid :::"0*"::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k5_euclid :::"0*"::: )  (Set (Var "n"))))) ; 
 
theorem :: BINARI_3:9 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "y")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "n")) "," (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  )  "st" (Bool (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_euclid :::"0*"::: )  (Set (Var "n"))))) "holds"  (Bool (Set   ($#k4_finseq_5 :::"Rev"::: )  (Set  "("  ($#k3_binarith :::"'not'"::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_binarith :::"'not'"::: )  (Set (Var "y")))))) ; 
 
theorem :: BINARI_3:10 (Bool (Set   ($#k1_binari_2 :::"Bin1"::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set  ($#k10_binarith :::"<*"::: ) (Set  ($#k8_margrel1 :::"TRUE"::: ) ) ($#k10_binarith :::"*>"::: ) )) ; 
 
theorem :: BINARI_3:11 (Bool  "for" (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k6_binarith :::"Absval"::: )  (Set  "("  ($#k1_binari_2 :::"Bin1"::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: BINARI_3:12 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  ) "holds"   (Bool  "("  (Bool  "("   "not" (Bool (Set (Set (Var "x"))  ($#k1_binarith :::"'or'"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set   ($#k8_margrel1 :::"TRUE"::: )  )) "or" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k8_margrel1 :::"TRUE"::: )  )) "or" (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k8_margrel1 :::"TRUE"::: )  ))  ")" ) &  "("  (Bool (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k8_margrel1 :::"TRUE"::: )  )) "or" (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k8_margrel1 :::"TRUE"::: )  ))  ")" )) "implies" (Bool (Set (Set (Var "x"))  ($#k1_binarith :::"'or'"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set   ($#k8_margrel1 :::"TRUE"::: )  ))  ")"  &  "("  (Bool (Bool (Set (Set (Var "x"))  ($#k1_binarith :::"'or'"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set   ($#k7_margrel1 :::"FALSE"::: )  ))) "implies" (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k7_margrel1 :::"FALSE"::: )  )) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k7_margrel1 :::"FALSE"::: )  ))  ")" )  ")"  &  "("  (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k7_margrel1 :::"FALSE"::: )  )) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k7_margrel1 :::"FALSE"::: )  ))) "implies" (Bool (Set (Set (Var "x"))  ($#k1_binarith :::"'or'"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set   ($#k7_margrel1 :::"FALSE"::: )  ))  ")"   ")" )) ; 
 
theorem :: BINARI_3:13 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  ) "holds"   (Bool  "("  (Bool (Set   ($#k8_binarith :::"add_ovfl"::: )   "(" (Set  ($#k10_binarith :::"<*"::: ) (Set (Var "x")) ($#k10_binarith :::"*>"::: ) ) "," (Set  ($#k10_binarith :::"<*"::: ) (Set (Var "y")) ($#k10_binarith :::"*>"::: ) ) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k8_margrel1 :::"TRUE"::: )  )) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k8_margrel1 :::"TRUE"::: )  )) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k8_margrel1 :::"TRUE"::: )  ))  ")" )  ")" )) ; 
 
theorem :: BINARI_3:14 (Bool (Set   ($#k3_binarith :::"'not'"::: )  (Set  ($#k10_binarith :::"<*"::: ) (Set  ($#k7_margrel1 :::"FALSE"::: ) ) ($#k10_binarith :::"*>"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k10_binarith :::"<*"::: ) (Set  ($#k8_margrel1 :::"TRUE"::: ) ) ($#k10_binarith :::"*>"::: ) )) ; 
 
theorem :: BINARI_3:15 (Bool (Set   ($#k3_binarith :::"'not'"::: )  (Set  ($#k10_binarith :::"<*"::: ) (Set  ($#k8_margrel1 :::"TRUE"::: ) ) ($#k10_binarith :::"*>"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k10_binarith :::"<*"::: ) (Set  ($#k7_margrel1 :::"FALSE"::: ) ) ($#k10_binarith :::"*>"::: ) )) ; 
 
theorem :: BINARI_3:16 (Bool (Set (Set  ($#k10_binarith :::"<*"::: ) (Set  ($#k7_margrel1 :::"FALSE"::: ) ) ($#k10_binarith :::"*>"::: ) )  ($#k7_binarith :::"+"::: )  (Set  ($#k10_binarith :::"<*"::: ) (Set  ($#k7_margrel1 :::"FALSE"::: ) ) ($#k10_binarith :::"*>"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k10_binarith :::"<*"::: ) (Set  ($#k7_margrel1 :::"FALSE"::: ) ) ($#k10_binarith :::"*>"::: ) )) ; 
 
theorem :: BINARI_3:17 (Bool  "("  (Bool (Set (Set  ($#k10_binarith :::"<*"::: ) (Set  ($#k7_margrel1 :::"FALSE"::: ) ) ($#k10_binarith :::"*>"::: ) )  ($#k7_binarith :::"+"::: )  (Set  ($#k10_binarith :::"<*"::: ) (Set  ($#k8_margrel1 :::"TRUE"::: ) ) ($#k10_binarith :::"*>"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k10_binarith :::"<*"::: ) (Set  ($#k8_margrel1 :::"TRUE"::: ) ) ($#k10_binarith :::"*>"::: ) )) & (Bool (Set (Set  ($#k10_binarith :::"<*"::: ) (Set  ($#k8_margrel1 :::"TRUE"::: ) ) ($#k10_binarith :::"*>"::: ) )  ($#k7_binarith :::"+"::: )  (Set  ($#k10_binarith :::"<*"::: ) (Set  ($#k7_margrel1 :::"FALSE"::: ) ) ($#k10_binarith :::"*>"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k10_binarith :::"<*"::: ) (Set  ($#k8_margrel1 :::"TRUE"::: ) ) ($#k10_binarith :::"*>"::: ) ))  ")" ) ; 
 
theorem :: BINARI_3:18 (Bool (Set (Set  ($#k10_binarith :::"<*"::: ) (Set  ($#k8_margrel1 :::"TRUE"::: ) ) ($#k10_binarith :::"*>"::: ) )  ($#k7_binarith :::"+"::: )  (Set  ($#k10_binarith :::"<*"::: ) (Set  ($#k8_margrel1 :::"TRUE"::: ) ) ($#k10_binarith :::"*>"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k10_binarith :::"<*"::: ) (Set  ($#k7_margrel1 :::"FALSE"::: ) ) ($#k10_binarith :::"*>"::: ) )) ; 
 
theorem :: BINARI_3:19 (Bool  "for" (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "n")) "," (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  )  "st" (Bool (Bool (Set (Set (Var "x"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k8_margrel1 :::"TRUE"::: )  )) & (Bool (Set (Set  "("  ($#k4_binarith :::"carry"::: )   "(" (Set (Var "x")) "," (Set  "("  ($#k1_binari_2 :::"Bin1"::: )  (Set (Var "n")) ")" ) ")"  ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k8_margrel1 :::"TRUE"::: )  ))) "holds"  (Bool  "for" (Set (Var "k")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r1_hidden :::"<>"::: )  (Num 1)) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "x"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set   ($#k8_margrel1 :::"TRUE"::: )  )) & (Bool (Set (Set  "("  ($#k4_binarith :::"carry"::: )   "(" (Set (Var "x")) "," (Set  "("  ($#k1_binari_2 :::"Bin1"::: )  (Set (Var "n")) ")" ) ")"  ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set   ($#k8_margrel1 :::"TRUE"::: )  ))  ")" )))) ; 
 
theorem :: BINARI_3:20 (Bool  "for" (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "n")) "," (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  )  "st" (Bool (Bool (Set (Set (Var "x"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k8_margrel1 :::"TRUE"::: )  )) & (Bool (Set (Set  "("  ($#k4_binarith :::"carry"::: )   "(" (Set (Var "x")) "," (Set  "("  ($#k1_binari_2 :::"Bin1"::: )  (Set (Var "n")) ")" ) ")"  ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k8_margrel1 :::"TRUE"::: )  ))) "holds"  (Bool (Set   ($#k4_binarith :::"carry"::: )   "(" (Set (Var "x")) "," (Set  "("  ($#k1_binari_2 :::"Bin1"::: )  (Set (Var "n")) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k3_binarith :::"'not'"::: )  (Set  "("  ($#k1_binari_2 :::"Bin1"::: )  (Set (Var "n")) ")" ))))) ; 
 
theorem :: BINARI_3:21 (Bool  "for" (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "n")) "," (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  )  "st" (Bool (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_euclid :::"0*"::: )  (Set (Var "n")))) & (Bool (Set (Set (Var "x"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k8_margrel1 :::"TRUE"::: )  )) & (Bool (Set (Set  "("  ($#k4_binarith :::"carry"::: )   "(" (Set (Var "x")) "," (Set  "("  ($#k1_binari_2 :::"Bin1"::: )  (Set (Var "n")) ")" ) ")"  ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k8_margrel1 :::"TRUE"::: )  ))) "holds"  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_binarith :::"'not'"::: )  (Set (Var "y")))))) ; 
 
theorem :: BINARI_3:22 (Bool  "for" (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "y")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "n")) "," (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  )  "st" (Bool (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_euclid :::"0*"::: )  (Set (Var "n"))))) "holds"  (Bool (Set   ($#k4_binarith :::"carry"::: )   "(" (Set  "("  ($#k3_binarith :::"'not'"::: )  (Set (Var "y")) ")" ) "," (Set  "("  ($#k1_binari_2 :::"Bin1"::: )  (Set (Var "n")) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k3_binarith :::"'not'"::: )  (Set  "("  ($#k1_binari_2 :::"Bin1"::: )  (Set (Var "n")) ")" ))))) ; 
 
theorem :: BINARI_3:23 (Bool  "for" (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "n")) "," (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  )  "st" (Bool (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_euclid :::"0*"::: )  (Set (Var "n"))))) "holds"  (Bool  "("  (Bool (Set   ($#k8_binarith :::"add_ovfl"::: )   "(" (Set (Var "x")) "," (Set  "("  ($#k1_binari_2 :::"Bin1"::: )  (Set (Var "n")) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k8_margrel1 :::"TRUE"::: )  )) "iff" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_binarith :::"'not'"::: )  (Set (Var "y"))))  ")" ))) ; 
 
theorem :: BINARI_3:24 (Bool  "for" (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "z")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "n")) "," (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  )  "st" (Bool (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_euclid :::"0*"::: )  (Set (Var "n"))))) "holds"  (Bool (Set (Set  "("  ($#k3_binarith :::"'not'"::: )  (Set (Var "z")) ")" )  ($#k7_binarith :::"+"::: )  (Set  "("  ($#k1_binari_2 :::"Bin1"::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "z"))))) ; 
 begin  definitionlet "n", "k" be   ($#m1_hidden :::"Nat":::); func "n" :::"-BinarySequence"::: "k" ->   ($#m2_finseq_1 :::"Tuple":::) "of" "n" "," (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  ) means :: BINARI_3:def 1 (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  "n"))) "holds"  (Bool (Set it  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set   ($#k15_funcop_1 :::"IFEQ"::: )   "(" (Set  "(" (Set  "(" "k"  ($#k3_nat_d :::"div"::: )  (Set  "(" (Num 2)  ($#k5_series_1 :::"to_power"::: )  (Set  "(" (Set (Var "i"))  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) ")" ) ")" )  ($#k4_nat_d :::"mod"::: )  (Num 2) ")" ) "," (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  ($#k7_margrel1 :::"FALSE"::: ) ) "," (Set  ($#k8_margrel1 :::"TRUE"::: ) ) ")" ))); end; 






:: deftheorem    defines :::"-BinarySequence"::: BINARI_3:def 1 :  (Bool  "for" (Set (Var "n")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "b3")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "n")) "," (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k1_binari_3 :::"-BinarySequence"::: )  (Set (Var "k")))) "iff" (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n"))))) "holds"  (Bool (Set (Set (Var "b3"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set   ($#k15_funcop_1 :::"IFEQ"::: )   "(" (Set  "(" (Set  "(" (Set (Var "k"))  ($#k3_nat_d :::"div"::: )  (Set  "(" (Num 2)  ($#k5_series_1 :::"to_power"::: )  (Set  "(" (Set (Var "i"))  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) ")" ) ")" )  ($#k4_nat_d :::"mod"::: )  (Num 2) ")" ) "," (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  ($#k7_margrel1 :::"FALSE"::: ) ) "," (Set  ($#k8_margrel1 :::"TRUE"::: ) ) ")" )))  ")" ))); 
 
theorem :: BINARI_3:25 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set (Var "n"))  ($#k1_binari_3 :::"-BinarySequence"::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k5_euclid :::"0*"::: )  (Set (Var "n"))))) ; 
 
theorem :: BINARI_3:26 (Bool  "for" (Set (Var "n")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Num 2)  ($#k5_series_1 :::"to_power"::: )  (Set (Var "n"))))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k1_binari_3 :::"-BinarySequence"::: )  (Set (Var "k")) ")" )  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k7_margrel1 :::"FALSE"::: )  ))) ; 
 
theorem :: BINARI_3:27 (Bool  "for" (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Num 2)  ($#k5_series_1 :::"to_power"::: )  (Set (Var "n"))))) "holds"  (Bool (Set (Set  "(" (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k1_binari_3 :::"-BinarySequence"::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "n"))  ($#k1_binari_3 :::"-BinarySequence"::: )  (Set (Var "k")) ")" )  ($#k9_binarith :::"^"::: )  (Set  ($#k10_binarith :::"<*"::: ) (Set  ($#k7_margrel1 :::"FALSE"::: ) ) ($#k10_binarith :::"*>"::: ) ))))) ; 
 
theorem :: BINARI_3:28 (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k1_binari_3 :::"-BinarySequence"::: )  (Set  "(" (Num 2)  ($#k5_series_1 :::"to_power"::: )  (Set (Var "i")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_euclid :::"0*"::: )  (Set (Var "i")) ")" )  ($#k7_finseq_1 :::"^"::: )  (Set  ($#k10_binarith :::"<*"::: ) (Num 1) ($#k10_binarith :::"*>"::: ) )))) ; 
 
theorem :: BINARI_3:29 (Bool  "for" (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Num 2)  ($#k5_series_1 :::"to_power"::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k"))) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Num 2)  ($#k5_series_1 :::"to_power"::: )  (Set  "(" (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k1_binari_3 :::"-BinarySequence"::: )  (Set (Var "k")) ")" )  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k8_margrel1 :::"TRUE"::: )  )))) ; 
 
theorem :: BINARI_3:30 (Bool  "for" (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Num 2)  ($#k5_series_1 :::"to_power"::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k"))) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Num 2)  ($#k5_series_1 :::"to_power"::: )  (Set  "(" (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )))) "holds"  (Bool (Set (Set  "(" (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k1_binari_3 :::"-BinarySequence"::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "n"))  ($#k1_binari_3 :::"-BinarySequence"::: )  (Set  "(" (Set (Var "k"))  ($#k7_nat_d :::"-'"::: )  (Set  "(" (Num 2)  ($#k5_series_1 :::"to_power"::: )  (Set (Var "n")) ")" ) ")" ) ")" )  ($#k9_binarith :::"^"::: )  (Set  ($#k10_binarith :::"<*"::: ) (Set  ($#k8_margrel1 :::"TRUE"::: ) ) ($#k10_binarith :::"*>"::: ) ))))) ; 
 
theorem :: BINARI_3:31 (Bool  "for" (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Num 2)  ($#k5_series_1 :::"to_power"::: )  (Set (Var "n"))))) "holds"  (Bool  "for" (Set (Var "x")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "n")) "," (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  )  "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_euclid :::"0*"::: )  (Set (Var "n"))))) "holds"  (Bool  "("  (Bool (Set (Set (Var "n"))  ($#k1_binari_3 :::"-BinarySequence"::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_binarith :::"'not'"::: )  (Set (Var "x")))) "iff" (Bool (Set (Var "k"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 2)  ($#k5_series_1 :::"to_power"::: )  (Set (Var "n")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Num 1)))  ")" )))) ; 
 
theorem :: BINARI_3:32 (Bool  "for" (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Set (Var "k"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<"::: )  (Set (Num 2)  ($#k5_series_1 :::"to_power"::: )  (Set (Var "n"))))) "holds"  (Bool (Set   ($#k8_binarith :::"add_ovfl"::: )   "(" (Set  "(" (Set (Var "n"))  ($#k1_binari_3 :::"-BinarySequence"::: )  (Set (Var "k")) ")" ) "," (Set  "("  ($#k1_binari_2 :::"Bin1"::: )  (Set (Var "n")) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k7_margrel1 :::"FALSE"::: )  )))) ; 
 
theorem :: BINARI_3:33 (Bool  "for" (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Set (Var "k"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<"::: )  (Set (Num 2)  ($#k5_series_1 :::"to_power"::: )  (Set (Var "n"))))) "holds"  (Bool (Set (Set (Var "n"))  ($#k1_binari_3 :::"-BinarySequence"::: )  (Set  "(" (Set (Var "k"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "n"))  ($#k1_binari_3 :::"-BinarySequence"::: )  (Set (Var "k")) ")" )  ($#k7_binarith :::"+"::: )  (Set  "("  ($#k1_binari_2 :::"Bin1"::: )  (Set (Var "n")) ")" ))))) ; 
 
theorem :: BINARI_3:34 (Bool  "for" (Set (Var "n")) "," (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "(" (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k1_binari_3 :::"-BinarySequence"::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k10_binarith :::"<*"::: ) (Set  "(" (Set (Var "i"))  ($#k4_nat_d :::"mod"::: )  (Num 2) ")" ) ($#k10_binarith :::"*>"::: ) )  ($#k7_finseq_1 :::"^"::: )  (Set  "(" (Set (Var "n"))  ($#k1_binari_3 :::"-BinarySequence"::: )  (Set  "(" (Set (Var "i"))  ($#k3_nat_d :::"div"::: )  (Num 2) ")" ) ")" )))) ; 
 
theorem :: BINARI_3:35 (Bool  "for" (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Num 2)  ($#k5_series_1 :::"to_power"::: )  (Set (Var "n"))))) "holds"  (Bool (Set   ($#k6_binarith :::"Absval"::: )  (Set  "(" (Set (Var "n"))  ($#k1_binari_3 :::"-BinarySequence"::: )  (Set (Var "k")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "k"))))) ; 
 
theorem :: BINARI_3:36 (Bool  "for" (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "n")) "," (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  ) "holds"  (Bool (Set (Set (Var "n"))  ($#k1_binari_3 :::"-BinarySequence"::: )  (Set  "("  ($#k6_binarith :::"Absval"::: )  (Set (Var "x")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "x"))))) ;