:: ARITHM  semantic presentation begin  



theorem :: ARITHM:1 (Bool  "for" (Set (Var "x")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "x"))  ($#k2_xcmplx_0 :::"+"::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "x")))) ; 
 
theorem :: ARITHM:2 (Bool  "for" (Set (Var "x")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "x"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: ARITHM:3 (Bool  "for" (Set (Var "x")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Num 1)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Var "x")))) ; 
 
theorem :: ARITHM:4 (Bool  "for" (Set (Var "x")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "x"))  ($#k6_xcmplx_0 :::"-"::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "x")))) ; 
 
theorem :: ARITHM:5 (Bool  "for" (Set (Var "x")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  ($#k6_numbers :::"0"::: ) )  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: ARITHM:6 (Bool  "for" (Set (Var "x")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "x"))  ($#k7_xcmplx_0 :::"/"::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "x")))) ;