:: RADIX_3 semantic presentation begin definitionlet "k" be ($#m1_hidden :::"Nat":::); func "k" :::"-SD_Sub_S"::: -> ($#m1_hidden :::"set"::: ) equals :: RADIX_3:def 1 "{" (Set (Var "e")) where e "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) : (Bool "(" (Bool (Set (Var "e")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Set "(" ($#k1_radix_1 :::"Radix"::: ) (Set "(" "k" ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ))) & (Bool (Set (Var "e")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k1_radix_1 :::"Radix"::: ) (Set "(" "k" ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1))) ")" ) "}" ; func "k" :::"-SD_Sub"::: -> ($#m1_hidden :::"set"::: ) equals :: RADIX_3: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 "(" ($#k4_xcmplx_0 :::"-"::: ) (Set "(" ($#k1_radix_1 :::"Radix"::: ) (Set "(" "k" ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1))) & (Bool (Set (Var "e")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_radix_1 :::"Radix"::: ) (Set "(" "k" ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ))) ")" ) "}" ; end; :: deftheorem defines :::"-SD_Sub_S"::: RADIX_3:def 1 : (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "k")) ($#k1_radix_3 :::"-SD_Sub_S"::: ) ) ($#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 ($#k4_xcmplx_0 :::"-"::: ) (Set "(" ($#k1_radix_1 :::"Radix"::: ) (Set "(" (Set (Var "k")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ))) & (Bool (Set (Var "e")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k1_radix_1 :::"Radix"::: ) (Set "(" (Set (Var "k")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1))) ")" ) "}" )); :: deftheorem defines :::"-SD_Sub"::: RADIX_3:def 2 : (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "k")) ($#k2_radix_3 :::"-SD_Sub"::: ) ) ($#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 "(" ($#k4_xcmplx_0 :::"-"::: ) (Set "(" ($#k1_radix_1 :::"Radix"::: ) (Set "(" (Set (Var "k")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1))) & (Bool (Set (Var "e")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_radix_1 :::"Radix"::: ) (Set "(" (Set (Var "k")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ))) ")" ) "}" )); theorem :: RADIX_3:1 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "i1")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "i1")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "k")) ($#k2_radix_3 :::"-SD_Sub"::: ) ))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set "(" ($#k1_radix_1 :::"Radix"::: ) (Set "(" (Set (Var "k")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i1"))) & (Bool (Set (Var "i1")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_radix_1 :::"Radix"::: ) (Set "(" (Set (Var "k")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ))) ")" ))) ; theorem :: RADIX_3:2 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "k")) ($#k1_radix_3 :::"-SD_Sub_S"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "k")) ($#k2_radix_3 :::"-SD_Sub"::: ) ))) ; theorem :: RADIX_3:3 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "k")) ($#k1_radix_3 :::"-SD_Sub_S"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "k")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ) ($#k1_radix_3 :::"-SD_Sub_S"::: ) ))) ; theorem :: RADIX_3:4 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 2) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k")))) "holds" (Bool (Set (Set (Var "k")) ($#k2_radix_3 :::"-SD_Sub"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "k")) ($#k3_radix_1 :::"-SD"::: ) ))) ; theorem :: RADIX_3:5 (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set ($#k6_numbers :::"0"::: ) ) ($#k1_radix_3 :::"-SD_Sub_S"::: ) )) ; theorem :: RADIX_3:6 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set (Var "k")) ($#k1_radix_3 :::"-SD_Sub_S"::: ) ))) ; theorem :: RADIX_3:7 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set (Var "k")) ($#k2_radix_3 :::"-SD_Sub"::: ) ))) ; theorem :: RADIX_3:8 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "k")) ($#k2_radix_3 :::"-SD_Sub"::: ) ))) "holds" (Bool (Set (Var "e")) "is" ($#m1_hidden :::"Integer":::)))) ; theorem :: RADIX_3:9 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "k")) ($#k2_radix_3 :::"-SD_Sub"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k4_numbers :::"INT"::: ) ))) ; theorem :: RADIX_3:10 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "k")) ($#k1_radix_3 :::"-SD_Sub_S"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k4_numbers :::"INT"::: ) ))) ; registrationlet "k" be ($#m1_hidden :::"Nat":::); cluster (Set "k" ($#k1_radix_3 :::"-SD_Sub_S"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; cluster (Set "k" ($#k2_radix_3 :::"-SD_Sub"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "k" be ($#m1_hidden :::"Nat":::); :: original: :::"-SD_Sub_S"::: redefine func "k" :::"-SD_Sub_S"::: -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k4_numbers :::"INT"::: ) ); end; definitionlet "k" be ($#m1_hidden :::"Nat":::); :: original: :::"-SD_Sub"::: redefine func "k" :::"-SD_Sub"::: -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k4_numbers :::"INT"::: ) ); end; theorem :: RADIX_3:11 (Bool "for" (Set (Var "i")) "," (Set (Var "n")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "aSub")) "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"))))) "holds" (Bool (Set (Set (Var "aSub")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Set (Var "k")) ($#k4_radix_3 :::"-SD_Sub"::: ) )))) ; begin definitionlet "x" be ($#m1_hidden :::"Integer":::); let "k" be ($#m1_hidden :::"Nat":::); func :::"SDSub_Add_Carry"::: "(" "x" "," "k" ")" -> ($#m1_hidden :::"Integer":::) equals :: RADIX_3:def 3 (Num 1) if (Bool (Set ($#k1_radix_1 :::"Radix"::: ) (Set "(" "k" ($#k7_nat_d :::"-'"::: ) (Num 1) ")" )) ($#r1_xxreal_0 :::"<="::: ) "x") (Set ($#k4_xcmplx_0 :::"-"::: ) (Num 1)) if (Bool "x" ($#r1_xxreal_0 :::"<"::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Set "(" ($#k1_radix_1 :::"Radix"::: ) (Set "(" "k" ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ))) otherwise (Set ($#k6_numbers :::"0"::: ) ); end; :: deftheorem defines :::"SDSub_Add_Carry"::: RADIX_3:def 3 : (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" "(" (Bool (Bool (Set ($#k1_radix_1 :::"Radix"::: ) (Set "(" (Set (Var "k")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "x")))) "implies" (Bool (Set ($#k5_radix_3 :::"SDSub_Add_Carry"::: ) "(" (Set (Var "x")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Num 1)) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Set "(" ($#k1_radix_1 :::"Radix"::: ) (Set "(" (Set (Var "k")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" )))) "implies" (Bool (Set ($#k5_radix_3 :::"SDSub_Add_Carry"::: ) "(" (Set (Var "x")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Num 1))) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k1_radix_1 :::"Radix"::: ) (Set "(" (Set (Var "k")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "x")))) & (Bool (Bool "not" (Set (Var "x")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Set "(" ($#k1_radix_1 :::"Radix"::: ) (Set "(" (Set (Var "k")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ))))) "implies" (Bool (Set ($#k5_radix_3 :::"SDSub_Add_Carry"::: ) "(" (Set (Var "x")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ")" ))); definitionlet "x" be ($#m1_hidden :::"Integer":::); let "k" be ($#m1_hidden :::"Nat":::); func :::"SDSub_Add_Data"::: "(" "x" "," "k" ")" -> ($#m1_hidden :::"Integer":::) equals :: RADIX_3:def 4 (Set "x" ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" ($#k1_radix_1 :::"Radix"::: ) "k" ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k5_radix_3 :::"SDSub_Add_Carry"::: ) "(" "x" "," "k" ")" ")" ) ")" )); end; :: deftheorem defines :::"SDSub_Add_Data"::: RADIX_3:def 4 : (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k6_radix_3 :::"SDSub_Add_Data"::: ) "(" (Set (Var "x")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" ($#k1_radix_1 :::"Radix"::: ) (Set (Var "k")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k5_radix_3 :::"SDSub_Add_Carry"::: ) "(" (Set (Var "x")) "," (Set (Var "k")) ")" ")" ) ")" ))))); theorem :: RADIX_3:12 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set ($#k4_xcmplx_0 :::"-"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k5_radix_3 :::"SDSub_Add_Carry"::: ) "(" (Set (Var "x")) "," (Set (Var "k")) ")" )) & (Bool (Set ($#k5_radix_3 :::"SDSub_Add_Carry"::: ) "(" (Set (Var "x")) "," (Set (Var "k")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Num 1)) ")" ))) ; theorem :: RADIX_3:13 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "i1")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Num 2) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "i1")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "k")) ($#k3_radix_1 :::"-SD"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k6_radix_3 :::"SDSub_Add_Data"::: ) "(" (Set (Var "i1")) "," (Set (Var "k")) ")" ) ($#r1_xxreal_0 :::">="::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Set "(" ($#k1_radix_1 :::"Radix"::: ) (Set "(" (Set (Var "k")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ))) & (Bool (Set ($#k6_radix_3 :::"SDSub_Add_Data"::: ) "(" (Set (Var "i1")) "," (Set (Var "k")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k1_radix_1 :::"Radix"::: ) (Set "(" (Set (Var "k")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1))) ")" ))) ; theorem :: RADIX_3:14 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 2) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k")))) "holds" (Bool (Set ($#k5_radix_3 :::"SDSub_Add_Carry"::: ) "(" (Set (Var "x")) "," (Set (Var "k")) ")" ) ($#r2_hidden :::"in"::: ) (Set (Set (Var "k")) ($#k3_radix_3 :::"-SD_Sub_S"::: ) )))) ; theorem :: RADIX_3:15 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Num 2) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "i1")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "k")) ($#k3_radix_1 :::"-SD"::: ) ))) "holds" (Bool (Set (Set "(" ($#k6_radix_3 :::"SDSub_Add_Data"::: ) "(" (Set (Var "i1")) "," (Set (Var "k")) ")" ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k5_radix_3 :::"SDSub_Add_Carry"::: ) "(" (Set (Var "i2")) "," (Set (Var "k")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set (Set (Var "k")) ($#k4_radix_3 :::"-SD_Sub"::: ) )))) ; theorem :: RADIX_3:16 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k5_radix_3 :::"SDSub_Add_Carry"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; begin definitionlet "i", "k", "n" be ($#m1_hidden :::"Nat":::); let "x" be ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Const "n")) "," (Set (Set (Const "k")) ($#k4_radix_3 :::"-SD_Sub"::: ) ); func :::"DigA_SDSub"::: "(" "x" "," "i" ")" -> ($#m1_hidden :::"Integer":::) equals :: RADIX_3:def 5 (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_SDSub"::: RADIX_3: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")) ($#k4_radix_3 :::"-SD_Sub"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n"))))) "implies" (Bool (Set ($#k7_radix_3 :::"DigA_SDSub"::: ) "(" (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 ($#k7_radix_3 :::"DigA_SDSub"::: ) "(" (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 :::"SD2SDSubDigit"::: "(" "x" "," "i" "," "k" ")" -> ($#m1_hidden :::"Integer":::) equals :: RADIX_3:def 6 (Set (Set "(" ($#k6_radix_3 :::"SDSub_Add_Data"::: ) "(" (Set "(" ($#k4_radix_1 :::"DigA"::: ) "(" "x" "," "i" ")" ")" ) "," "k" ")" ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k5_radix_3 :::"SDSub_Add_Carry"::: ) "(" (Set "(" ($#k4_radix_1 :::"DigA"::: ) "(" "x" "," (Set "(" "i" ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ")" ) "," "k" ")" ")" )) if (Bool "i" ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) "n")) (Set ($#k5_radix_3 :::"SDSub_Add_Carry"::: ) "(" (Set "(" ($#k4_radix_1 :::"DigA"::: ) "(" "x" "," (Set "(" "i" ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ")" ) "," "k" ")" ) if (Bool "i" ($#r1_hidden :::"="::: ) (Set "n" ($#k2_xcmplx_0 :::"+"::: ) (Num 1))) otherwise (Set ($#k6_numbers :::"0"::: ) ); end; :: deftheorem defines :::"SD2SDSubDigit"::: RADIX_3:def 6 : (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 ($#k8_radix_3 :::"SD2SDSubDigit"::: ) "(" (Set (Var "x")) "," (Set (Var "i")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_radix_3 :::"SDSub_Add_Data"::: ) "(" (Set "(" ($#k4_radix_1 :::"DigA"::: ) "(" (Set (Var "x")) "," (Set (Var "i")) ")" ")" ) "," (Set (Var "k")) ")" ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k5_radix_3 :::"SDSub_Add_Carry"::: ) "(" (Set "(" ($#k4_radix_1 :::"DigA"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "i")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ")" ) "," (Set (Var "k")) ")" ")" ))) ")" & "(" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1)))) "implies" (Bool (Set ($#k8_radix_3 :::"SD2SDSubDigit"::: ) "(" (Set (Var "x")) "," (Set (Var "i")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_radix_3 :::"SDSub_Add_Carry"::: ) "(" (Set "(" ($#k4_radix_1 :::"DigA"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "i")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ")" ) "," (Set (Var "k")) ")" )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n"))))) & (Bool (Bool "not" (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1))))) "implies" (Bool (Set ($#k8_radix_3 :::"SD2SDSubDigit"::: ) "(" (Set (Var "x")) "," (Set (Var "i")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ")" ))); theorem :: RADIX_3:17 (Bool "for" (Set (Var "k")) "," (Set (Var "i")) "," (Set (Var "n")) "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 (Num 2) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set (Var "n")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" )))) "holds" (Bool (Set ($#k8_radix_3 :::"SD2SDSubDigit"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "k")) ")" ) "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Set (Var "k")) ($#k4_radix_3 :::"-SD_Sub"::: ) )))) ; 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"::: ) ); assume (Bool "(" (Bool (Num 2) ($#r1_xxreal_0 :::"<="::: ) (Set (Const "k"))) & (Bool (Set (Const "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set (Const "n")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ))) ")" ) ; func :::"SD2SDSubDigitS"::: "(" "x" "," "i" "," "k" ")" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set "k" ($#k4_radix_3 :::"-SD_Sub"::: ) ) equals :: RADIX_3:def 7 (Set ($#k8_radix_3 :::"SD2SDSubDigit"::: ) "(" "x" "," "i" "," "k" ")" ); end; :: deftheorem defines :::"SD2SDSubDigitS"::: RADIX_3:def 7 : (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"::: ) ) "st" (Bool (Bool (Num 2) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set (Var "n")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" )))) "holds" (Bool (Set ($#k9_radix_3 :::"SD2SDSubDigitS"::: ) "(" (Set (Var "x")) "," (Set (Var "i")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_radix_3 :::"SD2SDSubDigit"::: ) "(" (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 :::"SD2SDSub"::: "x" -> ($#m2_finseq_1 :::"Tuple":::) "of" (Set "n" ($#k2_xcmplx_0 :::"+"::: ) (Num 1)) "," (Set "k" ($#k4_radix_3 :::"-SD_Sub"::: ) ) means :: RADIX_3: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"::: ) (Set "(" "n" ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" )))) "holds" (Bool (Set ($#k7_radix_3 :::"DigA_SDSub"::: ) "(" it "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_radix_3 :::"SD2SDSubDigitS"::: ) "(" "x" "," (Set (Var "i")) "," "k" ")" ))); end; :: deftheorem defines :::"SD2SDSub"::: RADIX_3:def 8 : (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 (Set (Var "n")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1)) "," (Set (Set (Var "k")) ($#k4_radix_3 :::"-SD_Sub"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k10_radix_3 :::"SD2SDSub"::: ) (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 "(" (Set (Var "n")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" )))) "holds" (Bool (Set ($#k7_radix_3 :::"DigA_SDSub"::: ) "(" (Set (Var "b4")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_radix_3 :::"SD2SDSubDigitS"::: ) "(" (Set (Var "x")) "," (Set (Var "i")) "," (Set (Var "k")) ")" ))) ")" )))); theorem :: RADIX_3:18 (Bool "for" (Set (Var "i")) "," (Set (Var "n")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "aSub")) "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"))))) "holds" (Bool (Set ($#k7_radix_3 :::"DigA_SDSub"::: ) "(" (Set (Var "aSub")) "," (Set (Var "i")) ")" ) "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Set (Var "k")) ($#k4_radix_3 :::"-SD_Sub"::: ) )))) ; theorem :: RADIX_3:19 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Num 2) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (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")) ($#k4_radix_3 :::"-SD_Sub"::: ) ))) "holds" (Bool (Set ($#k6_radix_3 :::"SDSub_Add_Data"::: ) "(" (Set "(" (Set (Var "i1")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "i2")) ")" ) "," (Set (Var "k")) ")" ) ($#r2_hidden :::"in"::: ) (Set (Set (Var "k")) ($#k3_radix_3 :::"-SD_Sub_S"::: ) )))) ; begin definitionlet "i", "k", "n" be ($#m1_hidden :::"Nat":::); let "x" be ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Const "n")) "," (Set (Set (Const "k")) ($#k4_radix_3 :::"-SD_Sub"::: ) ); func :::"DigB_SDSub"::: "(" "x" "," "i" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) equals :: RADIX_3:def 9 (Set ($#k7_radix_3 :::"DigA_SDSub"::: ) "(" "x" "," "i" ")" ); end; :: deftheorem defines :::"DigB_SDSub"::: RADIX_3:def 9 : (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")) ($#k4_radix_3 :::"-SD_Sub"::: ) ) "holds" (Bool (Set ($#k11_radix_3 :::"DigB_SDSub"::: ) "(" (Set (Var "x")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_radix_3 :::"DigA_SDSub"::: ) "(" (Set (Var "x")) "," (Set (Var "i")) ")" )))); definitionlet "i", "k", "n" be ($#m1_hidden :::"Nat":::); let "x" be ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Const "n")) "," (Set (Set (Const "k")) ($#k4_radix_3 :::"-SD_Sub"::: ) ); func :::"SDSub2INTDigit"::: "(" "x" "," "i" "," "k" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) equals :: RADIX_3:def 10 (Set (Set "(" (Set "(" ($#k1_radix_1 :::"Radix"::: ) "k" ")" ) ($#k13_newton :::"|^"::: ) (Set "(" "i" ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k11_radix_3 :::"DigB_SDSub"::: ) "(" "x" "," "i" ")" ")" )); end; :: deftheorem defines :::"SDSub2INTDigit"::: RADIX_3:def 10 : (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")) ($#k4_radix_3 :::"-SD_Sub"::: ) ) "holds" (Bool (Set ($#k12_radix_3 :::"SDSub2INTDigit"::: ) "(" (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 "(" ($#k11_radix_3 :::"DigB_SDSub"::: ) "(" (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")) ($#k4_radix_3 :::"-SD_Sub"::: ) ); func :::"SDSub2INT"::: "x" -> ($#m2_finseq_1 :::"Tuple":::) "of" "n" "," (Set ($#k4_numbers :::"INT"::: ) ) means :: RADIX_3: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 it ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k12_radix_3 :::"SDSub2INTDigit"::: ) "(" "x" "," (Set (Var "i")) "," "k" ")" ))); end; :: deftheorem defines :::"SDSub2INT"::: RADIX_3:def 11 : (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")) ($#k4_radix_3 :::"-SD_Sub"::: ) ) (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 ($#k13_radix_3 :::"SDSub2INT"::: ) (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 ($#k12_radix_3 :::"SDSub2INTDigit"::: ) "(" (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")) ($#k4_radix_3 :::"-SD_Sub"::: ) ); func :::"SDSub2IntOut"::: "x" -> ($#m1_hidden :::"Integer":::) equals :: RADIX_3:def 12 (Set ($#k1_gr_cy_1 :::"Sum"::: ) (Set "(" ($#k13_radix_3 :::"SDSub2INT"::: ) "x" ")" )); end; :: deftheorem defines :::"SDSub2IntOut"::: RADIX_3:def 12 : (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")) ($#k4_radix_3 :::"-SD_Sub"::: ) ) "holds" (Bool (Set ($#k14_radix_3 :::"SDSub2IntOut"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_gr_cy_1 :::"Sum"::: ) (Set "(" ($#k13_radix_3 :::"SDSub2INT"::: ) (Set (Var "x")) ")" ))))); theorem :: RADIX_3:20 (Bool "for" (Set (Var "n")) "," (Set (Var "k")) "," (Set (Var "m")) "," (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 ($#k7_radix_3 :::"DigA_SDSub"::: ) "(" (Set "(" ($#k10_radix_3 :::"SD2SDSub"::: ) (Set "(" ($#k10_radix_1 :::"DecSD"::: ) "(" (Set (Var "m")) "," (Set "(" (Set (Var "n")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "k")) ")" ")" ) ")" ) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_radix_3 :::"DigA_SDSub"::: ) "(" (Set "(" ($#k10_radix_3 :::"SD2SDSub"::: ) (Set "(" ($#k10_radix_1 :::"DecSD"::: ) "(" (Set "(" (Set (Var "m")) ($#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")) ")" ))) ; theorem :: RADIX_3:21 (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")) "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")))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k14_radix_3 :::"SDSub2IntOut"::: ) (Set "(" ($#k10_radix_3 :::"SD2SDSub"::: ) (Set "(" ($#k10_radix_1 :::"DecSD"::: ) "(" (Set (Var "x")) "," (Set (Var "n")) "," (Set (Var "k")) ")" ")" ) ")" ))))) ;