:: RADIX_4  semantic presentation begin  











theorem :: RADIX_4:1 (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Num 2)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k")))) "holds"  (Bool (Num 2)  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k1_radix_1 :::"Radix"::: )  (Set (Var "k"))))) ; 
 begin  
theorem :: RADIX_4:2 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_hidden :::"Integer":::)  (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Num 3)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k")))) "holds"  (Bool (Set   ($#k5_radix_3 :::"SDSub_Add_Carry"::: )   "(" (Set  "(" (Set  "("  ($#k5_radix_3 :::"SDSub_Add_Carry"::: )   "(" (Set (Var "x")) "," (Set (Var "k")) ")"  ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k5_radix_3 :::"SDSub_Add_Carry"::: )   "(" (Set (Var "y")) "," (Set (Var "k")) ")"  ")" ) ")" ) "," (Set (Var "k")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )))) ; 
 
theorem :: RADIX_4:3 (Bool  "for" (Set (Var "k")) "," (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Num 2)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k")))) "holds"  (Bool (Set   ($#k7_radix_3 :::"DigA_SDSub"::: )   "(" (Set  "("  ($#k10_radix_3 :::"SD2SDSub"::: )  (Set  "("  ($#k10_radix_1 :::"DecSD"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "k")) ")"  ")" ) ")" ) "," (Set  "(" (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k5_radix_3 :::"SDSub_Add_Carry"::: )   "(" (Set  "("  ($#k4_radix_1 :::"DigA"::: )   "(" (Set  "("  ($#k10_radix_1 :::"DecSD"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "k")) ")"  ")" ) "," (Set (Var "n")) ")"  ")" ) "," (Set (Var "k")) ")" ))) ; 
 
theorem :: RADIX_4:4 (Bool  "for" (Set (Var "k")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Num 2)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k"))) & (Bool (Set (Var "m"))  ($#r1_radix_1 :::"is_represented_by"::: )  (Num 1) "," (Set (Var "k")))) "holds"  (Bool (Set   ($#k7_radix_3 :::"DigA_SDSub"::: )   "(" (Set  "("  ($#k10_radix_3 :::"SD2SDSub"::: )  (Set  "("  ($#k10_radix_1 :::"DecSD"::: )   "(" (Set (Var "m")) "," (Num 1) "," (Set (Var "k")) ")"  ")" ) ")" ) "," (Set  "(" (Num 1)  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k5_radix_3 :::"SDSub_Add_Carry"::: )   "(" (Set (Var "m")) "," (Set (Var "k")) ")" ))) ; 
 
theorem :: RADIX_4:5 (Bool  "for" (Set (Var "k")) "," (Set (Var "x")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Num 1)) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">="::: )  (Num 3)) & (Bool (Set (Var "x"))  ($#r1_radix_1 :::"is_represented_by"::: )  (Set (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1)) "," (Set (Var "k")))) "holds"  (Bool (Set   ($#k7_radix_3 :::"DigA_SDSub"::: )   "(" (Set  "("  ($#k10_radix_3 :::"SD2SDSub"::: )  (Set  "("  ($#k10_radix_1 :::"DecSD"::: )   "(" (Set  "(" (Set (Var "x"))  ($#k4_nat_d :::"mod"::: )  (Set  "(" (Set  "("  ($#k1_radix_1 :::"Radix"::: )  (Set (Var "k")) ")" )  ($#k1_newton :::"|^"::: )  (Set (Var "n")) ")" ) ")" ) "," (Set (Var "n")) "," (Set (Var "k")) ")"  ")" ) ")" ) "," (Set  "(" (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k5_radix_3 :::"SDSub_Add_Carry"::: )   "(" (Set  "("  ($#k4_radix_1 :::"DigA"::: )   "(" (Set  "("  ($#k10_radix_1 :::"DecSD"::: )   "(" (Set (Var "x")) "," (Set (Var "n")) "," (Set (Var "k")) ")"  ")" ) "," (Set (Var "n")) ")"  ")" ) "," (Set (Var "k")) ")" ))) ; 
 
theorem :: RADIX_4:6 (Bool  "for" (Set (Var "k")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Num 2)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k"))) & (Bool (Set (Var "m"))  ($#r1_radix_1 :::"is_represented_by"::: )  (Num 1) "," (Set (Var "k")))) "holds"  (Bool (Set   ($#k7_radix_3 :::"DigA_SDSub"::: )   "(" (Set  "("  ($#k10_radix_3 :::"SD2SDSub"::: )  (Set  "("  ($#k10_radix_1 :::"DecSD"::: )   "(" (Set (Var "m")) "," (Num 1) "," (Set (Var "k")) ")"  ")" ) ")" ) "," (Num 1) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "m"))  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "("  ($#k5_radix_3 :::"SDSub_Add_Carry"::: )   "(" (Set (Var "m")) "," (Set (Var "k")) ")"  ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k1_radix_1 :::"Radix"::: )  (Set (Var "k")) ")" ) ")" )))) ; 
 
theorem :: RADIX_4:7 (Bool  "for" (Set (Var "k")) "," (Set (Var "x")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">="::: )  (Num 2))) "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k1_radix_1 :::"Radix"::: )  (Set (Var "k")) ")" )  ($#k1_newton :::"|^"::: )  (Set (Var "n")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k7_radix_3 :::"DigA_SDSub"::: )   "(" (Set  "("  ($#k10_radix_3 :::"SD2SDSub"::: )  (Set  "("  ($#k10_radix_1 :::"DecSD"::: )   "(" (Set (Var "x")) "," (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  "(" (Set  "(" (Set  "(" (Set  "("  ($#k1_radix_1 :::"Radix"::: )  (Set (Var "k")) ")" )  ($#k1_newton :::"|^"::: )  (Set (Var "n")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k4_radix_1 :::"DigA"::: )   "(" (Set  "("  ($#k10_radix_1 :::"DecSD"::: )   "(" (Set (Var "x")) "," (Set  "(" (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ) "," (Set (Var "k")) ")"  ")" ) "," (Set  "(" (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ) ")"  ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k1_radix_1 :::"Radix"::: )  (Set (Var "k")) ")" )  ($#k1_newton :::"|^"::: )  (Set  "(" (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k5_radix_3 :::"SDSub_Add_Carry"::: )   "(" (Set  "("  ($#k4_radix_1 :::"DigA"::: )   "(" (Set  "("  ($#k10_radix_1 :::"DecSD"::: )   "(" (Set (Var "x")) "," (Set  "(" (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ) "," (Set (Var "k")) ")"  ")" ) "," (Set  "(" (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ) ")"  ")" ) "," (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  "("  ($#k5_radix_3 :::"SDSub_Add_Carry"::: )   "(" (Set  "("  ($#k4_radix_1 :::"DigA"::: )   "(" (Set  "("  ($#k10_radix_1 :::"DecSD"::: )   "(" (Set (Var "x")) "," (Set  "(" (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ) "," (Set (Var "k")) ")"  ")" ) "," (Set (Var "n")) ")"  ")" ) "," (Set (Var "k")) ")"  ")" ) ")" )))) ; 
 begin  definitionlet "i", "n", "k" be   ($#m1_hidden :::"Nat":::); let "x", "y" be   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Const "n")) "," (Set (Set (Const "k"))  ($#k4_radix_3 :::"-SD_Sub"::: )  ); 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  :::"SDSubAddDigit":::  "(" "x" "," "y" "," "i" "," "k" ")"  ->    ($#m2_subset_1 :::"Element"::: )   "of" (Set "k"  ($#k4_radix_3 :::"-SD_Sub"::: )  ) equals :: RADIX_4:def 1 (Set (Set  "("  ($#k6_radix_3 :::"SDSub_Add_Data"::: )   "(" (Set  "(" (Set  "("  ($#k7_radix_3 :::"DigA_SDSub"::: )   "(" "x" "," "i" ")"  ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k7_radix_3 :::"DigA_SDSub"::: )   "(" "y" "," "i" ")"  ")" ) ")" ) "," "k" ")"  ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k5_radix_3 :::"SDSub_Add_Carry"::: )   "(" (Set  "(" (Set  "("  ($#k7_radix_3 :::"DigA_SDSub"::: )   "(" "x" "," (Set  "(" "i"  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) ")"  ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k7_radix_3 :::"DigA_SDSub"::: )   "(" "y" "," (Set  "(" "i"  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) ")"  ")" ) ")" ) "," "k" ")"  ")" )); end; 










:: deftheorem    defines :::"SDSubAddDigit"::: RADIX_4:def 1 :  (Bool  "for" (Set (Var "i")) "," (Set (Var "n")) "," (Set (Var "k")) "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"))  ($#k4_radix_3 :::"-SD_Sub"::: )  )  "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   ($#k1_radix_4 :::"SDSubAddDigit"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "i")) "," (Set (Var "k")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k6_radix_3 :::"SDSub_Add_Data"::: )   "(" (Set  "(" (Set  "("  ($#k7_radix_3 :::"DigA_SDSub"::: )   "(" (Set (Var "x")) "," (Set (Var "i")) ")"  ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k7_radix_3 :::"DigA_SDSub"::: )   "(" (Set (Var "y")) "," (Set (Var "i")) ")"  ")" ) ")" ) "," (Set (Var "k")) ")"  ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k5_radix_3 :::"SDSub_Add_Carry"::: )   "(" (Set  "(" (Set  "("  ($#k7_radix_3 :::"DigA_SDSub"::: )   "(" (Set (Var "x")) "," (Set  "(" (Set (Var "i"))  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) ")"  ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k7_radix_3 :::"DigA_SDSub"::: )   "(" (Set (Var "y")) "," (Set  "(" (Set (Var "i"))  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) ")"  ")" ) ")" ) "," (Set (Var "k")) ")"  ")" ))))); 
 definitionlet "n", "k" be   ($#m1_hidden :::"Nat":::); let "x", "y" be   ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Const "n")) "," (Set (Set (Const "k"))  ($#k4_radix_3 :::"-SD_Sub"::: )  ); func "x" :::"'+'"::: "y" ->   ($#m2_finseq_1 :::"Tuple":::) "of" "n" "," (Set "k"  ($#k4_radix_3 :::"-SD_Sub"::: )  ) means :: RADIX_4: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   ($#k7_radix_3 :::"DigA_SDSub"::: )   "(" it "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_radix_4 :::"SDSubAddDigit"::: )   "(" "x" "," "y" "," (Set (Var "i")) "," "k" ")" ))); end; 








:: deftheorem    defines :::"'+'"::: RADIX_4:def 2 :  (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"))  ($#k4_radix_3 :::"-SD_Sub"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "b5"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k2_radix_4 :::"'+'"::: )  (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   ($#k7_radix_3 :::"DigA_SDSub"::: )   "(" (Set (Var "b5")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_radix_4 :::"SDSubAddDigit"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "i")) "," (Set (Var "k")) ")" )))  ")" ))); 
 
theorem :: RADIX_4:8 (Bool  "for" (Set (Var "n")) "," (Set (Var "k")) "," (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n")))) & (Bool (Num 2)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k")))) "holds"  (Bool (Set   ($#k1_radix_4 :::"SDSubAddDigit"::: )   "(" (Set  "("  ($#k10_radix_3 :::"SD2SDSub"::: )  (Set  "("  ($#k10_radix_1 :::"DecSD"::: )   "(" (Set (Var "x")) "," (Set  "(" (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ) "," (Set (Var "k")) ")"  ")" ) ")" ) "," (Set  "("  ($#k10_radix_3 :::"SD2SDSub"::: )  (Set  "("  ($#k10_radix_1 :::"DecSD"::: )   "(" (Set (Var "y")) "," (Set  "(" (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ) "," (Set (Var "k")) ")"  ")" ) ")" ) "," (Set (Var "i")) "," (Set (Var "k")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_radix_4 :::"SDSubAddDigit"::: )   "(" (Set  "("  ($#k10_radix_3 :::"SD2SDSub"::: )  (Set  "("  ($#k10_radix_1 :::"DecSD"::: )   "(" (Set  "(" (Set (Var "x"))  ($#k4_nat_d :::"mod"::: )  (Set  "(" (Set  "("  ($#k1_radix_1 :::"Radix"::: )  (Set (Var "k")) ")" )  ($#k1_newton :::"|^"::: )  (Set (Var "n")) ")" ) ")" ) "," (Set (Var "n")) "," (Set (Var "k")) ")"  ")" ) ")" ) "," (Set  "("  ($#k10_radix_3 :::"SD2SDSub"::: )  (Set  "("  ($#k10_radix_1 :::"DecSD"::: )   "(" (Set  "(" (Set (Var "y"))  ($#k4_nat_d :::"mod"::: )  (Set  "(" (Set  "("  ($#k1_radix_1 :::"Radix"::: )  (Set (Var "k")) ")" )  ($#k1_newton :::"|^"::: )  (Set (Var "n")) ")" ) ")" ) "," (Set (Var "n")) "," (Set (Var "k")) ")"  ")" ) ")" ) "," (Set (Var "i")) "," (Set (Var "k")) ")" ))) ; 
 
theorem :: RADIX_4:9 (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 3)) & (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   ($#k14_radix_3 :::"SDSub2IntOut"::: )  (Set  "(" (Set  "("  ($#k10_radix_3 :::"SD2SDSub"::: )  (Set  "("  ($#k10_radix_1 :::"DecSD"::: )   "(" (Set (Var "x")) "," (Set (Var "n")) "," (Set (Var "k")) ")"  ")" ) ")" )  ($#k2_radix_4 :::"'+'"::: )  (Set  "("  ($#k10_radix_3 :::"SD2SDSub"::: )  (Set  "("  ($#k10_radix_1 :::"DecSD"::: )   "(" (Set (Var "y")) "," (Set (Var "n")) "," (Set (Var "k")) ")"  ")" ) ")" ) ")" ))))) ;