:: NUMERAL1  semantic presentation begin  
theorem :: NUMERAL1:1 (Bool  "for" (Set (Var "k")) "," (Set (Var "l")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "(" (Set (Var "k"))  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "l"))  ($#k1_prepower :::"GeoSeq"::: )  ")" ) ")" )  ($#k5_relset_1 :::"|"::: )  (Set (Var "m"))) "is"   ($#m1_hidden :::"XFinSequence":::) "of" (Set   ($#k5_numbers :::"NAT"::: )  ))) ; 
 
theorem :: NUMERAL1:2 (Bool  "for" (Set (Var "d")) "being"   ($#m1_hidden :::"XFinSequence":::) "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool  "("   "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "d"))))) "holds"  (Bool (Set (Var "n"))  ($#r1_nat_d :::"divides"::: )  (Set (Set (Var "d"))  ($#k1_recdef_1 :::"."::: )  (Set (Var "i"))))  ")" )) "holds"  (Bool (Set (Var "n"))  ($#r1_nat_d :::"divides"::: )  (Set   ($#k7_afinsq_2 :::"Sum"::: )  (Set (Var "d")))))) ; 
 
theorem :: NUMERAL1:3 (Bool  "for" (Set (Var "d")) "," (Set (Var "e")) "being"   ($#m1_hidden :::"XFinSequence":::) "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "d")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "e")))) & (Bool  "("   "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "d"))))) "holds"  (Bool (Set (Set (Var "e"))  ($#k1_recdef_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "d"))  ($#k1_recdef_1 :::"."::: )  (Set (Var "i")) ")" )  ($#k4_nat_d :::"mod"::: )  (Set (Var "n"))))  ")" )) "holds"  (Bool (Set (Set  "("  ($#k7_afinsq_2 :::"Sum"::: )  (Set (Var "d")) ")" )  ($#k4_nat_d :::"mod"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k7_afinsq_2 :::"Sum"::: )  (Set (Var "e")) ")" )  ($#k4_nat_d :::"mod"::: )  (Set (Var "n")))))) ; 
 begin  definitionlet "d" be   ($#m1_hidden :::"XFinSequence":::) "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "b" be   ($#m1_hidden :::"Nat":::); func  :::"value":::  "(" "d" "," "b" ")"  ->   ($#m1_hidden :::"Nat":::) means :: NUMERAL1:def 1 (Bool  "ex" (Set (Var "d9")) "being"   ($#m1_hidden :::"XFinSequence":::) "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "d9")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  "d")) & (Bool  "("   "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "d9"))))) "holds"  (Bool (Set (Set (Var "d9"))  ($#k1_recdef_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" "d"  ($#k1_recdef_1 :::"."::: )  (Set (Var "i")) ")" )  ($#k24_binop_2 :::"*"::: )  (Set  "(" "b"  ($#k1_newton :::"|^"::: )  (Set (Var "i")) ")" )))  ")" ) & (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k7_afinsq_2 :::"Sum"::: )  (Set (Var "d9"))))  ")" )); end; 






:: deftheorem    defines :::"value"::: NUMERAL1:def 1 :  (Bool  "for" (Set (Var "d")) "being"   ($#m1_hidden :::"XFinSequence":::) "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "b")) "," (Set (Var "b3")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_numeral1 :::"value"::: )   "(" (Set (Var "d")) "," (Set (Var "b")) ")" )) "iff" (Bool  "ex" (Set (Var "d9")) "being"   ($#m1_hidden :::"XFinSequence":::) "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "d9")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "d")))) & (Bool  "("   "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "d9"))))) "holds"  (Bool (Set (Set (Var "d9"))  ($#k1_recdef_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "d"))  ($#k1_recdef_1 :::"."::: )  (Set (Var "i")) ")" )  ($#k24_binop_2 :::"*"::: )  (Set  "(" (Set (Var "b"))  ($#k1_newton :::"|^"::: )  (Set (Var "i")) ")" )))  ")" ) & (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k7_afinsq_2 :::"Sum"::: )  (Set (Var "d9"))))  ")" ))  ")" ))); 
 definitionlet "n", "b" be   ($#m1_hidden :::"Nat":::); assume 
(Bool (Set (Const "b"))  ($#r1_xxreal_0 :::">"::: )  (Num 1))
 ; func  :::"digits":::  "(" "n" "," "b" ")"  ->   ($#m1_hidden :::"XFinSequence":::) "of" (Set   ($#k5_numbers :::"NAT"::: )  ) means :: NUMERAL1:def 2 (Bool  "("  (Bool (Set   ($#k1_numeral1 :::"value"::: )   "(" it "," "b" ")" )  ($#r1_hidden :::"="::: )  "n") & (Bool (Set it  ($#k1_recdef_1 :::"."::: )  (Set  "(" (Set  "("  ($#k1_afinsq_1 :::"len"::: )  it ")" )  ($#k21_binop_2 :::"-"::: )  (Num 1) ")" ))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool  "("   "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  it))) "holds"  (Bool  "("  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set it  ($#k1_recdef_1 :::"."::: )  (Set (Var "i")))) & (Bool (Set it  ($#k1_recdef_1 :::"."::: )  (Set (Var "i")))  ($#r1_xxreal_0 :::"<"::: )  "b")  ")" )  ")" )  ")" ) if (Bool "n"  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  otherwise (Bool it  ($#r1_hidden :::"="::: )  (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k5_afinsq_1 :::"%>"::: ) )); end; 







:: deftheorem    defines :::"digits"::: NUMERAL1:def 2 :  (Bool  "for" (Set (Var "n")) "," (Set (Var "b")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::">"::: )  (Num 1))) "holds"  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_hidden :::"XFinSequence":::) "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "n"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_numeral1 :::"digits"::: )   "(" (Set (Var "n")) "," (Set (Var "b")) ")" )) "iff" (Bool  "("  (Bool (Set   ($#k1_numeral1 :::"value"::: )   "(" (Set (Var "b3")) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "n"))) & (Bool (Set (Set (Var "b3"))  ($#k1_recdef_1 :::"."::: )  (Set  "(" (Set  "("  ($#k1_afinsq_1 :::"len"::: )  (Set (Var "b3")) ")" )  ($#k21_binop_2 :::"-"::: )  (Num 1) ")" ))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool  "("   "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "b3"))))) "holds"  (Bool  "("  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "b3"))  ($#k1_recdef_1 :::"."::: )  (Set (Var "i")))) & (Bool (Set (Set (Var "b3"))  ($#k1_recdef_1 :::"."::: )  (Set (Var "i")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b")))  ")" )  ")" )  ")" )  ")" )  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "n"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )))) "implies" (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_numeral1 :::"digits"::: )   "(" (Set (Var "n")) "," (Set (Var "b")) ")" )) "iff" (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k5_afinsq_1 :::"%>"::: ) ))  ")" )  ")"   ")" ))); 
 
theorem :: NUMERAL1:4 (Bool  "for" (Set (Var "n")) "," (Set (Var "b")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::">"::: )  (Num 1))) "holds"  (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  (Set  "("  ($#k2_numeral1 :::"digits"::: )   "(" (Set (Var "n")) "," (Set (Var "b")) ")"  ")" ))  ($#r1_xxreal_0 :::">="::: )  (Num 1))) ; 
 
theorem :: NUMERAL1:5 (Bool  "for" (Set (Var "n")) "," (Set (Var "b")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::">"::: )  (Num 1))) "holds"  (Bool (Set   ($#k1_numeral1 :::"value"::: )   "(" (Set  "("  ($#k2_numeral1 :::"digits"::: )   "(" (Set (Var "n")) "," (Set (Var "b")) ")"  ")" ) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "n")))) ; 
 begin  
theorem :: NUMERAL1:6 (Bool  "for" (Set (Var "n")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 10)  ($#k2_newton :::"|^"::: )  (Set (Var "n")) ")" )  ($#k21_binop_2 :::"-"::: )  (Num 1)))) "holds"  (Bool (Num 9)  ($#r1_nat_d :::"divides"::: )  (Set (Var "k")))) ; 
 
theorem :: NUMERAL1:7 (Bool  "for" (Set (Var "n")) "," (Set (Var "b")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::">"::: )  (Num 1))) "holds"  (Bool  "("  (Bool (Set (Var "b"))  ($#r1_nat_d :::"divides"::: )  (Set (Var "n"))) "iff" (Bool (Set (Set  "("  ($#k2_numeral1 :::"digits"::: )   "(" (Set (Var "n")) "," (Set (Var "b")) ")"  ")" )  ($#k1_recdef_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) ; 
 
theorem :: NUMERAL1:8 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool (Num 2)  ($#r1_nat_d :::"divides"::: )  (Set (Var "n"))) "iff" (Bool (Num 2)  ($#r1_nat_d :::"divides"::: )  (Set (Set  "("  ($#k2_numeral1 :::"digits"::: )   "(" (Set (Var "n")) "," (Num 10) ")"  ")" )  ($#k1_recdef_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) )))  ")" )) ; 
 
theorem :: NUMERAL1:9 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool (Num 3)  ($#r1_nat_d :::"divides"::: )  (Set (Var "n"))) "iff" (Bool (Num 3)  ($#r1_nat_d :::"divides"::: )  (Set   ($#k7_afinsq_2 :::"Sum"::: )  (Set  "("  ($#k2_numeral1 :::"digits"::: )   "(" (Set (Var "n")) "," (Num 10) ")"  ")" )))  ")" )) ; 
 
theorem :: NUMERAL1:10 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool (Num 5)  ($#r1_nat_d :::"divides"::: )  (Set (Var "n"))) "iff" (Bool (Num 5)  ($#r1_nat_d :::"divides"::: )  (Set (Set  "("  ($#k2_numeral1 :::"digits"::: )   "(" (Set (Var "n")) "," (Num 10) ")"  ")" )  ($#k1_recdef_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) )))  ")" )) ;