:: BINARI_2  semantic presentation begin  















definitionlet "n" be   ($#m1_hidden :::"Nat":::); func  :::"Bin1"::: "n" ->   ($#m2_finseq_1 :::"Tuple":::) "of" "n" "," (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  ) means :: BINARI_2: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 (Var "i")) "," (Num 1) "," (Set  ($#k8_margrel1 :::"TRUE"::: ) ) "," (Set  ($#k7_margrel1 :::"FALSE"::: ) ) ")" ))); end; 





:: deftheorem    defines :::"Bin1"::: BINARI_2:def 1 :  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "n")) "," (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_binari_2 :::"Bin1"::: )  (Set (Var "n")))) "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 "b2"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set   ($#k15_funcop_1 :::"IFEQ"::: )   "(" (Set (Var "i")) "," (Num 1) "," (Set  ($#k8_margrel1 :::"TRUE"::: ) ) "," (Set  ($#k7_margrel1 :::"FALSE"::: ) ) ")" )))  ")" ))); 
 definitionlet "n" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"Nat":::); let "x" be   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Const "n")) "," (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  ); func  :::"Neg2"::: "x" ->   ($#m2_finseq_1 :::"Tuple":::) "of" "n" "," (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  ) equals :: BINARI_2:def 2 (Set (Set  "("  ($#k3_binarith :::"'not'"::: )  "x" ")" )  ($#k7_binarith :::"+"::: )  (Set  "("  ($#k1_binari_2 :::"Bin1"::: )  "n" ")" )); end; 






:: deftheorem    defines :::"Neg2"::: BINARI_2:def 2 :  (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   ($#k2_binari_2 :::"Neg2"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_binarith :::"'not'"::: )  (Set (Var "x")) ")" )  ($#k7_binarith :::"+"::: )  (Set  "("  ($#k1_binari_2 :::"Bin1"::: )  (Set (Var "n")) ")" ))))); 
 definitionlet "n" be   ($#m1_hidden :::"Nat":::); let "x" be   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Const "n")) "," (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  ); func  :::"Intval"::: "x" ->   ($#m1_hidden :::"Integer":::) equals :: BINARI_2:def 3 (Set   ($#k6_binarith :::"Absval"::: )  "x") if (Bool (Set "x"  ($#k7_partfun1 :::"/."::: )  "n")  ($#r1_hidden :::"="::: )  (Set   ($#k7_margrel1 :::"FALSE"::: )  ))  otherwise (Set (Set  "("  ($#k6_binarith :::"Absval"::: )  "x" ")" )  ($#k21_binop_2 :::"-"::: )  (Set  "(" (Num 2)  ($#k5_series_1 :::"to_power"::: )  "n" ")" )); end; 






:: deftheorem    defines :::"Intval"::: BINARI_2: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"::: )  ) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Set (Var "x"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k7_margrel1 :::"FALSE"::: )  ))) "implies" (Bool (Set   ($#k3_binari_2 :::"Intval"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_binarith :::"Absval"::: )  (Set (Var "x"))))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Set (Var "x"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k7_margrel1 :::"FALSE"::: )  )))) "implies" (Bool (Set   ($#k3_binari_2 :::"Intval"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k6_binarith :::"Absval"::: )  (Set (Var "x")) ")" )  ($#k21_binop_2 :::"-"::: )  (Set  "(" (Num 2)  ($#k5_series_1 :::"to_power"::: )  (Set (Var "n")) ")" )))  ")"   ")" ))); 
 definitionlet "n" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"Nat":::); let "z1", "z2" be   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Const "n")) "," (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  ); func  :::"Int_add_ovfl":::  "(" "z1" "," "z2" ")"  ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  ) equals :: BINARI_2:def 4 (Set (Set  "(" (Set  "("  ($#k9_margrel1 :::"'not'"::: )  (Set  "(" "z1"  ($#k7_partfun1 :::"/."::: )  "n" ")" ) ")" )  ($#k10_margrel1 :::"'&'"::: )  (Set  "("  ($#k9_margrel1 :::"'not'"::: )  (Set  "(" "z2"  ($#k7_partfun1 :::"/."::: )  "n" ")" ) ")" ) ")" )  ($#k10_margrel1 :::"'&'"::: )  (Set  "(" (Set  "("  ($#k4_binarith :::"carry"::: )   "(" "z1" "," "z2" ")"  ")" )  ($#k7_partfun1 :::"/."::: )  "n" ")" )); end; 







:: deftheorem    defines :::"Int_add_ovfl"::: BINARI_2:def 4 :  (Bool  "for" (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#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   ($#k4_binari_2 :::"Int_add_ovfl"::: )   "(" (Set (Var "z1")) "," (Set (Var "z2")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k9_margrel1 :::"'not'"::: )  (Set  "(" (Set (Var "z1"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")) ")" ) ")" )  ($#k10_margrel1 :::"'&'"::: )  (Set  "("  ($#k9_margrel1 :::"'not'"::: )  (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 :::"empty"::: )   )   ($#m1_hidden :::"Nat":::); let "z1", "z2" be   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Const "n")) "," (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  ); func  :::"Int_add_udfl":::  "(" "z1" "," "z2" ")"  ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  ) equals :: BINARI_2:def 5 (Set (Set  "(" (Set  "(" "z1"  ($#k7_partfun1 :::"/."::: )  "n" ")" )  ($#k10_margrel1 :::"'&'"::: )  (Set  "(" "z2"  ($#k7_partfun1 :::"/."::: )  "n" ")" ) ")" )  ($#k10_margrel1 :::"'&'"::: )  (Set  "("  ($#k9_margrel1 :::"'not'"::: )  (Set  "(" (Set  "("  ($#k4_binarith :::"carry"::: )   "(" "z1" "," "z2" ")"  ")" )  ($#k7_partfun1 :::"/."::: )  "n" ")" ) ")" )); end; 







:: deftheorem    defines :::"Int_add_udfl"::: BINARI_2:def 5 :  (Bool  "for" (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#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   ($#k5_binari_2 :::"Int_add_udfl"::: )   "(" (Set (Var "z1")) "," (Set (Var "z2")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "z1"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")) ")" )  ($#k10_margrel1 :::"'&'"::: )  (Set  "(" (Set (Var "z2"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")) ")" ) ")" )  ($#k10_margrel1 :::"'&'"::: )  (Set  "("  ($#k9_margrel1 :::"'not'"::: )  (Set  "(" (Set  "("  ($#k4_binarith :::"carry"::: )   "(" (Set (Var "z1")) "," (Set (Var "z2")) ")"  ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")) ")" ) ")" ))))); 
 
theorem :: BINARI_2:1 (Bool  "for" (Set (Var "z1")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Num 2) "," (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  )  "st" (Bool (Bool (Set (Var "z1"))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k10_binarith :::"<*"::: ) (Set  ($#k7_margrel1 :::"FALSE"::: ) ) ($#k10_binarith :::"*>"::: ) )  ($#k9_binarith :::"^"::: )  (Set  ($#k10_binarith :::"<*"::: ) (Set  ($#k7_margrel1 :::"FALSE"::: ) ) ($#k10_binarith :::"*>"::: ) )))) "holds"  (Bool (Set   ($#k3_binari_2 :::"Intval"::: )  (Set (Var "z1")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: BINARI_2:2 (Bool  "for" (Set (Var "z1")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Num 2) "," (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  )  "st" (Bool (Bool (Set (Var "z1"))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k10_binarith :::"<*"::: ) (Set  ($#k8_margrel1 :::"TRUE"::: ) ) ($#k10_binarith :::"*>"::: ) )  ($#k9_binarith :::"^"::: )  (Set  ($#k10_binarith :::"<*"::: ) (Set  ($#k7_margrel1 :::"FALSE"::: ) ) ($#k10_binarith :::"*>"::: ) )))) "holds"  (Bool (Set   ($#k3_binari_2 :::"Intval"::: )  (Set (Var "z1")))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: BINARI_2:3 (Bool  "for" (Set (Var "z1")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Num 2) "," (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  )  "st" (Bool (Bool (Set (Var "z1"))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k10_binarith :::"<*"::: ) (Set  ($#k7_margrel1 :::"FALSE"::: ) ) ($#k10_binarith :::"*>"::: ) )  ($#k9_binarith :::"^"::: )  (Set  ($#k10_binarith :::"<*"::: ) (Set  ($#k8_margrel1 :::"TRUE"::: ) ) ($#k10_binarith :::"*>"::: ) )))) "holds"  (Bool (Set   ($#k3_binari_2 :::"Intval"::: )  (Set (Var "z1")))  ($#r1_hidden :::"="::: )  (Set   ($#k19_binop_2 :::"-"::: )  (Num 2)))) ; 
 
theorem :: BINARI_2:4 (Bool  "for" (Set (Var "z1")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Num 2) "," (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  )  "st" (Bool (Bool (Set (Var "z1"))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k10_binarith :::"<*"::: ) (Set  ($#k8_margrel1 :::"TRUE"::: ) ) ($#k10_binarith :::"*>"::: ) )  ($#k9_binarith :::"^"::: )  (Set  ($#k10_binarith :::"<*"::: ) (Set  ($#k8_margrel1 :::"TRUE"::: ) ) ($#k10_binarith :::"*>"::: ) )))) "holds"  (Bool (Set   ($#k3_binari_2 :::"Intval"::: )  (Set (Var "z1")))  ($#r1_hidden :::"="::: )  (Set   ($#k19_binop_2 :::"-"::: )  (Num 1)))) ; 
 
theorem :: BINARI_2:5 (Bool  "for" (Set (Var "n")) "," (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n")))) & (Bool (Set (Var "i"))  ($#r1_hidden :::"="::: )  (Num 1))) "holds"  (Bool (Set (Set  "("  ($#k1_binari_2 :::"Bin1"::: )  (Set (Var "n")) ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set   ($#k8_margrel1 :::"TRUE"::: )  ))) ; 
 
theorem :: BINARI_2:6 (Bool  "for" (Set (Var "n")) "," (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n")))) & (Bool (Set (Var "i"))  ($#r1_hidden :::"<>"::: )  (Num 1))) "holds"  (Bool (Set (Set  "("  ($#k1_binari_2 :::"Bin1"::: )  (Set (Var "n")) ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set   ($#k7_margrel1 :::"FALSE"::: )  ))) ; 
 
theorem :: BINARI_2:7 (Bool  "for" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k1_binari_2 :::"Bin1"::: )  (Set  "(" (Set (Var "m"))  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_binari_2 :::"Bin1"::: )  (Set (Var "m")) ")" )  ($#k9_binarith :::"^"::: )  (Set  ($#k10_binarith :::"<*"::: ) (Set  ($#k7_margrel1 :::"FALSE"::: ) ) ($#k10_binarith :::"*>"::: ) )))) ; 
 
theorem :: BINARI_2:8 (Bool  "for" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k3_binari_2 :::"Intval"::: )  (Set  "(" (Set  "("  ($#k1_binari_2 :::"Bin1"::: )  (Set (Var "m")) ")" )  ($#k9_binarith :::"^"::: )  (Set  ($#k10_binarith :::"<*"::: ) (Set  ($#k7_margrel1 :::"FALSE"::: ) ) ($#k10_binarith :::"*>"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: BINARI_2:9 (Bool  "for" (Set (Var "m")) "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 "m")) "," (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  )  (Bool  "for" (Set (Var "d")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  ) "holds"  (Bool (Set   ($#k3_binarith :::"'not'"::: )  (Set  "(" (Set (Var "z"))  ($#k9_binarith :::"^"::: )  (Set  ($#k10_binarith :::"<*"::: ) (Set (Var "d")) ($#k10_binarith :::"*>"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_binarith :::"'not'"::: )  (Set (Var "z")) ")" )  ($#k9_binarith :::"^"::: )  (Set  ($#k10_binarith :::"<*"::: ) (Set  "("  ($#k9_margrel1 :::"'not'"::: )  (Set (Var "d")) ")" ) ($#k10_binarith :::"*>"::: ) )))))) ; 
 
theorem :: BINARI_2:10 (Bool  "for" (Set (Var "m")) "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 "m")) "," (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  )  (Bool  "for" (Set (Var "d")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  ) "holds"  (Bool (Set   ($#k3_binari_2 :::"Intval"::: )  (Set  "(" (Set (Var "z"))  ($#k9_binarith :::"^"::: )  (Set  ($#k10_binarith :::"<*"::: ) (Set (Var "d")) ($#k10_binarith :::"*>"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k6_binarith :::"Absval"::: )  (Set (Var "z")) ")" )  ($#k21_binop_2 :::"-"::: )  (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 "m")) ")" ) ")"  ")" )))))) ; 
 
theorem :: BINARI_2:11 (Bool  "for" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "z1")) "," (Set (Var "z2")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "m")) "," (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  "("  ($#k3_binari_2 :::"Intval"::: )  (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 :::"*>"::: ) ) ")" ) ")" ) ")" )  ($#k20_binop_2 :::"+"::: )  (Set  "("  ($#k15_funcop_1 :::"IFEQ"::: )   "(" (Set  "("  ($#k4_binari_2 :::"Int_add_ovfl"::: )   "(" (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 :::"*>"::: ) ) ")" ) ")"  ")" ) "," (Set  ($#k7_margrel1 :::"FALSE"::: ) ) "," (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  "(" (Num 2)  ($#k5_series_1 :::"to_power"::: )  (Set  "(" (Set (Var "m"))  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" ) ")" ) ")"  ")" ) ")" )  ($#k21_binop_2 :::"-"::: )  (Set  "("  ($#k15_funcop_1 :::"IFEQ"::: )   "(" (Set  "("  ($#k5_binari_2 :::"Int_add_udfl"::: )   "(" (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 :::"*>"::: ) ) ")" ) ")"  ")" ) "," (Set  ($#k7_margrel1 :::"FALSE"::: ) ) "," (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  "(" (Num 2)  ($#k5_series_1 :::"to_power"::: )  (Set  "(" (Set (Var "m"))  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" ) ")" ) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_binari_2 :::"Intval"::: )  (Set  "(" (Set (Var "z1"))  ($#k9_binarith :::"^"::: )  (Set  ($#k10_binarith :::"<*"::: ) (Set (Var "d1")) ($#k10_binarith :::"*>"::: ) ) ")" ) ")" )  ($#k20_binop_2 :::"+"::: )  (Set  "("  ($#k3_binari_2 :::"Intval"::: )  (Set  "(" (Set (Var "z2"))  ($#k9_binarith :::"^"::: )  (Set  ($#k10_binarith :::"<*"::: ) (Set (Var "d2")) ($#k10_binarith :::"*>"::: ) ) ")" ) ")" )))))) ; 
 
theorem :: BINARI_2:12 (Bool  "for" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "z1")) "," (Set (Var "z2")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "m")) "," (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   ($#k3_binari_2 :::"Intval"::: )  (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  "(" (Set  "("  ($#k3_binari_2 :::"Intval"::: )  (Set  "(" (Set (Var "z1"))  ($#k9_binarith :::"^"::: )  (Set  ($#k10_binarith :::"<*"::: ) (Set (Var "d1")) ($#k10_binarith :::"*>"::: ) ) ")" ) ")" )  ($#k20_binop_2 :::"+"::: )  (Set  "("  ($#k3_binari_2 :::"Intval"::: )  (Set  "(" (Set (Var "z2"))  ($#k9_binarith :::"^"::: )  (Set  ($#k10_binarith :::"<*"::: ) (Set (Var "d2")) ($#k10_binarith :::"*>"::: ) ) ")" ) ")" ) ")" )  ($#k21_binop_2 :::"-"::: )  (Set  "("  ($#k15_funcop_1 :::"IFEQ"::: )   "(" (Set  "("  ($#k4_binari_2 :::"Int_add_ovfl"::: )   "(" (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 :::"*>"::: ) ) ")" ) ")"  ")" ) "," (Set  ($#k7_margrel1 :::"FALSE"::: ) ) "," (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  "(" (Num 2)  ($#k5_series_1 :::"to_power"::: )  (Set  "(" (Set (Var "m"))  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" ) ")" ) ")"  ")" ) ")" )  ($#k20_binop_2 :::"+"::: )  (Set  "("  ($#k15_funcop_1 :::"IFEQ"::: )   "(" (Set  "("  ($#k5_binari_2 :::"Int_add_udfl"::: )   "(" (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 :::"*>"::: ) ) ")" ) ")"  ")" ) "," (Set  ($#k7_margrel1 :::"FALSE"::: ) ) "," (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  "(" (Num 2)  ($#k5_series_1 :::"to_power"::: )  (Set  "(" (Set (Var "m"))  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" ) ")" ) ")"  ")" )))))) ; 
 
theorem :: BINARI_2:13 (Bool  "for" (Set (Var "m")) "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 "m")) "," (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  ) "holds"  (Bool (Set   ($#k6_binarith :::"Absval"::: )  (Set  "("  ($#k3_binarith :::"'not'"::: )  (Set (Var "x")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k19_binop_2 :::"-"::: )  (Set  "("  ($#k6_binarith :::"Absval"::: )  (Set (Var "x")) ")" ) ")" )  ($#k20_binop_2 :::"+"::: )  (Set  "(" (Num 2)  ($#k5_series_1 :::"to_power"::: )  (Set (Var "m")) ")" ) ")" )  ($#k21_binop_2 :::"-"::: )  (Num 1))))) ; 
 
theorem :: BINARI_2:14 (Bool  "for" (Set (Var "m")) "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 "m")) "," (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  )  (Bool  "for" (Set (Var "d")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  ) "holds"  (Bool (Set   ($#k2_binari_2 :::"Neg2"::: )  (Set  "(" (Set (Var "z"))  ($#k9_binarith :::"^"::: )  (Set  ($#k10_binarith :::"<*"::: ) (Set (Var "d")) ($#k10_binarith :::"*>"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_binari_2 :::"Neg2"::: )  (Set (Var "z")) ")" )  ($#k9_binarith :::"^"::: )  (Set  ($#k10_binarith :::"<*"::: ) (Set  "(" (Set  "("  ($#k9_margrel1 :::"'not'"::: )  (Set (Var "d")) ")" )  ($#k2_binarith :::"'xor'"::: )  (Set  "("  ($#k8_binarith :::"add_ovfl"::: )   "(" (Set  "("  ($#k3_binarith :::"'not'"::: )  (Set (Var "z")) ")" ) "," (Set  "("  ($#k1_binari_2 :::"Bin1"::: )  (Set (Var "m")) ")" ) ")"  ")" ) ")" ) ($#k10_binarith :::"*>"::: ) )))))) ; 
 
theorem :: BINARI_2:15 (Bool  "for" (Set (Var "m")) "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 "m")) "," (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  )  (Bool  "for" (Set (Var "d")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  ) "holds"  (Bool (Set (Set  "("  ($#k3_binari_2 :::"Intval"::: )  (Set  "("  ($#k2_binari_2 :::"Neg2"::: )  (Set  "(" (Set (Var "z"))  ($#k9_binarith :::"^"::: )  (Set  ($#k10_binarith :::"<*"::: ) (Set (Var "d")) ($#k10_binarith :::"*>"::: ) ) ")" ) ")" ) ")" )  ($#k20_binop_2 :::"+"::: )  (Set  "("  ($#k15_funcop_1 :::"IFEQ"::: )   "(" (Set  "("  ($#k4_binari_2 :::"Int_add_ovfl"::: )   "(" (Set  "("  ($#k3_binarith :::"'not'"::: )  (Set  "(" (Set (Var "z"))  ($#k9_binarith :::"^"::: )  (Set  ($#k10_binarith :::"<*"::: ) (Set (Var "d")) ($#k10_binarith :::"*>"::: ) ) ")" ) ")" ) "," (Set  "("  ($#k1_binari_2 :::"Bin1"::: )  (Set  "(" (Set (Var "m"))  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" ) ")" ) ")"  ")" ) "," (Set  ($#k7_margrel1 :::"FALSE"::: ) ) "," (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  "(" (Num 2)  ($#k5_series_1 :::"to_power"::: )  (Set  "(" (Set (Var "m"))  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" ) ")" ) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k19_binop_2 :::"-"::: )  (Set  "("  ($#k3_binari_2 :::"Intval"::: )  (Set  "(" (Set (Var "z"))  ($#k9_binarith :::"^"::: )  (Set  ($#k10_binarith :::"<*"::: ) (Set (Var "d")) ($#k10_binarith :::"*>"::: ) ) ")" ) ")" )))))) ; 
 
theorem :: BINARI_2:16 (Bool  "for" (Set (Var "m")) "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 "m")) "," (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  )  (Bool  "for" (Set (Var "d")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  ) "holds"  (Bool (Set   ($#k2_binari_2 :::"Neg2"::: )  (Set  "("  ($#k2_binari_2 :::"Neg2"::: )  (Set  "(" (Set (Var "z"))  ($#k9_binarith :::"^"::: )  (Set  ($#k10_binarith :::"<*"::: ) (Set (Var "d")) ($#k10_binarith :::"*>"::: ) ) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "z"))  ($#k9_binarith :::"^"::: )  (Set  ($#k10_binarith :::"<*"::: ) (Set (Var "d")) ($#k10_binarith :::"*>"::: ) )))))) ; 
 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 "x" :::"-"::: "y" ->   ($#m2_finseq_1 :::"Tuple":::) "of" "n" "," (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  ) means :: BINARI_2:def 6 (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  "(" (Set  "("  ($#k2_binari_2 :::"Neg2"::: )  "y" ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" ) ")" )  ($#k2_binarith :::"'xor'"::: )  (Set  "(" (Set  "("  ($#k4_binarith :::"carry"::: )   "(" "x" "," (Set  "("  ($#k2_binari_2 :::"Neg2"::: )  "y" ")" ) ")"  ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" )))); end; 







:: deftheorem    defines :::"-"::: BINARI_2:def 6 :  (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 (Set (Var "x"))  ($#k6_binari_2 :::"-"::: )  (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  "("  ($#k2_binari_2 :::"Neg2"::: )  (Set (Var "y")) ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" ) ")" )  ($#k2_binarith :::"'xor'"::: )  (Set  "(" (Set  "("  ($#k4_binarith :::"carry"::: )   "(" (Set (Var "x")) "," (Set  "("  ($#k2_binari_2 :::"Neg2"::: )  (Set (Var "y")) ")" ) ")"  ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" ))))  ")" ))); 
 
theorem :: BINARI_2:17 (Bool  "for" (Set (Var "m")) "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 "m")) "," (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  ) "holds"  (Bool (Set (Set (Var "x"))  ($#k6_binari_2 :::"-"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k7_binarith :::"+"::: )  (Set  "("  ($#k2_binari_2 :::"Neg2"::: )  (Set (Var "y")) ")" ))))) ; 
 
theorem :: BINARI_2:18 (Bool  "for" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "z1")) "," (Set (Var "z2")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "m")) "," (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 :::"*>"::: ) ) ")" )  ($#k6_binari_2 :::"-"::: )  (Set  "(" (Set (Var "z2"))  ($#k9_binarith :::"^"::: )  (Set  ($#k10_binarith :::"<*"::: ) (Set (Var "d2")) ($#k10_binarith :::"*>"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "z1"))  ($#k7_binarith :::"+"::: )  (Set  "("  ($#k2_binari_2 :::"Neg2"::: )  (Set (Var "z2")) ")" ) ")" )  ($#k9_binarith :::"^"::: )  (Set  ($#k10_binarith :::"<*"::: ) (Set  "(" (Set  "(" (Set  "(" (Set (Var "d1"))  ($#k2_binarith :::"'xor'"::: )  (Set  "("  ($#k9_margrel1 :::"'not'"::: )  (Set (Var "d2")) ")" ) ")" )  ($#k2_binarith :::"'xor'"::: )  (Set  "("  ($#k8_binarith :::"add_ovfl"::: )   "(" (Set  "("  ($#k3_binarith :::"'not'"::: )  (Set (Var "z2")) ")" ) "," (Set  "("  ($#k1_binari_2 :::"Bin1"::: )  (Set (Var "m")) ")" ) ")"  ")" ) ")" )  ($#k2_binarith :::"'xor'"::: )  (Set  "("  ($#k8_binarith :::"add_ovfl"::: )   "(" (Set (Var "z1")) "," (Set  "("  ($#k2_binari_2 :::"Neg2"::: )  (Set (Var "z2")) ")" ) ")"  ")" ) ")" ) ($#k10_binarith :::"*>"::: ) )))))) ; 
 
theorem :: BINARI_2:19 (Bool  "for" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "z1")) "," (Set (Var "z2")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "m")) "," (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  "(" (Set  "("  ($#k3_binari_2 :::"Intval"::: )  (Set  "(" (Set  "(" (Set (Var "z1"))  ($#k9_binarith :::"^"::: )  (Set  ($#k10_binarith :::"<*"::: ) (Set (Var "d1")) ($#k10_binarith :::"*>"::: ) ) ")" )  ($#k6_binari_2 :::"-"::: )  (Set  "(" (Set (Var "z2"))  ($#k9_binarith :::"^"::: )  (Set  ($#k10_binarith :::"<*"::: ) (Set (Var "d2")) ($#k10_binarith :::"*>"::: ) ) ")" ) ")" ) ")" )  ($#k20_binop_2 :::"+"::: )  (Set  "("  ($#k15_funcop_1 :::"IFEQ"::: )   "(" (Set  "("  ($#k4_binari_2 :::"Int_add_ovfl"::: )   "(" (Set  "(" (Set (Var "z1"))  ($#k9_binarith :::"^"::: )  (Set  ($#k10_binarith :::"<*"::: ) (Set (Var "d1")) ($#k10_binarith :::"*>"::: ) ) ")" ) "," (Set  "("  ($#k2_binari_2 :::"Neg2"::: )  (Set  "(" (Set (Var "z2"))  ($#k9_binarith :::"^"::: )  (Set  ($#k10_binarith :::"<*"::: ) (Set (Var "d2")) ($#k10_binarith :::"*>"::: ) ) ")" ) ")" ) ")"  ")" ) "," (Set  ($#k7_margrel1 :::"FALSE"::: ) ) "," (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  "(" (Num 2)  ($#k5_series_1 :::"to_power"::: )  (Set  "(" (Set (Var "m"))  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" ) ")" ) ")"  ")" ) ")" )  ($#k21_binop_2 :::"-"::: )  (Set  "("  ($#k15_funcop_1 :::"IFEQ"::: )   "(" (Set  "("  ($#k5_binari_2 :::"Int_add_udfl"::: )   "(" (Set  "(" (Set (Var "z1"))  ($#k9_binarith :::"^"::: )  (Set  ($#k10_binarith :::"<*"::: ) (Set (Var "d1")) ($#k10_binarith :::"*>"::: ) ) ")" ) "," (Set  "("  ($#k2_binari_2 :::"Neg2"::: )  (Set  "(" (Set (Var "z2"))  ($#k9_binarith :::"^"::: )  (Set  ($#k10_binarith :::"<*"::: ) (Set (Var "d2")) ($#k10_binarith :::"*>"::: ) ) ")" ) ")" ) ")"  ")" ) "," (Set  ($#k7_margrel1 :::"FALSE"::: ) ) "," (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  "(" (Num 2)  ($#k5_series_1 :::"to_power"::: )  (Set  "(" (Set (Var "m"))  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" ) ")" ) ")"  ")" ) ")" )  ($#k20_binop_2 :::"+"::: )  (Set  "("  ($#k15_funcop_1 :::"IFEQ"::: )   "(" (Set  "("  ($#k4_binari_2 :::"Int_add_ovfl"::: )   "(" (Set  "("  ($#k3_binarith :::"'not'"::: )  (Set  "(" (Set (Var "z2"))  ($#k9_binarith :::"^"::: )  (Set  ($#k10_binarith :::"<*"::: ) (Set (Var "d2")) ($#k10_binarith :::"*>"::: ) ) ")" ) ")" ) "," (Set  "("  ($#k1_binari_2 :::"Bin1"::: )  (Set  "(" (Set (Var "m"))  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" ) ")" ) ")"  ")" ) "," (Set  ($#k7_margrel1 :::"FALSE"::: ) ) "," (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  "(" (Num 2)  ($#k5_series_1 :::"to_power"::: )  (Set  "(" (Set (Var "m"))  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" ) ")" ) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_binari_2 :::"Intval"::: )  (Set  "(" (Set (Var "z1"))  ($#k9_binarith :::"^"::: )  (Set  ($#k10_binarith :::"<*"::: ) (Set (Var "d1")) ($#k10_binarith :::"*>"::: ) ) ")" ) ")" )  ($#k21_binop_2 :::"-"::: )  (Set  "("  ($#k3_binari_2 :::"Intval"::: )  (Set  "(" (Set (Var "z2"))  ($#k9_binarith :::"^"::: )  (Set  ($#k10_binarith :::"<*"::: ) (Set (Var "d2")) ($#k10_binarith :::"*>"::: ) ) ")" ) ")" )))))) ;