:: RADIX_6  semantic presentation begin  
theorem :: RADIX_6:1 (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 "m")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::">="::: )  (Num 1)) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">="::: )  (Num 2))) "holds"  (Bool (Set   ($#k8_radix_1 :::"SDDec"::: )  (Set  "("  ($#k6_radix_5 :::"Fmin"::: )   "(" (Set  "(" (Set (Var "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "n")) ")" ) "," (Set (Var "m")) "," (Set (Var "k")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k8_radix_1 :::"SDDec"::: )  (Set  "("  ($#k6_radix_5 :::"Fmin"::: )   "(" (Set (Var "m")) "," (Set (Var "m")) "," (Set (Var "k")) ")"  ")" ))))) ; 
 
theorem :: RADIX_6:2 (Bool  "for" (Set (Var "m")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::">="::: )  (Num 1)) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">="::: )  (Num 2))) "holds"  (Bool (Set   ($#k8_radix_1 :::"SDDec"::: )  (Set  "("  ($#k6_radix_5 :::"Fmin"::: )   "(" (Set (Var "m")) "," (Set (Var "m")) "," (Set (Var "k")) ")"  ")" ))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 begin  definitionlet "i", "m", "k" be   ($#m1_hidden :::"Nat":::); let "r" be   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Set (Const "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 2)) "," (Set (Set (Const "k"))  ($#k3_radix_1 :::"-SD"::: )  ); assume 
(Bool (Set (Const "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set  "(" (Set (Const "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 2) ")" )))
 ; func  :::"M0Digit":::  "(" "r" "," "i" ")"  ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set "k"  ($#k3_radix_1 :::"-SD"::: )  ) equals :: RADIX_6:def 1 (Set "r"  ($#k1_funct_1 :::"."::: )  "i") if (Bool "i"  ($#r1_xxreal_0 :::">="::: )  "m")  otherwise (Set   ($#k6_numbers :::"0"::: )  ); end; 









:: deftheorem    defines :::"M0Digit"::: RADIX_6:def 1 :  (Bool  "for" (Set (Var "i")) "," (Set (Var "m")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "r")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Set (Var "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 2)) "," (Set (Set (Var "k"))  ($#k3_radix_1 :::"-SD"::: )  )  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set  "(" (Set (Var "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 2) ")" )))) "holds"  (Bool  "("   "("  (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "m")))) "implies" (Bool (Set   ($#k1_radix_6 :::"M0Digit"::: )   "(" (Set (Var "r")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i"))))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "i"))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "m"))))) "implies" (Bool (Set   ($#k1_radix_6 :::"M0Digit"::: )   "(" (Set (Var "r")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")"   ")" ))); 
 definitionlet "m", "k" be   ($#m1_hidden :::"Nat":::); let "r" be   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Set (Const "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 2)) "," (Set (Set (Const "k"))  ($#k3_radix_1 :::"-SD"::: )  ); func  :::"M0"::: "r" ->   ($#m2_finseq_1 :::"Tuple":::) "of" (Set "m"  ($#k2_xcmplx_0 :::"+"::: )  (Num 2)) "," (Set "k"  ($#k3_radix_1 :::"-SD"::: )  ) means :: RADIX_6:def 2 (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set  "(" "m"  ($#k2_xcmplx_0 :::"+"::: )  (Num 2) ")" )))) "holds"  (Bool (Set   ($#k4_radix_1 :::"DigA"::: )   "(" it "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_radix_6 :::"M0Digit"::: )   "(" "r" "," (Set (Var "i")) ")" ))); end; 







:: deftheorem    defines :::"M0"::: RADIX_6:def 2 :  (Bool  "for" (Set (Var "m")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "r")) "," (Set (Var "b4")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Set (Var "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 2)) "," (Set (Set (Var "k"))  ($#k3_radix_1 :::"-SD"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_radix_6 :::"M0"::: )  (Set (Var "r")))) "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  "(" (Set (Var "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 2) ")" )))) "holds"  (Bool (Set   ($#k4_radix_1 :::"DigA"::: )   "(" (Set (Var "b4")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_radix_6 :::"M0Digit"::: )   "(" (Set (Var "r")) "," (Set (Var "i")) ")" )))  ")" ))); 
 definitionlet "i", "m", "k" be   ($#m1_hidden :::"Nat":::); let "r" be   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Set (Const "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 2)) "," (Set (Set (Const "k"))  ($#k3_radix_1 :::"-SD"::: )  ); assume that  
(Bool (Set (Const "k"))  ($#r1_xxreal_0 :::">="::: )  (Num 2))
 and  
(Bool (Set (Const "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set  "(" (Set (Const "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 2) ")" )))
 ; func  :::"MmaxDigit":::  "(" "r" "," "i" ")"  ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set "k"  ($#k3_radix_1 :::"-SD"::: )  ) equals :: RADIX_6:def 3 (Set "r"  ($#k1_funct_1 :::"."::: )  "i") if (Bool "i"  ($#r1_xxreal_0 :::">="::: )  "m")  otherwise (Set (Set  "("  ($#k1_radix_1 :::"Radix"::: )  "k" ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Num 1)); end; 









:: deftheorem    defines :::"MmaxDigit"::: RADIX_6:def 3 :  (Bool  "for" (Set (Var "i")) "," (Set (Var "m")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "r")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Set (Var "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 2)) "," (Set (Set (Var "k"))  ($#k3_radix_1 :::"-SD"::: )  )  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">="::: )  (Num 2)) & (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set  "(" (Set (Var "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 2) ")" )))) "holds"  (Bool  "("   "("  (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "m")))) "implies" (Bool (Set   ($#k3_radix_6 :::"MmaxDigit"::: )   "(" (Set (Var "r")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i"))))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "i"))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "m"))))) "implies" (Bool (Set   ($#k3_radix_6 :::"MmaxDigit"::: )   "(" (Set (Var "r")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_radix_1 :::"Radix"::: )  (Set (Var "k")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Num 1)))  ")"   ")" ))); 
 definitionlet "m", "k" be   ($#m1_hidden :::"Nat":::); let "r" be   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Set (Const "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 2)) "," (Set (Set (Const "k"))  ($#k3_radix_1 :::"-SD"::: )  ); func  :::"Mmax"::: "r" ->   ($#m2_finseq_1 :::"Tuple":::) "of" (Set "m"  ($#k2_xcmplx_0 :::"+"::: )  (Num 2)) "," (Set "k"  ($#k3_radix_1 :::"-SD"::: )  ) means :: RADIX_6:def 4 (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set  "(" "m"  ($#k2_xcmplx_0 :::"+"::: )  (Num 2) ")" )))) "holds"  (Bool (Set   ($#k4_radix_1 :::"DigA"::: )   "(" it "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k3_radix_6 :::"MmaxDigit"::: )   "(" "r" "," (Set (Var "i")) ")" ))); end; 







:: deftheorem    defines :::"Mmax"::: RADIX_6:def 4 :  (Bool  "for" (Set (Var "m")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "r")) "," (Set (Var "b4")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Set (Var "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 2)) "," (Set (Set (Var "k"))  ($#k3_radix_1 :::"-SD"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_radix_6 :::"Mmax"::: )  (Set (Var "r")))) "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  "(" (Set (Var "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 2) ")" )))) "holds"  (Bool (Set   ($#k4_radix_1 :::"DigA"::: )   "(" (Set (Var "b4")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k3_radix_6 :::"MmaxDigit"::: )   "(" (Set (Var "r")) "," (Set (Var "i")) ")" )))  ")" ))); 
 definitionlet "i", "m", "k" be   ($#m1_hidden :::"Nat":::); let "r" be   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Set (Const "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 2)) "," (Set (Set (Const "k"))  ($#k3_radix_1 :::"-SD"::: )  ); assume that  
(Bool (Set (Const "k"))  ($#r1_xxreal_0 :::">="::: )  (Num 2))
 and  
(Bool (Set (Const "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set  "(" (Set (Const "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 2) ")" )))
 ; func  :::"MminDigit":::  "(" "r" "," "i" ")"  ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set "k"  ($#k3_radix_1 :::"-SD"::: )  ) equals :: RADIX_6:def 5 (Set "r"  ($#k1_funct_1 :::"."::: )  "i") if (Bool "i"  ($#r1_xxreal_0 :::">="::: )  "m")  otherwise (Set (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set  "("  ($#k1_radix_1 :::"Radix"::: )  "k" ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Num 1)); end; 









:: deftheorem    defines :::"MminDigit"::: RADIX_6:def 5 :  (Bool  "for" (Set (Var "i")) "," (Set (Var "m")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "r")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Set (Var "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 2)) "," (Set (Set (Var "k"))  ($#k3_radix_1 :::"-SD"::: )  )  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">="::: )  (Num 2)) & (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set  "(" (Set (Var "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 2) ")" )))) "holds"  (Bool  "("   "("  (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "m")))) "implies" (Bool (Set   ($#k5_radix_6 :::"MminDigit"::: )   "(" (Set (Var "r")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i"))))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "i"))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "m"))))) "implies" (Bool (Set   ($#k5_radix_6 :::"MminDigit"::: )   "(" (Set (Var "r")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set  "("  ($#k1_radix_1 :::"Radix"::: )  (Set (Var "k")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Num 1)))  ")"   ")" ))); 
 definitionlet "m", "k" be   ($#m1_hidden :::"Nat":::); let "r" be   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Set (Const "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 2)) "," (Set (Set (Const "k"))  ($#k3_radix_1 :::"-SD"::: )  ); func  :::"Mmin"::: "r" ->   ($#m2_finseq_1 :::"Tuple":::) "of" (Set "m"  ($#k2_xcmplx_0 :::"+"::: )  (Num 2)) "," (Set "k"  ($#k3_radix_1 :::"-SD"::: )  ) means :: RADIX_6: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"::: )  (Set  "(" "m"  ($#k2_xcmplx_0 :::"+"::: )  (Num 2) ")" )))) "holds"  (Bool (Set   ($#k4_radix_1 :::"DigA"::: )   "(" it "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k5_radix_6 :::"MminDigit"::: )   "(" "r" "," (Set (Var "i")) ")" ))); end; 







:: deftheorem    defines :::"Mmin"::: RADIX_6:def 6 :  (Bool  "for" (Set (Var "m")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "r")) "," (Set (Var "b4")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Set (Var "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 2)) "," (Set (Set (Var "k"))  ($#k3_radix_1 :::"-SD"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_radix_6 :::"Mmin"::: )  (Set (Var "r")))) "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  "(" (Set (Var "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 2) ")" )))) "holds"  (Bool (Set   ($#k4_radix_1 :::"DigA"::: )   "(" (Set (Var "b4")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k5_radix_6 :::"MminDigit"::: )   "(" (Set (Var "r")) "," (Set (Var "i")) ")" )))  ")" ))); 
 
theorem :: RADIX_6:3 (Bool  "for" (Set (Var "m")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">="::: )  (Num 2))) "holds"  (Bool  "for" (Set (Var "r")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Set (Var "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 2)) "," (Set (Set (Var "k"))  ($#k3_radix_1 :::"-SD"::: )  ) "holds"  (Bool (Set   ($#k8_radix_1 :::"SDDec"::: )  (Set  "("  ($#k4_radix_6 :::"Mmax"::: )  (Set (Var "r")) ")" ))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k8_radix_1 :::"SDDec"::: )  (Set (Var "r")))))) ; 
 
theorem :: RADIX_6:4 (Bool  "for" (Set (Var "m")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">="::: )  (Num 2))) "holds"  (Bool  "for" (Set (Var "r")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Set (Var "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 2)) "," (Set (Set (Var "k"))  ($#k3_radix_1 :::"-SD"::: )  ) "holds"  (Bool (Set   ($#k8_radix_1 :::"SDDec"::: )  (Set (Var "r")))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k8_radix_1 :::"SDDec"::: )  (Set  "("  ($#k6_radix_6 :::"Mmin"::: )  (Set (Var "r")) ")" ))))) ; 
 begin  definitionlet "n", "k" be   ($#m1_hidden :::"Nat":::); let "x" be   ($#m1_hidden :::"Integer":::); pred "x" :::"needs_digits_of"::: "n" "," "k" means :: RADIX_6:def 7 (Bool  "("  (Bool "x"  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  "("  ($#k1_radix_1 :::"Radix"::: )  "k" ")" )  ($#k1_newton :::"|^"::: )  "n")) & (Bool "x"  ($#r1_xxreal_0 :::">="::: )  (Set (Set  "("  ($#k1_radix_1 :::"Radix"::: )  "k" ")" )  ($#k13_newton :::"|^"::: )  (Set  "(" "n"  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" )))  ")" ); end; 






:: deftheorem    defines :::"needs_digits_of"::: RADIX_6:def 7 :  (Bool  "for" (Set (Var "n")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_hidden :::"Integer":::) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r1_radix_6 :::"needs_digits_of"::: )  (Set (Var "n")) "," (Set (Var "k"))) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  "("  ($#k1_radix_1 :::"Radix"::: )  (Set (Var "k")) ")" )  ($#k1_newton :::"|^"::: )  (Set (Var "n")))) & (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::">="::: )  (Set (Set  "("  ($#k1_radix_1 :::"Radix"::: )  (Set (Var "k")) ")" )  ($#k13_newton :::"|^"::: )  (Set  "(" (Set (Var "n"))  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" )))  ")" )  ")" ))); 
 
theorem :: RADIX_6:5 (Bool  "for" (Set (Var "x")) "," (Set (Var "n")) "," (Set (Var "k")) "," (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  "("  ($#k10_radix_1 :::"DecSD"::: )   "(" (Set (Var "x")) "," (Set (Var "n")) "," (Set (Var "k")) ")"  ")" ) "," (Set (Var "i")) ")" )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: RADIX_6:6 (Bool  "for" (Set (Var "n")) "," (Set (Var "k")) "," (Set (Var "x")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Num 1)) & (Bool (Set (Var "x"))  ($#r1_radix_6 :::"needs_digits_of"::: )  (Set (Var "n")) "," (Set (Var "k")))) "holds"  (Bool (Set   ($#k4_radix_1 :::"DigA"::: )   "(" (Set  "("  ($#k10_radix_1 :::"DecSD"::: )   "(" (Set (Var "x")) "," (Set (Var "n")) "," (Set (Var "k")) ")"  ")" ) "," (Set (Var "n")) ")" )  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: RADIX_6:7 (Bool  "for" (Set (Var "f")) "," (Set (Var "m")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::">="::: )  (Num 1)) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">="::: )  (Num 2)) & (Bool (Set (Var "f"))  ($#r1_radix_6 :::"needs_digits_of"::: )  (Set (Var "m")) "," (Set (Var "k")))) "holds"  (Bool (Set (Var "f"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k8_radix_1 :::"SDDec"::: )  (Set  "("  ($#k6_radix_5 :::"Fmin"::: )   "(" (Set  "(" (Set (Var "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 2) ")" ) "," (Set (Var "m")) "," (Set (Var "k")) ")"  ")" )))) ; 
 begin  
theorem :: RADIX_6:8 (Bool  "for" (Set (Var "mlow")) "," (Set (Var "mhigh")) "," (Set (Var "f")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set (Var "mhigh"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "mlow"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "f")))) & (Bool (Set (Var "f"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "ex" (Set (Var "s")) "being"   ($#m1_hidden :::"Integer":::) "st"  (Bool  "("  (Bool (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "f")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "mlow"))  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "s"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "f")) ")" ))) & (Bool (Set (Set (Var "mhigh"))  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "s"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "f")) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "f")))  ")" ))) ; 
 
theorem :: RADIX_6:9 (Bool  "for" (Set (Var "m")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">="::: )  (Num 2))) "holds"  (Bool  "for" (Set (Var "r")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Set (Var "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 2)) "," (Set (Set (Var "k"))  ($#k3_radix_1 :::"-SD"::: )  ) "holds"  (Bool (Set (Set  "("  ($#k8_radix_1 :::"SDDec"::: )  (Set  "("  ($#k4_radix_6 :::"Mmax"::: )  (Set (Var "r")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k8_radix_1 :::"SDDec"::: )  (Set  "("  ($#k10_radix_1 :::"DecSD"::: )   "(" (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  "(" (Set (Var "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 2) ")" ) "," (Set (Var "k")) ")"  ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k8_radix_1 :::"SDDec"::: )  (Set  "("  ($#k2_radix_6 :::"M0"::: )  (Set (Var "r")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k8_radix_1 :::"SDDec"::: )  (Set  "("  ($#k4_radix_5 :::"SDMax"::: )   "(" (Set  "(" (Set (Var "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 2) ")" ) "," (Set (Var "m")) "," (Set (Var "k")) ")"  ")" ) ")" ))))) ; 
 
theorem :: RADIX_6:10 (Bool  "for" (Set (Var "m")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::">="::: )  (Num 1)) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">="::: )  (Num 2))) "holds"  (Bool  "for" (Set (Var "r")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Set (Var "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 2)) "," (Set (Set (Var "k"))  ($#k3_radix_1 :::"-SD"::: )  )  "holds" (Bool (Set   ($#k8_radix_1 :::"SDDec"::: )  (Set  "("  ($#k4_radix_6 :::"Mmax"::: )  (Set (Var "r")) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  "("  ($#k8_radix_1 :::"SDDec"::: )  (Set  "("  ($#k2_radix_6 :::"M0"::: )  (Set (Var "r")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k8_radix_1 :::"SDDec"::: )  (Set  "("  ($#k6_radix_5 :::"Fmin"::: )   "(" (Set  "(" (Set (Var "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 2) ")" ) "," (Set (Var "m")) "," (Set (Var "k")) ")"  ")" ) ")" ))))) ; 
 
theorem :: RADIX_6:11 (Bool  "for" (Set (Var "m")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">="::: )  (Num 2))) "holds"  (Bool  "for" (Set (Var "r")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Set (Var "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 2)) "," (Set (Set (Var "k"))  ($#k3_radix_1 :::"-SD"::: )  ) "holds"  (Bool (Set (Set  "("  ($#k8_radix_1 :::"SDDec"::: )  (Set  "("  ($#k6_radix_6 :::"Mmin"::: )  (Set (Var "r")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k8_radix_1 :::"SDDec"::: )  (Set  "("  ($#k10_radix_1 :::"DecSD"::: )   "(" (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  "(" (Set (Var "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 2) ")" ) "," (Set (Var "k")) ")"  ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k8_radix_1 :::"SDDec"::: )  (Set  "("  ($#k2_radix_6 :::"M0"::: )  (Set (Var "r")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k8_radix_1 :::"SDDec"::: )  (Set  "("  ($#k2_radix_5 :::"SDMin"::: )   "(" (Set  "(" (Set (Var "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 2) ")" ) "," (Set (Var "m")) "," (Set (Var "k")) ")"  ")" ) ")" ))))) ; 
 
theorem :: RADIX_6:12 (Bool  "for" (Set (Var "m")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "r")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Set (Var "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 2)) "," (Set (Set (Var "k"))  ($#k3_radix_1 :::"-SD"::: )  )  "st" (Bool (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::">="::: )  (Num 1)) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">="::: )  (Num 2))) "holds"  (Bool (Set (Set  "("  ($#k8_radix_1 :::"SDDec"::: )  (Set  "("  ($#k2_radix_6 :::"M0"::: )  (Set (Var "r")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k8_radix_1 :::"SDDec"::: )  (Set  "("  ($#k10_radix_1 :::"DecSD"::: )   "(" (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  "(" (Set (Var "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 2) ")" ) "," (Set (Var "k")) ")"  ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k8_radix_1 :::"SDDec"::: )  (Set  "("  ($#k6_radix_6 :::"Mmin"::: )  (Set (Var "r")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k8_radix_1 :::"SDDec"::: )  (Set  "("  ($#k4_radix_5 :::"SDMax"::: )   "(" (Set  "(" (Set (Var "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 2) ")" ) "," (Set (Var "m")) "," (Set (Var "k")) ")"  ")" ) ")" ))))) ; 
 
theorem :: RADIX_6:13 (Bool  "for" (Set (Var "m")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::">="::: )  (Num 1)) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">="::: )  (Num 2))) "holds"  (Bool  "for" (Set (Var "r")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Set (Var "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 2)) "," (Set (Set (Var "k"))  ($#k3_radix_1 :::"-SD"::: )  )  "holds" (Bool (Set   ($#k8_radix_1 :::"SDDec"::: )  (Set  "("  ($#k2_radix_6 :::"M0"::: )  (Set (Var "r")) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  "("  ($#k8_radix_1 :::"SDDec"::: )  (Set  "("  ($#k6_radix_6 :::"Mmin"::: )  (Set (Var "r")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k8_radix_1 :::"SDDec"::: )  (Set  "("  ($#k6_radix_5 :::"Fmin"::: )   "(" (Set  "(" (Set (Var "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 2) ")" ) "," (Set (Var "m")) "," (Set (Var "k")) ")"  ")" ) ")" ))))) ; 
 
theorem :: RADIX_6:14 (Bool  "for" (Set (Var "m")) "," (Set (Var "k")) "," (Set (Var "f")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "r")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Set (Var "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 2)) "," (Set (Set (Var "k"))  ($#k3_radix_1 :::"-SD"::: )  )  "st" (Bool (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::">="::: )  (Num 1)) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">="::: )  (Num 2)) & (Bool (Set (Var "f"))  ($#r1_radix_6 :::"needs_digits_of"::: )  (Set (Var "m")) "," (Set (Var "k")))) "holds"  (Bool  "ex" (Set (Var "s")) "being"   ($#m1_hidden :::"Integer":::) "st"  (Bool  "("  (Bool (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "f")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  "("  ($#k8_radix_1 :::"SDDec"::: )  (Set  "("  ($#k2_radix_6 :::"M0"::: )  (Set (Var "r")) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "s"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "f")) ")" ))) & (Bool (Set (Set  "("  ($#k8_radix_1 :::"SDDec"::: )  (Set  "("  ($#k4_radix_6 :::"Mmax"::: )  (Set (Var "r")) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "s"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "f")) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "f")))  ")" )))) ; 
 
theorem :: RADIX_6:15 (Bool  "for" (Set (Var "m")) "," (Set (Var "k")) "," (Set (Var "f")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "r")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Set (Var "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 2)) "," (Set (Set (Var "k"))  ($#k3_radix_1 :::"-SD"::: )  )  "st" (Bool (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::">="::: )  (Num 1)) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">="::: )  (Num 2)) & (Bool (Set (Var "f"))  ($#r1_radix_6 :::"needs_digits_of"::: )  (Set (Var "m")) "," (Set (Var "k")))) "holds"  (Bool  "ex" (Set (Var "s")) "being"   ($#m1_hidden :::"Integer":::) "st"  (Bool  "("  (Bool (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "f")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  "("  ($#k8_radix_1 :::"SDDec"::: )  (Set  "("  ($#k6_radix_6 :::"Mmin"::: )  (Set (Var "r")) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "s"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "f")) ")" ))) & (Bool (Set (Set  "("  ($#k8_radix_1 :::"SDDec"::: )  (Set  "("  ($#k2_radix_6 :::"M0"::: )  (Set (Var "r")) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "s"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "f")) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "f")))  ")" )))) ; 
 
theorem :: RADIX_6:16 (Bool  "for" (Set (Var "m")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "r")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Set (Var "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 2)) "," (Set (Set (Var "k"))  ($#k3_radix_1 :::"-SD"::: )  )  "holds"  (Bool  "("   "not" (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">="::: )  (Num 2)) "or" (Bool  "("  (Bool (Set   ($#k8_radix_1 :::"SDDec"::: )  (Set  "("  ($#k2_radix_6 :::"M0"::: )  (Set (Var "r")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k8_radix_1 :::"SDDec"::: )  (Set (Var "r")))) & (Bool (Set   ($#k8_radix_1 :::"SDDec"::: )  (Set (Var "r")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k8_radix_1 :::"SDDec"::: )  (Set  "("  ($#k4_radix_6 :::"Mmax"::: )  (Set (Var "r")) ")" )))  ")" ) "or" (Bool  "("  (Bool (Set   ($#k8_radix_1 :::"SDDec"::: )  (Set  "("  ($#k6_radix_6 :::"Mmin"::: )  (Set (Var "r")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k8_radix_1 :::"SDDec"::: )  (Set (Var "r")))) & (Bool (Set   ($#k8_radix_1 :::"SDDec"::: )  (Set (Var "r")))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k8_radix_1 :::"SDDec"::: )  (Set  "("  ($#k2_radix_6 :::"M0"::: )  (Set (Var "r")) ")" )))  ")" )  ")" ))) ; 
 begin  definitionlet "i", "m", "k" be   ($#m1_hidden :::"Nat":::); let "r" be   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Set (Const "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 2)) "," (Set (Set (Const "k"))  ($#k3_radix_1 :::"-SD"::: )  ); assume 
(Bool (Set (Const "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set  "(" (Set (Const "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 2) ")" )))
 ; func  :::"MmaskDigit":::  "(" "r" "," "i" ")"  ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set "k"  ($#k3_radix_1 :::"-SD"::: )  ) equals :: RADIX_6:def 8 (Set "r"  ($#k1_funct_1 :::"."::: )  "i") if (Bool "i"  ($#r1_xxreal_0 :::"<"::: )  "m")  otherwise (Set   ($#k6_numbers :::"0"::: )  ); end; 









:: deftheorem    defines :::"MmaskDigit"::: RADIX_6:def 8 :  (Bool  "for" (Set (Var "i")) "," (Set (Var "m")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "r")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Set (Var "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 2)) "," (Set (Set (Var "k"))  ($#k3_radix_1 :::"-SD"::: )  )  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set  "(" (Set (Var "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 2) ")" )))) "holds"  (Bool  "("   "("  (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "m")))) "implies" (Bool (Set   ($#k7_radix_6 :::"MmaskDigit"::: )   "(" (Set (Var "r")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i"))))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "m"))))) "implies" (Bool (Set   ($#k7_radix_6 :::"MmaskDigit"::: )   "(" (Set (Var "r")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")"   ")" ))); 
 definitionlet "m", "k" be   ($#m1_hidden :::"Nat":::); let "r" be   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Set (Const "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 2)) "," (Set (Set (Const "k"))  ($#k3_radix_1 :::"-SD"::: )  ); func  :::"Mmask"::: "r" ->   ($#m2_finseq_1 :::"Tuple":::) "of" (Set "m"  ($#k2_xcmplx_0 :::"+"::: )  (Num 2)) "," (Set "k"  ($#k3_radix_1 :::"-SD"::: )  ) means :: RADIX_6: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"::: )  (Set  "(" "m"  ($#k2_xcmplx_0 :::"+"::: )  (Num 2) ")" )))) "holds"  (Bool (Set   ($#k4_radix_1 :::"DigA"::: )   "(" it "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k7_radix_6 :::"MmaskDigit"::: )   "(" "r" "," (Set (Var "i")) ")" ))); end; 







:: deftheorem    defines :::"Mmask"::: RADIX_6:def 9 :  (Bool  "for" (Set (Var "m")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "r")) "," (Set (Var "b4")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Set (Var "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 2)) "," (Set (Set (Var "k"))  ($#k3_radix_1 :::"-SD"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k8_radix_6 :::"Mmask"::: )  (Set (Var "r")))) "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  "(" (Set (Var "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 2) ")" )))) "holds"  (Bool (Set   ($#k4_radix_1 :::"DigA"::: )   "(" (Set (Var "b4")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k7_radix_6 :::"MmaskDigit"::: )   "(" (Set (Var "r")) "," (Set (Var "i")) ")" )))  ")" ))); 
 
theorem :: RADIX_6:17 (Bool  "for" (Set (Var "m")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "r")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Set (Var "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 2)) "," (Set (Set (Var "k"))  ($#k3_radix_1 :::"-SD"::: )  )  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">="::: )  (Num 2))) "holds"  (Bool (Set (Set  "("  ($#k8_radix_1 :::"SDDec"::: )  (Set  "("  ($#k2_radix_6 :::"M0"::: )  (Set (Var "r")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k8_radix_1 :::"SDDec"::: )  (Set  "("  ($#k8_radix_6 :::"Mmask"::: )  (Set (Var "r")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k8_radix_1 :::"SDDec"::: )  (Set (Var "r")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k8_radix_1 :::"SDDec"::: )  (Set  "("  ($#k10_radix_1 :::"DecSD"::: )   "(" (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  "(" (Set (Var "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 2) ")" ) "," (Set (Var "k")) ")"  ")" ) ")" ))))) ; 
 
theorem :: RADIX_6:18 (Bool  "for" (Set (Var "m")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "r")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Set (Var "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 2)) "," (Set (Set (Var "k"))  ($#k3_radix_1 :::"-SD"::: )  )  "st" (Bool (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::">="::: )  (Num 1)) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">="::: )  (Num 2)) & (Bool (Set   ($#k8_radix_1 :::"SDDec"::: )  (Set  "("  ($#k8_radix_6 :::"Mmask"::: )  (Set (Var "r")) ")" ))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k8_radix_1 :::"SDDec"::: )  (Set (Var "r")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k8_radix_1 :::"SDDec"::: )  (Set  "("  ($#k2_radix_6 :::"M0"::: )  (Set (Var "r")) ")" ))))) ; 
 definitionlet "i", "m", "k" be   ($#m1_hidden :::"Nat":::); assume 
(Bool (Set (Const "k"))  ($#r1_xxreal_0 :::">="::: )  (Num 2))
 ; func  :::"FSDMinDigit":::  "(" "m" "," "k" "," "i" ")"  ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set "k"  ($#k3_radix_1 :::"-SD"::: )  ) equals :: RADIX_6:def 10 (Set   ($#k6_numbers :::"0"::: )  ) if (Bool "i"  ($#r1_xxreal_0 :::">"::: )  "m") (Num 1) if (Bool "i"  ($#r1_hidden :::"="::: )  "m")  otherwise (Set (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set  "("  ($#k1_radix_1 :::"Radix"::: )  "k" ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Num 1)); end; 








:: deftheorem    defines :::"FSDMinDigit"::: RADIX_6:def 10 :  (Bool  "for" (Set (Var "i")) "," (Set (Var "m")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">="::: )  (Num 2))) "holds"  (Bool  "("   "("  (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::">"::: )  (Set (Var "m")))) "implies" (Bool (Set   ($#k9_radix_6 :::"FSDMinDigit"::: )   "(" (Set (Var "m")) "," (Set (Var "k")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")"  &  "("  (Bool (Bool (Set (Var "i"))  ($#r1_hidden :::"="::: )  (Set (Var "m")))) "implies" (Bool (Set   ($#k9_radix_6 :::"FSDMinDigit"::: )   "(" (Set (Var "m")) "," (Set (Var "k")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Num 1))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "i"))  ($#r1_xxreal_0 :::">"::: )  (Set (Var "m")))) & (Bool (Bool  "not" (Set (Var "i"))  ($#r1_hidden :::"="::: )  (Set (Var "m"))))) "implies" (Bool (Set   ($#k9_radix_6 :::"FSDMinDigit"::: )   "(" (Set (Var "m")) "," (Set (Var "k")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set  "("  ($#k1_radix_1 :::"Radix"::: )  (Set (Var "k")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Num 1)))  ")"   ")" )); 
 definitionlet "n", "m", "k" be   ($#m1_hidden :::"Nat":::); func  :::"FSDMin":::  "(" "n" "," "m" "," "k" ")"  ->   ($#m2_finseq_1 :::"Tuple":::) "of" "n" "," (Set "k"  ($#k3_radix_1 :::"-SD"::: )  ) means :: RADIX_6:def 11 (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_6 :::"FSDMinDigit"::: )   "(" "m" "," "k" "," (Set (Var "i")) ")" ))); end; 







:: deftheorem    defines :::"FSDMin"::: RADIX_6:def 11 :  (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "k")) "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_6 :::"FSDMin"::: )   "(" (Set (Var "n")) "," (Set (Var "m")) "," (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_6 :::"FSDMinDigit"::: )   "(" (Set (Var "m")) "," (Set (Var "k")) "," (Set (Var "i")) ")" )))  ")" ))); 
 
theorem :: RADIX_6:19 (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 "m")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "m"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n")))) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">="::: )  (Num 2))) "holds"  (Bool (Set   ($#k8_radix_1 :::"SDDec"::: )  (Set  "("  ($#k10_radix_6 :::"FSDMin"::: )   "(" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "k")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Num 1)))) ; 
 definitionlet "n", "m", "k" be   ($#m1_hidden :::"Nat":::); let "r" be   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Set (Const "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 2)) "," (Set (Set (Const "k"))  ($#k3_radix_1 :::"-SD"::: )  ); pred "r" :::"is_Zero_over"::: "n" means :: RADIX_6:def 12 (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::">"::: )  "n")) "holds"  (Bool (Set   ($#k4_radix_1 :::"DigA"::: )   "(" "r" "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))); end; 







:: deftheorem    defines :::"is_Zero_over"::: RADIX_6:def 12 :  (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "r")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Set (Var "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 2)) "," (Set (Set (Var "k"))  ($#k3_radix_1 :::"-SD"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "r"))  ($#r2_radix_6 :::"is_Zero_over"::: )  (Set (Var "n"))) "iff" (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::">"::: )  (Set (Var "n")))) "holds"  (Bool (Set   ($#k4_radix_1 :::"DigA"::: )   "(" (Set (Var "r")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )))  ")" ))); 
 
theorem :: RADIX_6:20 (Bool  "for" (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::">="::: )  (Num 1))) "holds"  (Bool  "for" (Set (Var "n")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "r")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Set (Var "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 2)) "," (Set (Set (Var "k"))  ($#k3_radix_1 :::"-SD"::: )  )  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">="::: )  (Num 2)) & (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set  "(" (Set (Var "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 2) ")" ))) & (Bool (Set   ($#k8_radix_6 :::"Mmask"::: )  (Set (Var "r")))  ($#r2_radix_6 :::"is_Zero_over"::: )  (Set (Var "n"))) & (Bool (Set   ($#k4_radix_1 :::"DigA"::: )   "(" (Set  "("  ($#k8_radix_6 :::"Mmask"::: )  (Set (Var "r")) ")" ) "," (Set (Var "n")) ")" )  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k8_radix_1 :::"SDDec"::: )  (Set  "("  ($#k8_radix_6 :::"Mmask"::: )  (Set (Var "r")) ")" ))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))))) ;