:: BINARITH  semantic presentation begin  
theorem :: BINARITH:1 (Bool  "for" (Set (Var "i")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "d")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "D"))  (Bool  "for" (Set (Var "z")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "n")) "," (Set (Var "D"))  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n"))))) "holds"  (Bool (Set (Set  "(" (Set (Var "z"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "d")) ($#k12_finseq_1 :::"*>"::: ) ) ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "z"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")))))))) ; 
 
theorem :: BINARITH:2 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "d")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "D"))  (Bool  "for" (Set (Var "z")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "n")) "," (Set (Var "D")) "holds"  (Bool (Set (Set  "(" (Set (Var "z"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "d")) ($#k12_finseq_1 :::"*>"::: ) ) ")" )  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "d"))))))) ; 
 definitionlet "x", "y" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  ); :: original: :::"'or'"::: redefine func "x" :::"'or'"::: "y" ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  ); :: original: :::"'xor'"::: redefine func "x" :::"'xor'"::: "y" ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  ); end; 





theorem :: BINARITH:3 (Bool  "for" (Set (Var "x")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set (Var "x"))  ($#k5_xboolean :::"'or'"::: )  (Set  ($#k7_margrel1 :::"FALSE"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "x")))) ; 
 
theorem :: BINARITH:4 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k3_xboolean :::"'not'"::: )  (Set  "(" (Set (Var "x"))  ($#k4_xboolean :::"'&'"::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "x")) ")" )  ($#k5_xboolean :::"'or'"::: )  (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "y")) ")" )))) ; 
 
theorem :: BINARITH:5 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k3_xboolean :::"'not'"::: )  (Set  "(" (Set (Var "x"))  ($#k5_xboolean :::"'or'"::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "x")) ")" )  ($#k4_xboolean :::"'&'"::: )  (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "y")) ")" )))) ; 
 
theorem :: BINARITH:6 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set (Var "x"))  ($#k4_xboolean :::"'&'"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_xboolean :::"'not'"::: )  (Set  "(" (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "x")) ")" )  ($#k5_xboolean :::"'or'"::: )  (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "y")) ")" ) ")" )))) ; 
 
theorem :: BINARITH:7 (Bool  "for" (Set (Var "x")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set  ($#k8_margrel1 :::"TRUE"::: ) )  ($#k10_xboolean :::"'xor'"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_xboolean :::"'not'"::: )  (Set (Var "x"))))) ; 
 
theorem :: BINARITH:8 (Bool  "for" (Set (Var "x")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set  ($#k7_margrel1 :::"FALSE"::: ) )  ($#k10_xboolean :::"'xor'"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Var "x")))) ; 
 
theorem :: BINARITH:9 (Bool  "for" (Set (Var "x")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set (Var "x"))  ($#k4_xboolean :::"'&'"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Var "x")))) ; 
 
theorem :: BINARITH:10 (Bool  "for" (Set (Var "x")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set (Var "x"))  ($#k5_xboolean :::"'or'"::: )  (Set  ($#k8_margrel1 :::"TRUE"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k8_margrel1 :::"TRUE"::: )  ))) ; 
 
theorem :: BINARITH:11 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k5_xboolean :::"'or'"::: )  (Set (Var "y")) ")" )  ($#k5_xboolean :::"'or'"::: )  (Set (Var "z")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k5_xboolean :::"'or'"::: )  (Set  "(" (Set (Var "y"))  ($#k5_xboolean :::"'or'"::: )  (Set (Var "z")) ")" )))) ; 
 
theorem :: BINARITH:12 (Bool  "for" (Set (Var "x")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set (Var "x"))  ($#k5_xboolean :::"'or'"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Var "x")))) ; 
 
theorem :: BINARITH:13 (Bool (Set (Set  ($#k8_margrel1 :::"TRUE"::: ) )  ($#k2_binarith :::"'xor'"::: )  (Set  ($#k7_margrel1 :::"FALSE"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k8_margrel1 :::"TRUE"::: )  )) ; 
 













definitionlet "n" be   ($#m1_hidden :::"Nat":::); let "x" be   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Const "n")) "," (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  ); func  :::"'not'"::: "x" ->   ($#m2_finseq_1 :::"Tuple":::) "of" "n" "," (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  ) means :: BINARITH: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   ($#k9_margrel1 :::"'not'"::: )  (Set  "(" "x"  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" )))); end; 






:: deftheorem    defines :::"'not'"::: BINARITH:def 1 :  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "x")) "," (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   ($#k3_binarith :::"'not'"::: )  (Set (Var "x")))) "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   ($#k9_margrel1 :::"'not'"::: )  (Set  "(" (Set (Var "x"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" ))))  ")" ))); 
 definitionlet "n" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"Nat":::); let "x", "y" be   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Const "n")) "," (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  ); func  :::"carry":::  "(" "x" "," "y" ")"  ->   ($#m2_finseq_1 :::"Tuple":::) "of" "n" "," (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  ) means :: BINARITH:def 2 (Bool  "("  (Bool (Set it  ($#k7_partfun1 :::"/."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set   ($#k7_margrel1 :::"FALSE"::: )  )) & (Bool  "("   "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  "n")) "holds"  (Bool (Set it  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "i"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" "x"  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" )  ($#k10_margrel1 :::"'&'"::: )  (Set  "(" "y"  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" ) ")" )  ($#k1_binarith :::"'or'"::: )  (Set  "(" (Set  "(" "x"  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" )  ($#k10_margrel1 :::"'&'"::: )  (Set  "(" it  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" ) ")" ) ")" )  ($#k1_binarith :::"'or'"::: )  (Set  "(" (Set  "(" "y"  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" )  ($#k10_margrel1 :::"'&'"::: )  (Set  "(" it  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" ) ")" )))  ")" )  ")" ); end; 







:: deftheorem    defines :::"carry"::: BINARITH:def 2 :  (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")) "," (Set (Var "b4")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "n")) "," (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_binarith :::"carry"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) "iff" (Bool  "("  (Bool (Set (Set (Var "b4"))  ($#k7_partfun1 :::"/."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set   ($#k7_margrel1 :::"FALSE"::: )  )) & (Bool  "("   "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "n")))) "holds"  (Bool (Set (Set (Var "b4"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "i"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "x"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" )  ($#k10_margrel1 :::"'&'"::: )  (Set  "(" (Set (Var "y"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" ) ")" )  ($#k1_binarith :::"'or'"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" )  ($#k10_margrel1 :::"'&'"::: )  (Set  "(" (Set (Var "b4"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" ) ")" ) ")" )  ($#k1_binarith :::"'or'"::: )  (Set  "(" (Set  "(" (Set (Var "y"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" )  ($#k10_margrel1 :::"'&'"::: )  (Set  "(" (Set (Var "b4"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" ) ")" )))  ")" )  ")" )  ")" ))); 
 definitionlet "n" be   ($#m1_hidden :::"Nat":::); let "x" be   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Const "n")) "," (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  ); func  :::"Binary"::: "x" ->   ($#m2_finseq_1 :::"Tuple":::) "of" "n" "," (Set   ($#k5_numbers :::"NAT"::: )  ) means :: BINARITH:def 3 (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  "(" "x"  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" ) "," (Set  ($#k7_margrel1 :::"FALSE"::: ) ) "," (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  "(" (Num 2)  ($#k5_series_1 :::"to_power"::: )  (Set  "(" (Set (Var "i"))  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) ")" ) ")" ))); end; 






:: deftheorem    defines :::"Binary"::: BINARITH:def 3 :  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "n")) "," (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  )  (Bool  "for" (Set (Var "b3")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "n")) "," (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_binarith :::"Binary"::: )  (Set (Var "x")))) "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 (Var "x"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" ) "," (Set  ($#k7_margrel1 :::"FALSE"::: ) ) "," (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  "(" (Num 2)  ($#k5_series_1 :::"to_power"::: )  (Set  "(" (Set (Var "i"))  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) ")" ) ")" )))  ")" )))); 
 definitionlet "n" be   ($#m1_hidden :::"Nat":::); let "x" be   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Const "n")) "," (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  ); func  :::"Absval"::: "x" ->    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) equals :: BINARITH:def 4 (Set (Set  ($#k47_binop_2 :::"addnat"::: ) )  ($#k1_finsop_1 :::"$$"::: )  (Set  "("  ($#k5_binarith :::"Binary"::: )  "x" ")" )); end; 






:: deftheorem    defines :::"Absval"::: BINARITH:def 4 :  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "n")) "," (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  ) "holds"  (Bool (Set   ($#k6_binarith :::"Absval"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k47_binop_2 :::"addnat"::: ) )  ($#k1_finsop_1 :::"$$"::: )  (Set  "("  ($#k5_binarith :::"Binary"::: )  (Set (Var "x")) ")" ))))); 
 definitionlet "n" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"zero"::: )   )   ($#m1_hidden :::"Nat":::); let "x", "y" be   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Const "n")) "," (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  ); func "x" :::"+"::: "y" ->   ($#m2_finseq_1 :::"Tuple":::) "of" "n" "," (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  ) means :: BINARITH:def 5 (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 (Set  "(" (Set  "(" "x"  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" )  ($#k2_binarith :::"'xor'"::: )  (Set  "(" "y"  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" ) ")" )  ($#k2_binarith :::"'xor'"::: )  (Set  "(" (Set  "("  ($#k4_binarith :::"carry"::: )   "(" "x" "," "y" ")"  ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" )))); end; 







:: deftheorem    defines :::"+"::: BINARITH:def 5 :  (Bool  "for" (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"zero"::: )   )   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "b4")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "n")) "," (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k7_binarith :::"+"::: )  (Set (Var "y")))) "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 "b4"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "x"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" )  ($#k2_binarith :::"'xor'"::: )  (Set  "(" (Set (Var "y"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" ) ")" )  ($#k2_binarith :::"'xor'"::: )  (Set  "(" (Set  "("  ($#k4_binarith :::"carry"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")"  ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" ))))  ")" ))); 
 definitionlet "n" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"zero"::: )   )   ($#m1_hidden :::"Nat":::); let "z1", "z2" be   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Const "n")) "," (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  ); func  :::"add_ovfl":::  "(" "z1" "," "z2" ")"  ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  ) equals :: BINARITH:def 6 (Set (Set  "(" (Set  "(" (Set  "(" "z1"  ($#k7_partfun1 :::"/."::: )  "n" ")" )  ($#k10_margrel1 :::"'&'"::: )  (Set  "(" "z2"  ($#k7_partfun1 :::"/."::: )  "n" ")" ) ")" )  ($#k1_binarith :::"'or'"::: )  (Set  "(" (Set  "(" "z1"  ($#k7_partfun1 :::"/."::: )  "n" ")" )  ($#k10_margrel1 :::"'&'"::: )  (Set  "(" (Set  "("  ($#k4_binarith :::"carry"::: )   "(" "z1" "," "z2" ")"  ")" )  ($#k7_partfun1 :::"/."::: )  "n" ")" ) ")" ) ")" )  ($#k1_binarith :::"'or'"::: )  (Set  "(" (Set  "(" "z2"  ($#k7_partfun1 :::"/."::: )  "n" ")" )  ($#k10_margrel1 :::"'&'"::: )  (Set  "(" (Set  "("  ($#k4_binarith :::"carry"::: )   "(" "z1" "," "z2" ")"  ")" )  ($#k7_partfun1 :::"/."::: )  "n" ")" ) ")" )); end; 







:: deftheorem    defines :::"add_ovfl"::: BINARITH:def 6 :  (Bool  "for" (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"zero"::: )   )   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "z1")) "," (Set (Var "z2")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "n")) "," (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  ) "holds"  (Bool (Set   ($#k8_binarith :::"add_ovfl"::: )   "(" (Set (Var "z1")) "," (Set (Var "z2")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "z1"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")) ")" )  ($#k10_margrel1 :::"'&'"::: )  (Set  "(" (Set (Var "z2"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")) ")" ) ")" )  ($#k1_binarith :::"'or'"::: )  (Set  "(" (Set  "(" (Set (Var "z1"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")) ")" )  ($#k10_margrel1 :::"'&'"::: )  (Set  "(" (Set  "("  ($#k4_binarith :::"carry"::: )   "(" (Set (Var "z1")) "," (Set (Var "z2")) ")"  ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")) ")" ) ")" ) ")" )  ($#k1_binarith :::"'or'"::: )  (Set  "(" (Set  "(" (Set (Var "z2"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")) ")" )  ($#k10_margrel1 :::"'&'"::: )  (Set  "(" (Set  "("  ($#k4_binarith :::"carry"::: )   "(" (Set (Var "z1")) "," (Set (Var "z2")) ")"  ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")) ")" ) ")" ))))); 
 definitionlet "n" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"zero"::: )   )   ($#m1_hidden :::"Nat":::); let "z1", "z2" be   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Const "n")) "," (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  ); pred "z1" "," "z2" :::"are_summable":::  means :: BINARITH:def 7 (Bool (Set   ($#k8_binarith :::"add_ovfl"::: )   "(" "z1" "," "z2" ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k7_margrel1 :::"FALSE"::: )  )); end; 






:: deftheorem    defines :::"are_summable"::: BINARITH:def 7 :  (Bool  "for" (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"zero"::: )   )   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "z1")) "," (Set (Var "z2")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "n")) "," (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "z1")) "," (Set (Var "z2"))  ($#r1_binarith :::"are_summable"::: )  ) "iff" (Bool (Set   ($#k8_binarith :::"add_ovfl"::: )   "(" (Set (Var "z1")) "," (Set (Var "z2")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k7_margrel1 :::"FALSE"::: )  ))  ")" ))); 
 
theorem :: BINARITH:14 (Bool  "for" (Set (Var "z1")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Num 1) "," (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  )  "holds"  (Bool  "("  (Bool (Set (Var "z1"))  ($#r1_hidden :::"="::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set  ($#k7_margrel1 :::"FALSE"::: ) ) ($#k12_finseq_1 :::"*>"::: ) )) "or" (Bool (Set (Var "z1"))  ($#r1_hidden :::"="::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set  ($#k8_margrel1 :::"TRUE"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ))  ")" )) ; 
 
theorem :: BINARITH:15 (Bool  "for" (Set (Var "z1")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Num 1) "," (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  )  "st" (Bool (Bool (Set (Var "z1"))  ($#r1_hidden :::"="::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set  ($#k7_margrel1 :::"FALSE"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ))) "holds"  (Bool (Set   ($#k6_binarith :::"Absval"::: )  (Set (Var "z1")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: BINARITH:16 (Bool  "for" (Set (Var "z1")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Num 1) "," (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  )  "st" (Bool (Bool (Set (Var "z1"))  ($#r1_hidden :::"="::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set  ($#k8_margrel1 :::"TRUE"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ))) "holds"  (Bool (Set   ($#k6_binarith :::"Absval"::: )  (Set (Var "z1")))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 definitionlet "n1", "n2" be   ($#m1_hidden :::"Nat":::); let "D" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "z1" be   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Const "n1")) "," (Set (Const "D")); let "z2" be   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Const "n2")) "," (Set (Const "D")); :: original: :::"^"::: redefine func "z1" :::"^"::: "z2" ->   ($#m2_finseq_1 :::"Tuple":::) "of" (Set "n1"  ($#k23_binop_2 :::"+"::: )  "n2") "," "D"; end; definitionlet "D" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "d" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Const "D")); :: original: :::"<*"::: redefine func :::"<*":::"d":::"*>"::: ->   ($#m2_finseq_1 :::"Tuple":::) "of" (Num 1) "," "D"; end; 
theorem :: BINARITH:17 (Bool  "for" (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"zero"::: )   )   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "z1")) "," (Set (Var "z2")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "n")) "," (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  )  (Bool  "for" (Set (Var "d1")) "," (Set (Var "d2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  )  (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  "("  ($#k4_binarith :::"carry"::: )   "(" (Set  "(" (Set (Var "z1"))  ($#k9_binarith :::"^"::: )  (Set  ($#k10_binarith :::"<*"::: ) (Set (Var "d1")) ($#k10_binarith :::"*>"::: ) ) ")" ) "," (Set  "(" (Set (Var "z2"))  ($#k9_binarith :::"^"::: )  (Set  ($#k10_binarith :::"<*"::: ) (Set (Var "d2")) ($#k10_binarith :::"*>"::: ) ) ")" ) ")"  ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_binarith :::"carry"::: )   "(" (Set (Var "z1")) "," (Set (Var "z2")) ")"  ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")))))))) ; 
 
theorem :: BINARITH:18 (Bool  "for" (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"zero"::: )   )   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "z1")) "," (Set (Var "z2")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "n")) "," (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  )  (Bool  "for" (Set (Var "d1")) "," (Set (Var "d2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  ) "holds"  (Bool (Set   ($#k8_binarith :::"add_ovfl"::: )   "(" (Set (Var "z1")) "," (Set (Var "z2")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_binarith :::"carry"::: )   "(" (Set  "(" (Set (Var "z1"))  ($#k9_binarith :::"^"::: )  (Set  ($#k10_binarith :::"<*"::: ) (Set (Var "d1")) ($#k10_binarith :::"*>"::: ) ) ")" ) "," (Set  "(" (Set (Var "z2"))  ($#k9_binarith :::"^"::: )  (Set  ($#k10_binarith :::"<*"::: ) (Set (Var "d2")) ($#k10_binarith :::"*>"::: ) ) ")" ) ")"  ")" )  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" )))))) ; 
 
theorem :: BINARITH:19 (Bool  "for" (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"zero"::: )   )   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "z1")) "," (Set (Var "z2")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "n")) "," (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  )  (Bool  "for" (Set (Var "d1")) "," (Set (Var "d2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  ) "holds"  (Bool (Set (Set  "(" (Set (Var "z1"))  ($#k9_binarith :::"^"::: )  (Set  ($#k10_binarith :::"<*"::: ) (Set (Var "d1")) ($#k10_binarith :::"*>"::: ) ) ")" )  ($#k7_binarith :::"+"::: )  (Set  "(" (Set (Var "z2"))  ($#k9_binarith :::"^"::: )  (Set  ($#k10_binarith :::"<*"::: ) (Set (Var "d2")) ($#k10_binarith :::"*>"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "z1"))  ($#k7_binarith :::"+"::: )  (Set (Var "z2")) ")" )  ($#k9_binarith :::"^"::: )  (Set  ($#k10_binarith :::"<*"::: ) (Set  "(" (Set  "(" (Set (Var "d1"))  ($#k2_binarith :::"'xor'"::: )  (Set (Var "d2")) ")" )  ($#k2_binarith :::"'xor'"::: )  (Set  "("  ($#k8_binarith :::"add_ovfl"::: )   "(" (Set (Var "z1")) "," (Set (Var "z2")) ")"  ")" ) ")" ) ($#k10_binarith :::"*>"::: ) )))))) ; 
 
theorem :: BINARITH:20 (Bool  "for" (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"zero"::: )   )   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "z")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "n")) "," (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  )  (Bool  "for" (Set (Var "d")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  ) "holds"  (Bool (Set   ($#k6_binarith :::"Absval"::: )  (Set  "(" (Set (Var "z"))  ($#k9_binarith :::"^"::: )  (Set  ($#k10_binarith :::"<*"::: ) (Set (Var "d")) ($#k10_binarith :::"*>"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k6_binarith :::"Absval"::: )  (Set (Var "z")) ")" )  ($#k2_nat_1 :::"+"::: )  (Set  "("  ($#k15_funcop_1 :::"IFEQ"::: )   "(" (Set (Var "d")) "," (Set  ($#k7_margrel1 :::"FALSE"::: ) ) "," (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  "(" (Num 2)  ($#k5_series_1 :::"to_power"::: )  (Set (Var "n")) ")" ) ")"  ")" )))))) ; 
 
theorem :: BINARITH:21 (Bool  "for" (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"zero"::: )   )   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "z1")) "," (Set (Var "z2")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "n")) "," (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  ) "holds"  (Bool (Set (Set  "("  ($#k6_binarith :::"Absval"::: )  (Set  "(" (Set (Var "z1"))  ($#k7_binarith :::"+"::: )  (Set (Var "z2")) ")" ) ")" )  ($#k2_nat_1 :::"+"::: )  (Set  "("  ($#k15_funcop_1 :::"IFEQ"::: )   "(" (Set  "("  ($#k8_binarith :::"add_ovfl"::: )   "(" (Set (Var "z1")) "," (Set (Var "z2")) ")"  ")" ) "," (Set  ($#k7_margrel1 :::"FALSE"::: ) ) "," (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  "(" (Num 2)  ($#k5_series_1 :::"to_power"::: )  (Set (Var "n")) ")" ) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k6_binarith :::"Absval"::: )  (Set (Var "z1")) ")" )  ($#k2_nat_1 :::"+"::: )  (Set  "("  ($#k6_binarith :::"Absval"::: )  (Set (Var "z2")) ")" ))))) ; 
 
theorem :: BINARITH:22 (Bool  "for" (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"zero"::: )   )   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "z1")) "," (Set (Var "z2")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "n")) "," (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  )  "st" (Bool (Bool (Set (Var "z1")) "," (Set (Var "z2"))  ($#r1_binarith :::"are_summable"::: )  )) "holds"  (Bool (Set   ($#k6_binarith :::"Absval"::: )  (Set  "(" (Set (Var "z1"))  ($#k7_binarith :::"+"::: )  (Set (Var "z2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k6_binarith :::"Absval"::: )  (Set (Var "z1")) ")" )  ($#k2_nat_1 :::"+"::: )  (Set  "("  ($#k6_binarith :::"Absval"::: )  (Set (Var "z2")) ")" ))))) ;