:: RADIX_5  semantic presentation begin  
theorem :: RADIX_5:1 (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">="::: )  (Num 2))) "holds"  (Bool (Set (Set  "("  ($#k1_radix_1 :::"Radix"::: )  (Set (Var "k")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Num 1))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "k"))  ($#k3_radix_1 :::"-SD"::: )  ))) ; 
 
theorem :: RADIX_5:2 (Bool  "for" (Set (Var "i")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::">"::: )  (Num 1)) & (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n"))))) "holds"  (Bool (Set (Set (Var "i"))  ($#k7_nat_d :::"-'"::: )  (Num 1))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n"))))) ; 
 
theorem :: RADIX_5:3 (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Num 2)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k")))) "holds"  (Bool (Num 4)  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_radix_1 :::"Radix"::: )  (Set (Var "k"))))) ; 
 
theorem :: RADIX_5:4 (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "tx")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Num 1) "," (Set (Set (Var "k"))  ($#k3_radix_1 :::"-SD"::: )  ) "holds"  (Bool (Set   ($#k8_radix_1 :::"SDDec"::: )  (Set (Var "tx")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_radix_1 :::"DigA"::: )   "(" (Set (Var "tx")) "," (Num 1) ")" )))) ; 
 begin  
theorem :: RADIX_5:5 (Bool  "for" (Set (Var "i")) "," (Set (Var "k")) "," (Set (Var "n")) "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  ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n")) "," (Set (Var "k")) ")"  ")" ) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: RADIX_5:6 (Bool  "for" (Set (Var "n")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Num 1))) "holds"  (Bool (Set   ($#k8_radix_1 :::"SDDec"::: )  (Set  "("  ($#k10_radix_1 :::"DecSD"::: )   "(" (Set  ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n")) "," (Set (Var "k")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: RADIX_5:7 (Bool  "for" (Set (Var "k")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Num 1)  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n")))) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">="::: )  (Num 2))) "holds"  (Bool (Set   ($#k4_radix_1 :::"DigA"::: )   "(" (Set  "("  ($#k10_radix_1 :::"DecSD"::: )   "(" (Num 1) "," (Set (Var "n")) "," (Set (Var "k")) ")"  ")" ) "," (Num 1) ")" )  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: RADIX_5:8 (Bool  "for" (Set (Var "i")) "," (Set (Var "k")) "," (Set (Var "n")) "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_xxreal_0 :::">"::: )  (Num 1)) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">="::: )  (Num 2))) "holds"  (Bool (Set   ($#k4_radix_1 :::"DigA"::: )   "(" (Set  "("  ($#k10_radix_1 :::"DecSD"::: )   "(" (Num 1) "," (Set (Var "n")) "," (Set (Var "k")) ")"  ")" ) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: RADIX_5:9 (Bool  "for" (Set (Var "n")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Num 1)) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">="::: )  (Num 2))) "holds"  (Bool (Set   ($#k8_radix_1 :::"SDDec"::: )  (Set  "("  ($#k10_radix_1 :::"DecSD"::: )   "(" (Num 1) "," (Set (Var "n")) "," (Set (Var "k")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: RADIX_5:10 (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">="::: )  (Num 2))) "holds"  (Bool (Set   ($#k11_radix_1 :::"SD_Add_Carry"::: )  (Set  "("  ($#k1_radix_1 :::"Radix"::: )  (Set (Var "k")) ")" ))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: RADIX_5:11 (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">="::: )  (Num 2))) "holds"  (Bool (Set   ($#k12_radix_1 :::"SD_Add_Data"::: )   "(" (Set  "("  ($#k1_radix_1 :::"Radix"::: )  (Set (Var "k")) ")" ) "," (Set (Var "k")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 begin  
theorem :: RADIX_5:12 (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")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "tx")) "," (Set (Var "ty")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "n")) "," (Set (Set (Var "k"))  ($#k3_radix_1 :::"-SD"::: )  )  "st" (Bool (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 "tx")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k4_radix_1 :::"DigA"::: )   "(" (Set (Var "ty")) "," (Set (Var "i")) ")" ))  ")" )) "holds"  (Bool (Set   ($#k8_radix_1 :::"SDDec"::: )  (Set (Var "tx")))  ($#r1_hidden :::"="::: )  (Set   ($#k8_radix_1 :::"SDDec"::: )  (Set (Var "ty"))))))) ; 
 
theorem :: RADIX_5:13 (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")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "tx")) "," (Set (Var "ty")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "n")) "," (Set (Set (Var "k"))  ($#k3_radix_1 :::"-SD"::: )  )  "st" (Bool (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 "tx")) "," (Set (Var "i")) ")" )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k4_radix_1 :::"DigA"::: )   "(" (Set (Var "ty")) "," (Set (Var "i")) ")" ))  ")" )) "holds"  (Bool (Set   ($#k8_radix_1 :::"SDDec"::: )  (Set (Var "tx")))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k8_radix_1 :::"SDDec"::: )  (Set (Var "ty"))))))) ; 
 
theorem :: RADIX_5:14 (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")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">="::: )  (Num 2))) "holds"  (Bool  "for" (Set (Var "tx")) "," (Set (Var "ty")) "," (Set (Var "tz")) "," (Set (Var "tw")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "n")) "," (Set (Set (Var "k"))  ($#k3_radix_1 :::"-SD"::: )  )  "st" (Bool (Bool  "("   "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "holds"  (Bool  "("   "not" (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n")))) "or" (Bool  "("  (Bool (Set   ($#k4_radix_1 :::"DigA"::: )   "(" (Set (Var "tx")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k4_radix_1 :::"DigA"::: )   "(" (Set (Var "tz")) "," (Set (Var "i")) ")" )) & (Bool (Set   ($#k4_radix_1 :::"DigA"::: )   "(" (Set (Var "ty")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k4_radix_1 :::"DigA"::: )   "(" (Set (Var "tw")) "," (Set (Var "i")) ")" ))  ")" ) "or" (Bool  "("  (Bool (Set   ($#k4_radix_1 :::"DigA"::: )   "(" (Set (Var "ty")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k4_radix_1 :::"DigA"::: )   "(" (Set (Var "tz")) "," (Set (Var "i")) ")" )) & (Bool (Set   ($#k4_radix_1 :::"DigA"::: )   "(" (Set (Var "tx")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k4_radix_1 :::"DigA"::: )   "(" (Set (Var "tw")) "," (Set (Var "i")) ")" ))  ")" )  ")" )  ")" )) "holds"  (Bool (Set (Set  "("  ($#k8_radix_1 :::"SDDec"::: )  (Set (Var "tz")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k8_radix_1 :::"SDDec"::: )  (Set (Var "tw")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k8_radix_1 :::"SDDec"::: )  (Set (Var "tx")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k8_radix_1 :::"SDDec"::: )  (Set (Var "ty")) ")" )))))) ; 
 
theorem :: RADIX_5:15 (Bool  "for" (Set (Var "n")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Num 1)) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">="::: )  (Num 2))) "holds"  (Bool  "for" (Set (Var "tx")) "," (Set (Var "ty")) "," (Set (Var "tz")) "being"   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "n")) "," (Set (Set (Var "k"))  ($#k3_radix_1 :::"-SD"::: )  )  "st" (Bool (Bool  "("   "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "holds"  (Bool  "("   "not" (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n")))) "or" (Bool  "("  (Bool (Set   ($#k4_radix_1 :::"DigA"::: )   "(" (Set (Var "tx")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k4_radix_1 :::"DigA"::: )   "(" (Set (Var "tz")) "," (Set (Var "i")) ")" )) & (Bool (Set   ($#k4_radix_1 :::"DigA"::: )   "(" (Set (Var "ty")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ) "or" (Bool  "("  (Bool (Set   ($#k4_radix_1 :::"DigA"::: )   "(" (Set (Var "ty")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k4_radix_1 :::"DigA"::: )   "(" (Set (Var "tz")) "," (Set (Var "i")) ")" )) & (Bool (Set   ($#k4_radix_1 :::"DigA"::: )   "(" (Set (Var "tx")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )  ")" )) "holds"  (Bool (Set (Set  "("  ($#k8_radix_1 :::"SDDec"::: )  (Set (Var "tz")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k8_radix_1 :::"SDDec"::: )  (Set  "("  ($#k10_radix_1 :::"DecSD"::: )   "(" (Set  ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n")) "," (Set (Var "k")) ")"  ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k8_radix_1 :::"SDDec"::: )  (Set (Var "tx")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k8_radix_1 :::"SDDec"::: )  (Set (Var "ty")) ")" ))))) ; 
 begin  definitionlet "i", "m", "k" be   ($#m1_hidden :::"Nat":::); assume 
(Bool (Set (Const "k"))  ($#r1_xxreal_0 :::">="::: )  (Num 2))
 ; func  :::"SDMinDigit":::  "(" "m" "," "k" "," "i" ")"  ->    ($#m2_subset_1 :::"Element"::: )   "of" (Set "k"  ($#k3_radix_1 :::"-SD"::: )  ) equals :: RADIX_5:def 1 (Set (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set  "("  ($#k1_radix_1 :::"Radix"::: )  "k" ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Num 1)) if (Bool  "("  (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  "i") & (Bool "i"  ($#r1_xxreal_0 :::"<"::: )  "m")  ")" )  otherwise (Set   ($#k6_numbers :::"0"::: )  ); end; 








:: deftheorem    defines :::"SDMinDigit"::: RADIX_5:def 1 :  (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 (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "m")))) "implies" (Bool (Set   ($#k1_radix_5 :::"SDMinDigit"::: )   "(" (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)))  ")"  &  "("  (Bool (Bool  "("   "not" (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) "or"  "not" (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "m")))  ")" )) "implies" (Bool (Set   ($#k1_radix_5 :::"SDMinDigit"::: )   "(" (Set (Var "m")) "," (Set (Var "k")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")"   ")" )); 
 definitionlet "n", "m", "k" be   ($#m1_hidden :::"Nat":::); func  :::"SDMin":::  "(" "n" "," "m" "," "k" ")"  ->   ($#m2_finseq_1 :::"Tuple":::) "of" "n" "," (Set "k"  ($#k3_radix_1 :::"-SD"::: )  ) means :: RADIX_5: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"::: )  "n"))) "holds"  (Bool (Set   ($#k4_radix_1 :::"DigA"::: )   "(" it "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_radix_5 :::"SDMinDigit"::: )   "(" "m" "," "k" "," (Set (Var "i")) ")" ))); end; 







:: deftheorem    defines :::"SDMin"::: RADIX_5:def 2 :  (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   ($#k2_radix_5 :::"SDMin"::: )   "(" (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   ($#k1_radix_5 :::"SDMinDigit"::: )   "(" (Set (Var "m")) "," (Set (Var "k")) "," (Set (Var "i")) ")" )))  ")" ))); 
 definitionlet "i", "m", "k" be   ($#m1_hidden :::"Nat":::); assume 
(Bool (Set (Const "k"))  ($#r1_xxreal_0 :::">="::: )  (Num 2))
 ; func  :::"SDMaxDigit":::  "(" "m" "," "k" "," "i" ")"  ->    ($#m2_subset_1 :::"Element"::: )   "of" (Set "k"  ($#k3_radix_1 :::"-SD"::: )  ) equals :: RADIX_5:def 3 (Set (Set  "("  ($#k1_radix_1 :::"Radix"::: )  "k" ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Num 1)) if (Bool  "("  (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  "i") & (Bool "i"  ($#r1_xxreal_0 :::"<"::: )  "m")  ")" )  otherwise (Set   ($#k6_numbers :::"0"::: )  ); end; 








:: deftheorem    defines :::"SDMaxDigit"::: RADIX_5:def 3 :  (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 (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "m")))) "implies" (Bool (Set   ($#k3_radix_5 :::"SDMaxDigit"::: )   "(" (Set (Var "m")) "," (Set (Var "k")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_radix_1 :::"Radix"::: )  (Set (Var "k")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Num 1)))  ")"  &  "("  (Bool (Bool  "("   "not" (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) "or"  "not" (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "m")))  ")" )) "implies" (Bool (Set   ($#k3_radix_5 :::"SDMaxDigit"::: )   "(" (Set (Var "m")) "," (Set (Var "k")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")"   ")" )); 
 definitionlet "n", "m", "k" be   ($#m1_hidden :::"Nat":::); func  :::"SDMax":::  "(" "n" "," "m" "," "k" ")"  ->   ($#m2_finseq_1 :::"Tuple":::) "of" "n" "," (Set "k"  ($#k3_radix_1 :::"-SD"::: )  ) means :: RADIX_5: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"::: )  "n"))) "holds"  (Bool (Set   ($#k4_radix_1 :::"DigA"::: )   "(" it "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k3_radix_5 :::"SDMaxDigit"::: )   "(" "m" "," "k" "," (Set (Var "i")) ")" ))); end; 







:: deftheorem    defines :::"SDMax"::: RADIX_5:def 4 :  (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   ($#k4_radix_5 :::"SDMax"::: )   "(" (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   ($#k3_radix_5 :::"SDMaxDigit"::: )   "(" (Set (Var "m")) "," (Set (Var "k")) "," (Set (Var "i")) ")" )))  ")" ))); 
 definitionlet "i", "m", "k" be   ($#m1_hidden :::"Nat":::); assume 
(Bool (Set (Const "k"))  ($#r1_xxreal_0 :::">="::: )  (Num 2))
 ; func  :::"FminDigit":::  "(" "m" "," "k" "," "i" ")"  ->    ($#m2_subset_1 :::"Element"::: )   "of" (Set "k"  ($#k3_radix_1 :::"-SD"::: )  ) equals :: RADIX_5:def 5 (Num 1) if (Bool "i"  ($#r1_hidden :::"="::: )  "m")  otherwise (Set   ($#k6_numbers :::"0"::: )  ); end; 








:: deftheorem    defines :::"FminDigit"::: RADIX_5:def 5 :  (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_hidden :::"="::: )  (Set (Var "m")))) "implies" (Bool (Set   ($#k5_radix_5 :::"FminDigit"::: )   "(" (Set (Var "m")) "," (Set (Var "k")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Num 1))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "i"))  ($#r1_hidden :::"="::: )  (Set (Var "m"))))) "implies" (Bool (Set   ($#k5_radix_5 :::"FminDigit"::: )   "(" (Set (Var "m")) "," (Set (Var "k")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")"   ")" )); 
 definitionlet "n", "m", "k" be   ($#m1_hidden :::"Nat":::); func  :::"Fmin":::  "(" "n" "," "m" "," "k" ")"  ->   ($#m2_finseq_1 :::"Tuple":::) "of" "n" "," (Set "k"  ($#k3_radix_1 :::"-SD"::: )  ) means :: RADIX_5: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   ($#k4_radix_1 :::"DigA"::: )   "(" it "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k5_radix_5 :::"FminDigit"::: )   "(" "m" "," "k" "," (Set (Var "i")) ")" ))); end; 







:: deftheorem    defines :::"Fmin"::: RADIX_5:def 6 :  (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   ($#k6_radix_5 :::"Fmin"::: )   "(" (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   ($#k5_radix_5 :::"FminDigit"::: )   "(" (Set (Var "m")) "," (Set (Var "k")) "," (Set (Var "i")) ")" )))  ")" ))); 
 definitionlet "i", "m", "k" be   ($#m1_hidden :::"Nat":::); assume 
(Bool (Set (Const "k"))  ($#r1_xxreal_0 :::">="::: )  (Num 2))
 ; func  :::"FmaxDigit":::  "(" "m" "," "k" "," "i" ")"  ->    ($#m2_subset_1 :::"Element"::: )   "of" (Set "k"  ($#k3_radix_1 :::"-SD"::: )  ) equals :: RADIX_5:def 7 (Set (Set  "("  ($#k1_radix_1 :::"Radix"::: )  "k" ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Num 1)) if (Bool "i"  ($#r1_hidden :::"="::: )  "m")  otherwise (Set   ($#k6_numbers :::"0"::: )  ); end; 








:: deftheorem    defines :::"FmaxDigit"::: RADIX_5:def 7 :  (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_hidden :::"="::: )  (Set (Var "m")))) "implies" (Bool (Set   ($#k7_radix_5 :::"FmaxDigit"::: )   "(" (Set (Var "m")) "," (Set (Var "k")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_radix_1 :::"Radix"::: )  (Set (Var "k")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Num 1)))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "i"))  ($#r1_hidden :::"="::: )  (Set (Var "m"))))) "implies" (Bool (Set   ($#k7_radix_5 :::"FmaxDigit"::: )   "(" (Set (Var "m")) "," (Set (Var "k")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")"   ")" )); 
 definitionlet "n", "m", "k" be   ($#m1_hidden :::"Nat":::); func  :::"Fmax":::  "(" "n" "," "m" "," "k" ")"  ->   ($#m2_finseq_1 :::"Tuple":::) "of" "n" "," (Set "k"  ($#k3_radix_1 :::"-SD"::: )  ) means :: RADIX_5:def 8 (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   ($#k7_radix_5 :::"FmaxDigit"::: )   "(" "m" "," "k" "," (Set (Var "i")) ")" ))); end; 







:: deftheorem    defines :::"Fmax"::: RADIX_5:def 8 :  (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   ($#k8_radix_5 :::"Fmax"::: )   "(" (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   ($#k7_radix_5 :::"FmaxDigit"::: )   "(" (Set (Var "m")) "," (Set (Var "k")) "," (Set (Var "i")) ")" )))  ")" ))); 
 begin  
theorem :: RADIX_5:16 (Bool  "for" (Set (Var "n")) "," (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 "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n"))))) "holds"  (Bool (Set (Set  "("  ($#k4_radix_1 :::"DigA"::: )   "(" (Set  "("  ($#k4_radix_5 :::"SDMax"::: )   "(" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "k")) ")"  ")" ) "," (Set (Var "i")) ")"  ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k4_radix_1 :::"DigA"::: )   "(" (Set  "("  ($#k2_radix_5 :::"SDMin"::: )   "(" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "k")) ")"  ")" ) "," (Set (Var "i")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )))) ; 
 
theorem :: RADIX_5:17 (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 "k"))  ($#r1_xxreal_0 :::">="::: )  (Num 2))) "holds"  (Bool (Set (Set  "("  ($#k8_radix_1 :::"SDDec"::: )  (Set  "("  ($#k4_radix_5 :::"SDMax"::: )   "(" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "k")) ")"  ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k8_radix_1 :::"SDDec"::: )  (Set  "("  ($#k2_radix_5 :::"SDMin"::: )   "(" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "k")) ")"  ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k8_radix_1 :::"SDDec"::: )  (Set  "("  ($#k10_radix_1 :::"DecSD"::: )   "(" (Set  ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n")) "," (Set (Var "k")) ")"  ")" ))))) ; 
 
theorem :: RADIX_5:18 (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  "("  ($#k6_radix_5 :::"Fmin"::: )   "(" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "k")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k8_radix_1 :::"SDDec"::: )  (Set  "("  ($#k4_radix_5 :::"SDMax"::: )   "(" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "k")) ")"  ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k8_radix_1 :::"SDDec"::: )  (Set  "("  ($#k10_radix_1 :::"DecSD"::: )   "(" (Num 1) "," (Set (Var "n")) "," (Set (Var "k")) ")"  ")" ) ")" ))))) ; 
 
theorem :: RADIX_5:19 (Bool  "for" (Set (Var "n")) "," (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  "("  ($#k6_radix_5 :::"Fmin"::: )   "(" (Set  "(" (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ) "," (Set  "(" (Set (Var "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ) "," (Set (Var "k")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k8_radix_1 :::"SDDec"::: )  (Set  "("  ($#k6_radix_5 :::"Fmin"::: )   "(" (Set  "(" (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ) "," (Set (Var "m")) "," (Set (Var "k")) ")"  ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k8_radix_1 :::"SDDec"::: )  (Set  "("  ($#k8_radix_5 :::"Fmax"::: )   "(" (Set  "(" (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ) "," (Set (Var "m")) "," (Set (Var "k")) ")"  ")" ) ")" )))) ;