:: XCMPLX_0  semantic presentation begin  definitionfunc  :::"<i>":::  ->    ($#m1_hidden :::"set"::: )   equals :: XCMPLX_0:def 1 (Set  "(" (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")"   ($#k5_funct_4 :::"-->"::: )   "(" (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ); let "c" be    ($#m1_hidden :::"number"::: )  ; attr "c" is  :::"complex":::  means :: XCMPLX_0:def 2 (Bool "c"  ($#r2_hidden :::"in"::: )  (Set   ($#k2_numbers :::"COMPLEX"::: )  )); end; 








:: deftheorem    defines :::"<i>"::: XCMPLX_0:def 1 :  (Bool (Set   ($#k1_xcmplx_0 :::"<i>"::: )  )  ($#r1_hidden :::"="::: )  (Set  "(" (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")"   ($#k5_funct_4 :::"-->"::: )   "(" (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" )); 
 
:: deftheorem    defines :::"complex"::: XCMPLX_0:def 2 :  (Bool  "for" (Set (Var "c")) "being"    ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set (Var "c")) "is"   ($#v1_xcmplx_0 :::"complex"::: )  ) "iff" (Bool (Set (Var "c"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_numbers :::"COMPLEX"::: )  ))  ")" )); 
 registration
cluster (Set   ($#k1_xcmplx_0 :::"<i>"::: )  ) ->   ($#v1_xcmplx_0 :::"complex"::: )   ; 
end; registration
cluster   ($#v1_xcmplx_0 :::"complex"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; registration


  ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )  


(Bool  "ex" (Set (Var "b1")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "for" (Set (Var "b2")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Var "b2"))  ($#r2_hidden :::"in"::: )  (Set (Var "b1")))))
 
; 
end; notationlet "x" be   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )  ; synonym  :::"zero"::: "x" for  :::"empty"::: ; end; definitionlet "x" be   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )  ; redefine attr "x" is  :::"empty":::  means :: XCMPLX_0:def 3 (Bool "x"  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )); end; 




:: deftheorem    defines :::"zero"::: XCMPLX_0:def 3 :  (Bool  "for" (Set (Var "x")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x")) "is"   ($#v1_xboole_0 :::"zero"::: )  ) "iff" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )); 
 definitionlet "x", "y" be   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )  ; func "x" :::"+"::: "y" ->    ($#m1_hidden :::"set"::: )   means :: XCMPLX_0:def 4 (Bool  "ex" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) "st"  (Bool  "("  (Bool "x"  ($#r1_hidden :::"="::: )  (Set  ($#k5_arytm_0 :::"[*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k5_arytm_0 :::"*]"::: ) )) & (Bool "y"  ($#r1_hidden :::"="::: )  (Set  ($#k5_arytm_0 :::"[*"::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k5_arytm_0 :::"*]"::: ) )) & (Bool it  ($#r1_hidden :::"="::: )  (Set  ($#k5_arytm_0 :::"[*"::: ) (Set  "("  ($#k1_arytm_0 :::"+"::: )   "(" (Set (Var "x1")) "," (Set (Var "y1")) ")"  ")" ) "," (Set  "("  ($#k1_arytm_0 :::"+"::: )   "(" (Set (Var "x2")) "," (Set (Var "y2")) ")"  ")" ) ($#k5_arytm_0 :::"*]"::: ) ))  ")" )); commutativity  
(Bool  "for" (Set (Var "b1")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool  "ex" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set  ($#k5_arytm_0 :::"[*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k5_arytm_0 :::"*]"::: ) )) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set  ($#k5_arytm_0 :::"[*"::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k5_arytm_0 :::"*]"::: ) )) & (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set  ($#k5_arytm_0 :::"[*"::: ) (Set  "("  ($#k1_arytm_0 :::"+"::: )   "(" (Set (Var "x1")) "," (Set (Var "y1")) ")"  ")" ) "," (Set  "("  ($#k1_arytm_0 :::"+"::: )   "(" (Set (Var "x2")) "," (Set (Var "y2")) ")"  ")" ) ($#k5_arytm_0 :::"*]"::: ) ))  ")" ))) "holds"  (Bool  "ex" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set  ($#k5_arytm_0 :::"[*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k5_arytm_0 :::"*]"::: ) )) & (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set  ($#k5_arytm_0 :::"[*"::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k5_arytm_0 :::"*]"::: ) )) & (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set  ($#k5_arytm_0 :::"[*"::: ) (Set  "("  ($#k1_arytm_0 :::"+"::: )   "(" (Set (Var "x1")) "," (Set (Var "y1")) ")"  ")" ) "," (Set  "("  ($#k1_arytm_0 :::"+"::: )   "(" (Set (Var "x2")) "," (Set (Var "y2")) ")"  ")" ) ($#k5_arytm_0 :::"*]"::: ) ))  ")" ))))
 ; func "x" :::"*"::: "y" ->    ($#m1_hidden :::"set"::: )   means :: XCMPLX_0:def 5 (Bool  "ex" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) "st"  (Bool  "("  (Bool "x"  ($#r1_hidden :::"="::: )  (Set  ($#k5_arytm_0 :::"[*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k5_arytm_0 :::"*]"::: ) )) & (Bool "y"  ($#r1_hidden :::"="::: )  (Set  ($#k5_arytm_0 :::"[*"::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k5_arytm_0 :::"*]"::: ) )) & (Bool it  ($#r1_hidden :::"="::: )  (Set  ($#k5_arytm_0 :::"[*"::: ) (Set  "("  ($#k1_arytm_0 :::"+"::: )   "(" (Set  "("  ($#k2_arytm_0 :::"*"::: )   "(" (Set (Var "x1")) "," (Set (Var "y1")) ")"  ")" ) "," (Set  "("  ($#k3_arytm_0 :::"opp"::: )  (Set  "("  ($#k2_arytm_0 :::"*"::: )   "(" (Set (Var "x2")) "," (Set (Var "y2")) ")"  ")" ) ")" ) ")"  ")" ) "," (Set  "("  ($#k1_arytm_0 :::"+"::: )   "(" (Set  "("  ($#k2_arytm_0 :::"*"::: )   "(" (Set (Var "x1")) "," (Set (Var "y2")) ")"  ")" ) "," (Set  "("  ($#k2_arytm_0 :::"*"::: )   "(" (Set (Var "x2")) "," (Set (Var "y1")) ")"  ")" ) ")"  ")" ) ($#k5_arytm_0 :::"*]"::: ) ))  ")" )); commutativity  
(Bool  "for" (Set (Var "b1")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool  "ex" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set  ($#k5_arytm_0 :::"[*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k5_arytm_0 :::"*]"::: ) )) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set  ($#k5_arytm_0 :::"[*"::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k5_arytm_0 :::"*]"::: ) )) & (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set  ($#k5_arytm_0 :::"[*"::: ) (Set  "("  ($#k1_arytm_0 :::"+"::: )   "(" (Set  "("  ($#k2_arytm_0 :::"*"::: )   "(" (Set (Var "x1")) "," (Set (Var "y1")) ")"  ")" ) "," (Set  "("  ($#k3_arytm_0 :::"opp"::: )  (Set  "("  ($#k2_arytm_0 :::"*"::: )   "(" (Set (Var "x2")) "," (Set (Var "y2")) ")"  ")" ) ")" ) ")"  ")" ) "," (Set  "("  ($#k1_arytm_0 :::"+"::: )   "(" (Set  "("  ($#k2_arytm_0 :::"*"::: )   "(" (Set (Var "x1")) "," (Set (Var "y2")) ")"  ")" ) "," (Set  "("  ($#k2_arytm_0 :::"*"::: )   "(" (Set (Var "x2")) "," (Set (Var "y1")) ")"  ")" ) ")"  ")" ) ($#k5_arytm_0 :::"*]"::: ) ))  ")" ))) "holds"  (Bool  "ex" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set  ($#k5_arytm_0 :::"[*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k5_arytm_0 :::"*]"::: ) )) & (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set  ($#k5_arytm_0 :::"[*"::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k5_arytm_0 :::"*]"::: ) )) & (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set  ($#k5_arytm_0 :::"[*"::: ) (Set  "("  ($#k1_arytm_0 :::"+"::: )   "(" (Set  "("  ($#k2_arytm_0 :::"*"::: )   "(" (Set (Var "x1")) "," (Set (Var "y1")) ")"  ")" ) "," (Set  "("  ($#k3_arytm_0 :::"opp"::: )  (Set  "("  ($#k2_arytm_0 :::"*"::: )   "(" (Set (Var "x2")) "," (Set (Var "y2")) ")"  ")" ) ")" ) ")"  ")" ) "," (Set  "("  ($#k1_arytm_0 :::"+"::: )   "(" (Set  "("  ($#k2_arytm_0 :::"*"::: )   "(" (Set (Var "x1")) "," (Set (Var "y2")) ")"  ")" ) "," (Set  "("  ($#k2_arytm_0 :::"*"::: )   "(" (Set (Var "x2")) "," (Set (Var "y1")) ")"  ")" ) ")"  ")" ) ($#k5_arytm_0 :::"*]"::: ) ))  ")" ))))
 ; end; 












:: deftheorem    defines :::"+"::: XCMPLX_0:def 4 :  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "b3")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "y")))) "iff" (Bool  "ex" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set  ($#k5_arytm_0 :::"[*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k5_arytm_0 :::"*]"::: ) )) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set  ($#k5_arytm_0 :::"[*"::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k5_arytm_0 :::"*]"::: ) )) & (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set  ($#k5_arytm_0 :::"[*"::: ) (Set  "("  ($#k1_arytm_0 :::"+"::: )   "(" (Set (Var "x1")) "," (Set (Var "y1")) ")"  ")" ) "," (Set  "("  ($#k1_arytm_0 :::"+"::: )   "(" (Set (Var "x2")) "," (Set (Var "y2")) ")"  ")" ) ($#k5_arytm_0 :::"*]"::: ) ))  ")" ))  ")" ))); 
 
:: deftheorem    defines :::"*"::: XCMPLX_0:def 5 :  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "b3")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "y")))) "iff" (Bool  "ex" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set  ($#k5_arytm_0 :::"[*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k5_arytm_0 :::"*]"::: ) )) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set  ($#k5_arytm_0 :::"[*"::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k5_arytm_0 :::"*]"::: ) )) & (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set  ($#k5_arytm_0 :::"[*"::: ) (Set  "("  ($#k1_arytm_0 :::"+"::: )   "(" (Set  "("  ($#k2_arytm_0 :::"*"::: )   "(" (Set (Var "x1")) "," (Set (Var "y1")) ")"  ")" ) "," (Set  "("  ($#k3_arytm_0 :::"opp"::: )  (Set  "("  ($#k2_arytm_0 :::"*"::: )   "(" (Set (Var "x2")) "," (Set (Var "y2")) ")"  ")" ) ")" ) ")"  ")" ) "," (Set  "("  ($#k1_arytm_0 :::"+"::: )   "(" (Set  "("  ($#k2_arytm_0 :::"*"::: )   "(" (Set (Var "x1")) "," (Set (Var "y2")) ")"  ")" ) "," (Set  "("  ($#k2_arytm_0 :::"*"::: )   "(" (Set (Var "x2")) "," (Set (Var "y1")) ")"  ")" ) ")"  ")" ) ($#k5_arytm_0 :::"*]"::: ) ))  ")" ))  ")" ))); 
 registrationlet "z", "z9" be   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set "z"  ($#k2_xcmplx_0 :::"+"::: )  "z9") ->   ($#v1_xcmplx_0 :::"complex"::: )   ; 

cluster (Set "z"  ($#k3_xcmplx_0 :::"*"::: )  "z9") ->   ($#v1_xcmplx_0 :::"complex"::: )   ; 
end; definitionlet "z" be   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )  ; func  :::"-"::: "z" ->   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   means :: XCMPLX_0:def 6 (Bool (Set "z"  ($#k2_xcmplx_0 :::"+"::: )  it)  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )); involutiveness  
(Bool  "for" (Set (Var "b1")) "," (Set (Var "b2")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "b2"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b1")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "b1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )))
 ; func "z" :::""":::  ->   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   means :: XCMPLX_0:def 7 (Bool (Set "z"  ($#k3_xcmplx_0 :::"*"::: )  it)  ($#r1_hidden :::"="::: )  (Num 1)) if (Bool "z"  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  otherwise (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )); involutiveness  
(Bool  "for" (Set (Var "b1")) "," (Set (Var "b2")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool  "("  (Bool (Bool (Set (Var "b2"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool (Set (Set (Var "b2"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b1")))  ($#r1_hidden :::"="::: )  (Num 1))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b2"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )))) "implies" (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ) "holds"  (Bool  "("   "("  (Bool (Bool (Set (Var "b1"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool (Set (Set (Var "b1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Num 1))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b1"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )))) "implies" (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")"   ")" ))
 ; end; 










:: deftheorem    defines :::"-"::: XCMPLX_0:def 6 :  (Bool  "for" (Set (Var "z")) "," (Set (Var "b2")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "z")))) "iff" (Bool (Set (Set (Var "z"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )); 
 
:: deftheorem    defines :::"""::: XCMPLX_0:def 7 :  (Bool  "for" (Set (Var "z")) "," (Set (Var "b2")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "z"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "z"))  ($#k5_xcmplx_0 :::"""::: )  )) "iff" (Bool (Set (Set (Var "z"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Num 1))  ")" )  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "z"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )))) "implies" (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "z"))  ($#k5_xcmplx_0 :::"""::: )  )) "iff" (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")"   ")" )); 
 definitionlet "x", "y" be   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )  ; func "x" :::"-"::: "y" ->    ($#m1_hidden :::"set"::: )   equals :: XCMPLX_0:def 8 (Set "x"  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  "y" ")" )); func "x" :::"/"::: "y" ->    ($#m1_hidden :::"set"::: )   equals :: XCMPLX_0:def 9 (Set "x"  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" "y"  ($#k5_xcmplx_0 :::"""::: )  ")" )); end; 












:: deftheorem    defines :::"-"::: XCMPLX_0:def 8 :  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "x"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "y")) ")" )))); 
 
:: deftheorem    defines :::"/"::: XCMPLX_0:def 9 :  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "x"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "y"))  ($#k5_xcmplx_0 :::"""::: )  ")" )))); 
 registrationlet "x", "y" be   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set "x"  ($#k6_xcmplx_0 :::"-"::: )  "y") ->   ($#v1_xcmplx_0 :::"complex"::: )   ; 

cluster (Set "x"  ($#k7_xcmplx_0 :::"/"::: )  "y") ->   ($#v1_xcmplx_0 :::"complex"::: )   ; 
end; registration
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"zero"::: )   )    ($#v1_xcmplx_0 :::"complex"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; registrationlet "x" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"zero"::: )   )    ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set   ($#k4_xcmplx_0 :::"-"::: )  "x") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"zero"::: )   )    ($#v1_xcmplx_0 :::"complex"::: )   ; 

cluster (Set "x"  ($#k5_xcmplx_0 :::"""::: )  ) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"zero"::: )   )    ($#v1_xcmplx_0 :::"complex"::: )   ; 
let "y" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"zero"::: )   )    ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set "x"  ($#k3_xcmplx_0 :::"*"::: )  "y") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"zero"::: )   )  ; 
end; registrationlet "x", "y" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"zero"::: )   )    ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set "x"  ($#k7_xcmplx_0 :::"/"::: )  "y") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"zero"::: )   )  ; 
end; registration
cluster   ->   ($#v1_xcmplx_0 :::"complex"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ); 
end; registration
cluster   ($#v7_ordinal1 :::"natural"::: )    ->   ($#v1_xcmplx_0 :::"complex"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; registration
cluster   ->   ($#v1_xcmplx_0 :::"complex"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ); 
end;