:: RADIX_1  semantic presentation begin  













theorem :: RADIX_1:1 (Bool  "for" (Set (Var "n")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Set (Var "n"))  ($#k4_nat_d :::"mod"::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "k"))  ($#k6_xcmplx_0 :::"-"::: )  (Num 1)))) "holds"  (Bool (Set (Set  "(" (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k4_nat_d :::"mod"::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: RADIX_1:2 (Bool  "for" (Set (Var "n")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Set (Var "n"))  ($#k4_nat_d :::"mod"::: )  (Set (Var "k")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "k"))  ($#k6_xcmplx_0 :::"-"::: )  (Num 1)))) "holds"  (Bool (Set (Set  "(" (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k4_nat_d :::"mod"::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "n"))  ($#k4_nat_d :::"mod"::: )  (Set (Var "k")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Num 1)))) ; 
 
theorem :: RADIX_1:3 (Bool  "for" (Set (Var "m")) "," (Set (Var "k")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "m"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set (Var "k"))  ($#k4_nat_d :::"mod"::: )  (Set  "(" (Set (Var "m"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "n")) ")" ) ")" )  ($#k4_nat_d :::"mod"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "k"))  ($#k4_nat_d :::"mod"::: )  (Set (Var "n"))))) ; 
 
theorem :: RADIX_1:4 (Bool  "for" (Set (Var "k")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "holds"  (Bool  "("   "not" (Bool (Set (Var "k"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) "or" (Bool (Set (Set  "(" (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k4_nat_d :::"mod"::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "or" (Bool (Set (Set  "(" (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k4_nat_d :::"mod"::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "n"))  ($#k4_nat_d :::"mod"::: )  (Set (Var "k")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Num 1)))  ")" )) ; 
 









theorem :: RADIX_1:5 (Bool  "for" (Set (Var "i")) "," (Set (Var "k")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "k"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set (Var "n"))  ($#k4_nat_d :::"mod"::: )  (Set  "(" (Set (Var "i"))  ($#k1_newton :::"|^"::: )  (Set (Var "k")) ")" ) ")" )  ($#k3_nat_d :::"div"::: )  (Set  "(" (Set (Var "i"))  ($#k1_newton :::"|^"::: )  (Set  "(" (Set (Var "k"))  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "i")))) ; 
 
theorem :: RADIX_1:6 canceled; 
 
theorem :: RADIX_1:7 (Bool  "for" (Set (Var "i2")) "," (Set (Var "i3")) "," (Set (Var "i1")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set (Var "i2"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "i3"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set (Var "i1"))  ($#k6_int_1 :::"mod"::: )  (Set  "(" (Set (Var "i2"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "i3")) ")" ) ")" )  ($#k6_int_1 :::"mod"::: )  (Set (Var "i3")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "i1"))  ($#k6_int_1 :::"mod"::: )  (Set (Var "i3"))))) ; 
 begin  definitionlet "n" be   ($#m1_hidden :::"Nat":::); func  :::"Radix"::: "n" ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) equals :: RADIX_1:def 1 (Set (Num 2)  ($#k3_power :::"to_power"::: )  "n"); end; 





:: deftheorem    defines :::"Radix"::: RADIX_1:def 1 :  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k1_radix_1 :::"Radix"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k3_power :::"to_power"::: )  (Set (Var "n"))))); 
 definitionlet "k" be   ($#m1_hidden :::"Nat":::); func "k" :::"-SD":::  ->    ($#m1_hidden :::"set"::: )   equals :: RADIX_1:def 2  "{"  (Set (Var "e")) where e "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k4_numbers :::"INT"::: )  ) : (Bool  "("  (Bool (Set (Var "e"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "("  ($#k1_radix_1 :::"Radix"::: )  "k" ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Num 1))) & (Bool (Set (Var "e"))  ($#r1_xxreal_0 :::">="::: )  (Set (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set  "("  ($#k1_radix_1 :::"Radix"::: )  "k" ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Num 1)))  ")" )  "}"  ; end; 





:: deftheorem    defines :::"-SD"::: RADIX_1:def 2 :  (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set (Var "k"))  ($#k2_radix_1 :::"-SD"::: )  )  ($#r1_hidden :::"="::: )   "{"  (Set (Var "e")) where e "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k4_numbers :::"INT"::: )  ) : (Bool  "("  (Bool (Set (Var "e"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "("  ($#k1_radix_1 :::"Radix"::: )  (Set (Var "k")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Num 1))) & (Bool (Set (Var "e"))  ($#r1_xxreal_0 :::">="::: )  (Set (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set  "("  ($#k1_radix_1 :::"Radix"::: )  (Set (Var "k")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Num 1)))  ")" )  "}"  )); 
 
theorem :: RADIX_1:8 (Bool  "for" (Set (Var "e")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "e"))  ($#r2_hidden :::"in"::: )  (Set (Set  ($#k6_numbers :::"0"::: ) )  ($#k2_radix_1 :::"-SD"::: )  )) "iff" (Bool (Set (Var "e"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) ; 
 
theorem :: RADIX_1:9 (Bool (Set (Set  ($#k6_numbers :::"0"::: ) )  ($#k2_radix_1 :::"-SD"::: )  )  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) )) ; 
 
theorem :: RADIX_1:10 (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set (Var "k"))  ($#k2_radix_1 :::"-SD"::: )  )  ($#r1_tarski :::"c="::: )  (Set (Set  "(" (Set (Var "k"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k2_radix_1 :::"-SD"::: )  ))) ; 
 
theorem :: RADIX_1:11 (Bool  "for" (Set (Var "e")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "e"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "k"))  ($#k2_radix_1 :::"-SD"::: )  ))) "holds"  (Bool (Set (Var "e")) "is"   ($#m1_hidden :::"Integer":::)))) ; 
 
theorem :: RADIX_1:12 (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set (Var "k"))  ($#k2_radix_1 :::"-SD"::: )  )  ($#r1_tarski :::"c="::: )  (Set   ($#k4_numbers :::"INT"::: )  ))) ; 
 
theorem :: RADIX_1:13 (Bool  "for" (Set (Var "i1")) "being"   ($#m1_hidden :::"Integer":::)  (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i1"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "k"))  ($#k2_radix_1 :::"-SD"::: )  ))) "holds"  (Bool  "("  (Bool (Set (Var "i1"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "("  ($#k1_radix_1 :::"Radix"::: )  (Set (Var "k")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Num 1))) & (Bool (Set (Var "i1"))  ($#r1_xxreal_0 :::">="::: )  (Set (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set  "("  ($#k1_radix_1 :::"Radix"::: )  (Set (Var "k")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Num 1)))  ")" ))) ; 
 
theorem :: RADIX_1:14 (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r2_hidden :::"in"::: )  (Set (Set (Var "k"))  ($#k2_radix_1 :::"-SD"::: )  ))) ; 
 registrationlet "k" be   ($#m1_hidden :::"Nat":::); 
cluster (Set "k"  ($#k2_radix_1 :::"-SD"::: )  ) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; definitionlet "k" be   ($#m1_hidden :::"Nat":::); :: original: :::"-SD"::: redefine func "k" :::"-SD":::  ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k4_numbers :::"INT"::: ) ); end; begin  



theorem :: RADIX_1:15 (Bool  "for" (Set (Var "i")) "," (Set (Var "n")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "n")) "," (Set (Set (Var "k"))  ($#k3_radix_1 :::"-SD"::: )  )  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n"))))) "holds"  (Bool (Set (Set (Var "a"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i"))) "is"    ($#m2_subset_1 :::"Element"::: )   "of" (Set (Set (Var "k"))  ($#k3_radix_1 :::"-SD"::: )  )))) ; 
 definitionlet "i", "k", "n" be   ($#m1_hidden :::"Nat":::); let "x" be   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Const "n")) "," (Set (Set (Const "k"))  ($#k3_radix_1 :::"-SD"::: )  ); func  :::"DigA":::  "(" "x" "," "i" ")"  ->   ($#m1_hidden :::"Integer":::) equals :: RADIX_1:def 3 (Set "x"  ($#k1_funct_1 :::"."::: )  "i") if (Bool "i"  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  "n")) (Set   ($#k6_numbers :::"0"::: )  ) if (Bool "i"  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) ; end; 








:: deftheorem    defines :::"DigA"::: RADIX_1:def 3 :  (Bool  "for" (Set (Var "i")) "," (Set (Var "k")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "n")) "," (Set (Set (Var "k"))  ($#k3_radix_1 :::"-SD"::: )  ) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n"))))) "implies" (Bool (Set   ($#k4_radix_1 :::"DigA"::: )   "(" (Set (Var "x")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i"))))  ")"  &  "("  (Bool (Bool (Set (Var "i"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool (Set   ($#k4_radix_1 :::"DigA"::: )   "(" (Set (Var "x")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")"   ")" ))); 
 definitionlet "i", "k", "n" be   ($#m1_hidden :::"Nat":::); let "x" be   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Const "n")) "," (Set (Set (Const "k"))  ($#k3_radix_1 :::"-SD"::: )  ); func  :::"DigB":::  "(" "x" "," "i" ")"  ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k4_numbers :::"INT"::: )  ) equals :: RADIX_1:def 4 (Set   ($#k4_radix_1 :::"DigA"::: )   "(" "x" "," "i" ")" ); end; 








:: deftheorem    defines :::"DigB"::: RADIX_1:def 4 :  (Bool  "for" (Set (Var "i")) "," (Set (Var "k")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "n")) "," (Set (Set (Var "k"))  ($#k3_radix_1 :::"-SD"::: )  ) "holds"  (Bool (Set   ($#k5_radix_1 :::"DigB"::: )   "(" (Set (Var "x")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k4_radix_1 :::"DigA"::: )   "(" (Set (Var "x")) "," (Set (Var "i")) ")" )))); 
 
theorem :: RADIX_1:16 (Bool  "for" (Set (Var "i")) "," (Set (Var "n")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "n")) "," (Set (Set (Var "k"))  ($#k3_radix_1 :::"-SD"::: )  )  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n"))))) "holds"  (Bool (Set   ($#k4_radix_1 :::"DigA"::: )   "(" (Set (Var "a")) "," (Set (Var "i")) ")" ) "is"    ($#m2_subset_1 :::"Element"::: )   "of" (Set (Set (Var "k"))  ($#k3_radix_1 :::"-SD"::: )  )))) ; 
 
theorem :: RADIX_1:17 (Bool  "for" (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Num 1) "," (Set   ($#k4_numbers :::"INT"::: )  )  "st" (Bool (Bool (Set (Set (Var "x"))  ($#k7_partfun1 :::"/."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "m")))) "holds"  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set  ($#k9_finseq_1 :::"<*"::: ) (Set (Var "m")) ($#k9_finseq_1 :::"*>"::: ) )))) ; 
 definitionlet "i", "k", "n" be   ($#m1_hidden :::"Nat":::); let "x" be   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Const "n")) "," (Set (Set (Const "k"))  ($#k3_radix_1 :::"-SD"::: )  ); func  :::"SubDigit":::  "(" "x" "," "i" "," "k" ")"  ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k4_numbers :::"INT"::: )  ) equals :: RADIX_1:def 5 (Set (Set  "(" (Set  "("  ($#k1_radix_1 :::"Radix"::: )  "k" ")" )  ($#k13_newton :::"|^"::: )  (Set  "(" "i"  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k5_radix_1 :::"DigB"::: )   "(" "x" "," "i" ")"  ")" )); end; 








:: deftheorem    defines :::"SubDigit"::: RADIX_1:def 5 :  (Bool  "for" (Set (Var "i")) "," (Set (Var "k")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "n")) "," (Set (Set (Var "k"))  ($#k3_radix_1 :::"-SD"::: )  ) "holds"  (Bool (Set   ($#k6_radix_1 :::"SubDigit"::: )   "(" (Set (Var "x")) "," (Set (Var "i")) "," (Set (Var "k")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k1_radix_1 :::"Radix"::: )  (Set (Var "k")) ")" )  ($#k13_newton :::"|^"::: )  (Set  "(" (Set (Var "i"))  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k5_radix_1 :::"DigB"::: )   "(" (Set (Var "x")) "," (Set (Var "i")) ")"  ")" ))))); 
 definitionlet "n", "k" be   ($#m1_hidden :::"Nat":::); let "x" be   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Const "n")) "," (Set (Set (Const "k"))  ($#k3_radix_1 :::"-SD"::: )  ); func  :::"DigitSD"::: "x" ->   ($#m2_finseq_1 :::"Tuple":::) "of" "n" "," (Set   ($#k4_numbers :::"INT"::: )  ) means :: RADIX_1: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   ($#k6_radix_1 :::"SubDigit"::: )   "(" "x" "," (Set (Var "i")) "," "k" ")" ))); end; 







:: deftheorem    defines :::"DigitSD"::: RADIX_1:def 6 :  (Bool  "for" (Set (Var "n")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "n")) "," (Set (Set (Var "k"))  ($#k3_radix_1 :::"-SD"::: )  )  (Bool  "for" (Set (Var "b4")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "n")) "," (Set   ($#k4_numbers :::"INT"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k7_radix_1 :::"DigitSD"::: )  (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 "b4"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_radix_1 :::"SubDigit"::: )   "(" (Set (Var "x")) "," (Set (Var "i")) "," (Set (Var "k")) ")" )))  ")" )))); 
 definitionlet "n", "k" be   ($#m1_hidden :::"Nat":::); let "x" be   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Const "n")) "," (Set (Set (Const "k"))  ($#k3_radix_1 :::"-SD"::: )  ); func  :::"SDDec"::: "x" ->   ($#m1_hidden :::"Integer":::) equals :: RADIX_1:def 7 (Set   ($#k1_gr_cy_1 :::"Sum"::: )  (Set  "("  ($#k7_radix_1 :::"DigitSD"::: )  "x" ")" )); end; 







:: deftheorem    defines :::"SDDec"::: RADIX_1:def 7 :  (Bool  "for" (Set (Var "n")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "n")) "," (Set (Set (Var "k"))  ($#k3_radix_1 :::"-SD"::: )  ) "holds"  (Bool (Set   ($#k8_radix_1 :::"SDDec"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_gr_cy_1 :::"Sum"::: )  (Set  "("  ($#k7_radix_1 :::"DigitSD"::: )  (Set (Var "x")) ")" ))))); 
 definitionlet "i", "k", "x" be   ($#m1_hidden :::"Nat":::); func  :::"DigitDC":::  "(" "x" "," "i" "," "k" ")"  ->    ($#m2_subset_1 :::"Element"::: )   "of" (Set "k"  ($#k3_radix_1 :::"-SD"::: )  ) equals :: RADIX_1:def 8 (Set (Set  "(" "x"  ($#k4_nat_d :::"mod"::: )  (Set  "(" (Set  "("  ($#k1_radix_1 :::"Radix"::: )  "k" ")" )  ($#k1_newton :::"|^"::: )  "i" ")" ) ")" )  ($#k3_nat_d :::"div"::: )  (Set  "(" (Set  "("  ($#k1_radix_1 :::"Radix"::: )  "k" ")" )  ($#k13_newton :::"|^"::: )  (Set  "(" "i"  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) ")" )); end; 







:: deftheorem    defines :::"DigitDC"::: RADIX_1:def 8 :  (Bool  "for" (Set (Var "i")) "," (Set (Var "k")) "," (Set (Var "x")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k9_radix_1 :::"DigitDC"::: )   "(" (Set (Var "x")) "," (Set (Var "i")) "," (Set (Var "k")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k4_nat_d :::"mod"::: )  (Set  "(" (Set  "("  ($#k1_radix_1 :::"Radix"::: )  (Set (Var "k")) ")" )  ($#k1_newton :::"|^"::: )  (Set (Var "i")) ")" ) ")" )  ($#k3_nat_d :::"div"::: )  (Set  "(" (Set  "("  ($#k1_radix_1 :::"Radix"::: )  (Set (Var "k")) ")" )  ($#k13_newton :::"|^"::: )  (Set  "(" (Set (Var "i"))  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) ")" )))); 
 definitionlet "k", "n", "x" be   ($#m1_hidden :::"Nat":::); func  :::"DecSD":::  "(" "x" "," "n" "," "k" ")"  ->   ($#m2_finseq_1 :::"Tuple":::) "of" "n" "," (Set "k"  ($#k3_radix_1 :::"-SD"::: )  ) means :: RADIX_1:def 9 (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   ($#k4_radix_1 :::"DigA"::: )   "(" it "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k9_radix_1 :::"DigitDC"::: )   "(" "x" "," (Set (Var "i")) "," "k" ")" ))); end; 







:: deftheorem    defines :::"DecSD"::: RADIX_1:def 9 :  (Bool  "for" (Set (Var "k")) "," (Set (Var "n")) "," (Set (Var "x")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "b4")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "n")) "," (Set (Set (Var "k"))  ($#k3_radix_1 :::"-SD"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k10_radix_1 :::"DecSD"::: )   "(" (Set (Var "x")) "," (Set (Var "n")) "," (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   ($#k4_radix_1 :::"DigA"::: )   "(" (Set (Var "b4")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k9_radix_1 :::"DigitDC"::: )   "(" (Set (Var "x")) "," (Set (Var "i")) "," (Set (Var "k")) ")" )))  ")" ))); 
 begin  definitionlet "x" be   ($#m1_hidden :::"Integer":::); func  :::"SD_Add_Carry"::: "x" ->   ($#m1_hidden :::"Integer":::) equals :: RADIX_1:def 10 (Num 1) if (Bool "x"  ($#r1_xxreal_0 :::">"::: )  (Num 2)) (Set   ($#k4_xcmplx_0 :::"-"::: )  (Num 1)) if (Bool "x"  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Num 2)))  otherwise (Set   ($#k6_numbers :::"0"::: )  ); end; 





:: deftheorem    defines :::"SD_Add_Carry"::: RADIX_1:def 10 :  (Bool  "for" (Set (Var "x")) "being"   ($#m1_hidden :::"Integer":::) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::">"::: )  (Num 2))) "implies" (Bool (Set   ($#k11_radix_1 :::"SD_Add_Carry"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Num 1))  ")"  &  "("  (Bool (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Num 2)))) "implies" (Bool (Set   ($#k11_radix_1 :::"SD_Add_Carry"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Num 1)))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "x"))  ($#r1_xxreal_0 :::">"::: )  (Num 2))) & (Bool (Bool  "not" (Set (Var "x"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Num 2))))) "implies" (Bool (Set   ($#k11_radix_1 :::"SD_Add_Carry"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")"   ")" )); 
 
theorem :: RADIX_1:18 (Bool (Set   ($#k11_radix_1 :::"SD_Add_Carry"::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) ; 
 definitionlet "x" be   ($#m1_hidden :::"Integer":::); let "k" be   ($#m1_hidden :::"Nat":::); func  :::"SD_Add_Data":::  "(" "x" "," "k" ")"  ->   ($#m1_hidden :::"Integer":::) equals :: RADIX_1:def 11 (Set "x"  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "("  ($#k11_radix_1 :::"SD_Add_Carry"::: )  "x" ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k1_radix_1 :::"Radix"::: )  "k" ")" ) ")" )); end; 






:: deftheorem    defines :::"SD_Add_Data"::: RADIX_1:def 11 :  (Bool  "for" (Set (Var "x")) "being"   ($#m1_hidden :::"Integer":::)  (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k12_radix_1 :::"SD_Add_Data"::: )   "(" (Set (Var "x")) "," (Set (Var "k")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "("  ($#k11_radix_1 :::"SD_Add_Carry"::: )  (Set (Var "x")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k1_radix_1 :::"Radix"::: )  (Set (Var "k")) ")" ) ")" ))))); 
 
theorem :: RADIX_1:19 (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k12_radix_1 :::"SD_Add_Data"::: )   "(" (Set  ($#k6_numbers :::"0"::: ) ) "," (Set (Var "k")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: RADIX_1:20 (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "being"   ($#m1_hidden :::"Integer":::)  (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">="::: )  (Num 2)) & (Bool (Set (Var "i1"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "k"))  ($#k3_radix_1 :::"-SD"::: )  )) & (Bool (Set (Var "i2"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "k"))  ($#k3_radix_1 :::"-SD"::: )  ))) "holds"  (Bool  "("  (Bool (Set (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set  "("  ($#k1_radix_1 :::"Radix"::: )  (Set (Var "k")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Num 2))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k12_radix_1 :::"SD_Add_Data"::: )   "(" (Set  "(" (Set (Var "i1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "i2")) ")" ) "," (Set (Var "k")) ")" )) & (Bool (Set   ($#k12_radix_1 :::"SD_Add_Data"::: )   "(" (Set  "(" (Set (Var "i1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "i2")) ")" ) "," (Set (Var "k")) ")" )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "("  ($#k1_radix_1 :::"Radix"::: )  (Set (Var "k")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Num 2)))  ")" ))) ; 
 begin  definitionlet "n", "x", "k" be   ($#m1_hidden :::"Nat":::); pred "x" :::"is_represented_by"::: "n" "," "k" means :: RADIX_1:def 12 (Bool "x"  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  "("  ($#k1_radix_1 :::"Radix"::: )  "k" ")" )  ($#k1_newton :::"|^"::: )  "n")); end; 






:: deftheorem    defines :::"is_represented_by"::: RADIX_1:def 12 :  (Bool  "for" (Set (Var "n")) "," (Set (Var "x")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r1_radix_1 :::"is_represented_by"::: )  (Set (Var "n")) "," (Set (Var "k"))) "iff" (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  "("  ($#k1_radix_1 :::"Radix"::: )  (Set (Var "k")) ")" )  ($#k1_newton :::"|^"::: )  (Set (Var "n"))))  ")" )); 
 
theorem :: RADIX_1:21 (Bool  "for" (Set (Var "m")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "m"))  ($#r1_radix_1 :::"is_represented_by"::: )  (Num 1) "," (Set (Var "k")))) "holds"  (Bool (Set   ($#k4_radix_1 :::"DigA"::: )   "(" (Set  "("  ($#k10_radix_1 :::"DecSD"::: )   "(" (Set (Var "m")) "," (Num 1) "," (Set (Var "k")) ")"  ")" ) "," (Num 1) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "m")))) ; 
 
theorem :: RADIX_1:22 (Bool  "for" (Set (Var "k")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Num 1))) "holds"  (Bool  "for" (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "m"))  ($#r1_radix_1 :::"is_represented_by"::: )  (Set (Var "n")) "," (Set (Var "k")))) "holds"  (Bool (Set (Var "m"))  ($#r1_hidden :::"="::: )  (Set   ($#k8_radix_1 :::"SDDec"::: )  (Set  "("  ($#k10_radix_1 :::"DecSD"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "k")) ")"  ")" ))))) ; 
 
theorem :: RADIX_1:23 (Bool  "for" (Set (Var "m")) "," (Set (Var "k")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "m"))  ($#r1_radix_1 :::"is_represented_by"::: )  (Num 1) "," (Set (Var "k"))) & (Bool (Set (Var "n"))  ($#r1_radix_1 :::"is_represented_by"::: )  (Num 1) "," (Set (Var "k")))) "holds"  (Bool (Set   ($#k11_radix_1 :::"SD_Add_Carry"::: )  (Set  "(" (Set  "("  ($#k4_radix_1 :::"DigA"::: )   "(" (Set  "("  ($#k10_radix_1 :::"DecSD"::: )   "(" (Set (Var "m")) "," (Num 1) "," (Set (Var "k")) ")"  ")" ) "," (Num 1) ")"  ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k4_radix_1 :::"DigA"::: )   "(" (Set  "("  ($#k10_radix_1 :::"DecSD"::: )   "(" (Set (Var "n")) "," (Num 1) "," (Set (Var "k")) ")"  ")" ) "," (Num 1) ")"  ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k11_radix_1 :::"SD_Add_Carry"::: )  (Set  "(" (Set (Var "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "n")) ")" )))) ; 
 
theorem :: RADIX_1:24 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "m"))  ($#r1_radix_1 :::"is_represented_by"::: )  (Set (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1)) "," (Set (Var "k")))) "holds"  (Bool (Set   ($#k4_radix_1 :::"DigA"::: )   "(" (Set  "("  ($#k10_radix_1 :::"DecSD"::: )   "(" (Set (Var "m")) "," (Set  "(" (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ) "," (Set (Var "k")) ")"  ")" ) "," (Set  "(" (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "m"))  ($#k3_nat_d :::"div"::: )  (Set  "(" (Set  "("  ($#k1_radix_1 :::"Radix"::: )  (Set (Var "k")) ")" )  ($#k1_newton :::"|^"::: )  (Set (Var "n")) ")" )))) ; 
 begin  definitionlet "k", "i", "n" be   ($#m1_hidden :::"Nat":::); let "x", "y" be   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Const "n")) "," (Set (Set (Const "k"))  ($#k3_radix_1 :::"-SD"::: )  ); assume that  
(Bool (Set (Const "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Const "n"))))
 and  
(Bool (Set (Const "k"))  ($#r1_xxreal_0 :::">="::: )  (Num 2))
 ; func  :::"Add":::  "(" "x" "," "y" "," "i" "," "k" ")"  ->    ($#m2_subset_1 :::"Element"::: )   "of" (Set "k"  ($#k3_radix_1 :::"-SD"::: )  ) equals :: RADIX_1:def 13 (Set (Set  "("  ($#k12_radix_1 :::"SD_Add_Data"::: )   "(" (Set  "(" (Set  "("  ($#k4_radix_1 :::"DigA"::: )   "(" "x" "," "i" ")"  ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k4_radix_1 :::"DigA"::: )   "(" "y" "," "i" ")"  ")" ) ")" ) "," "k" ")"  ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k11_radix_1 :::"SD_Add_Carry"::: )  (Set  "(" (Set  "("  ($#k4_radix_1 :::"DigA"::: )   "(" "x" "," (Set  "(" "i"  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) ")"  ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k4_radix_1 :::"DigA"::: )   "(" "y" "," (Set  "(" "i"  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) ")"  ")" ) ")" ) ")" )); end; 










:: deftheorem    defines :::"Add"::: RADIX_1:def 13 :  (Bool  "for" (Set (Var "k")) "," (Set (Var "i")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "n")) "," (Set (Set (Var "k"))  ($#k3_radix_1 :::"-SD"::: )  )  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n")))) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">="::: )  (Num 2))) "holds"  (Bool (Set   ($#k13_radix_1 :::"Add"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "i")) "," (Set (Var "k")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k12_radix_1 :::"SD_Add_Data"::: )   "(" (Set  "(" (Set  "("  ($#k4_radix_1 :::"DigA"::: )   "(" (Set (Var "x")) "," (Set (Var "i")) ")"  ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k4_radix_1 :::"DigA"::: )   "(" (Set (Var "y")) "," (Set (Var "i")) ")"  ")" ) ")" ) "," (Set (Var "k")) ")"  ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k11_radix_1 :::"SD_Add_Carry"::: )  (Set  "(" (Set  "("  ($#k4_radix_1 :::"DigA"::: )   "(" (Set (Var "x")) "," (Set  "(" (Set (Var "i"))  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) ")"  ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k4_radix_1 :::"DigA"::: )   "(" (Set (Var "y")) "," (Set  "(" (Set (Var "i"))  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) ")"  ")" ) ")" ) ")" ))))); 
 definitionlet "n", "k" be   ($#m1_hidden :::"Nat":::); let "x", "y" be   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Const "n")) "," (Set (Set (Const "k"))  ($#k3_radix_1 :::"-SD"::: )  ); func "x" :::"'+'"::: "y" ->   ($#m2_finseq_1 :::"Tuple":::) "of" "n" "," (Set "k"  ($#k3_radix_1 :::"-SD"::: )  ) means :: RADIX_1:def 14 (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   ($#k4_radix_1 :::"DigA"::: )   "(" it "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k13_radix_1 :::"Add"::: )   "(" "x" "," "y" "," (Set (Var "i")) "," "k" ")" ))); end; 








:: deftheorem    defines :::"'+'"::: RADIX_1:def 14 :  (Bool  "for" (Set (Var "n")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "b5")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "n")) "," (Set (Set (Var "k"))  ($#k3_radix_1 :::"-SD"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "b5"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k14_radix_1 :::"'+'"::: )  (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   ($#k4_radix_1 :::"DigA"::: )   "(" (Set (Var "b5")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k13_radix_1 :::"Add"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "i")) "," (Set (Var "k")) ")" )))  ")" ))); 
 
theorem :: RADIX_1:25 (Bool  "for" (Set (Var "k")) "," (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">="::: )  (Num 2)) & (Bool (Set (Var "m"))  ($#r1_radix_1 :::"is_represented_by"::: )  (Num 1) "," (Set (Var "k"))) & (Bool (Set (Var "n"))  ($#r1_radix_1 :::"is_represented_by"::: )  (Num 1) "," (Set (Var "k")))) "holds"  (Bool (Set   ($#k8_radix_1 :::"SDDec"::: )  (Set  "(" (Set  "("  ($#k10_radix_1 :::"DecSD"::: )   "(" (Set (Var "m")) "," (Num 1) "," (Set (Var "k")) ")"  ")" )  ($#k14_radix_1 :::"'+'"::: )  (Set  "("  ($#k10_radix_1 :::"DecSD"::: )   "(" (Set (Var "n")) "," (Num 1) "," (Set (Var "k")) ")"  ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k12_radix_1 :::"SD_Add_Data"::: )   "(" (Set  "(" (Set (Var "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "n")) ")" ) "," (Set (Var "k")) ")" ))) ; 
 
theorem :: RADIX_1:26 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Num 1))) "holds"  (Bool  "for" (Set (Var "k")) "," (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">="::: )  (Num 2)) & (Bool (Set (Var "x"))  ($#r1_radix_1 :::"is_represented_by"::: )  (Set (Var "n")) "," (Set (Var "k"))) & (Bool (Set (Var "y"))  ($#r1_radix_1 :::"is_represented_by"::: )  (Set (Var "n")) "," (Set (Var "k")))) "holds"  (Bool (Set (Set (Var "x"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k8_radix_1 :::"SDDec"::: )  (Set  "(" (Set  "("  ($#k10_radix_1 :::"DecSD"::: )   "(" (Set (Var "x")) "," (Set (Var "n")) "," (Set (Var "k")) ")"  ")" )  ($#k14_radix_1 :::"'+'"::: )  (Set  "("  ($#k10_radix_1 :::"DecSD"::: )   "(" (Set (Var "y")) "," (Set (Var "n")) "," (Set (Var "k")) ")"  ")" ) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k1_radix_1 :::"Radix"::: )  (Set (Var "k")) ")" )  ($#k1_newton :::"|^"::: )  (Set (Var "n")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k11_radix_1 :::"SD_Add_Carry"::: )  (Set  "(" (Set  "("  ($#k4_radix_1 :::"DigA"::: )   "(" (Set  "("  ($#k10_radix_1 :::"DecSD"::: )   "(" (Set (Var "x")) "," (Set (Var "n")) "," (Set (Var "k")) ")"  ")" ) "," (Set (Var "n")) ")"  ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k4_radix_1 :::"DigA"::: )   "(" (Set  "("  ($#k10_radix_1 :::"DecSD"::: )   "(" (Set (Var "y")) "," (Set (Var "n")) "," (Set (Var "k")) ")"  ")" ) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" ) ")" ))))) ;