:: XCMPLX_1  semantic presentation begin  







theorem :: XCMPLX_1:1 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "c")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "c"))))) ; 
 
theorem :: XCMPLX_1:2 (Bool  "for" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "c"))))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "b")))) ; 
 
theorem :: XCMPLX_1:3 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b"))))) "holds"  (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: XCMPLX_1:4 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "b"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "c")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "c"))))) ; 
 
theorem :: XCMPLX_1:5 (Bool  "for" (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "c"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "c"))))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "b")))) ; 
 
theorem :: XCMPLX_1:6 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "holds"  (Bool  "("   "not" (Bool (Set (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "or" (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "or" (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) ; 
 
theorem :: XCMPLX_1:7 (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Var "b")))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: XCMPLX_1:8 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "b"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "c")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "c")) ")" )))) ; 
 
theorem :: XCMPLX_1:9 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "c")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "d")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "d")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "d")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "c"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "d")) ")" )))) ; 
 
theorem :: XCMPLX_1:10 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "c"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "d")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "c")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "d")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "c")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "d")) ")" )))) ; 
 
theorem :: XCMPLX_1:11 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "a"))))) ; 
 
theorem :: XCMPLX_1:12 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "a")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "a"))))) ; 
 
theorem :: XCMPLX_1:13 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Num 4)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "a")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "a")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "a"))))) ; 
 
theorem :: XCMPLX_1:14 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: XCMPLX_1:15 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "b")))) ; 
 
theorem :: XCMPLX_1:16 (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "b"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "b")))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: XCMPLX_1:17 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "b"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )))) ; 
 
theorem :: XCMPLX_1:18 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "b")))) ; 
 
theorem :: XCMPLX_1:19 (Bool  "for" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c"))))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "b")))) ; 
 
theorem :: XCMPLX_1:20 (Bool  "for" (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "c"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "c"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b"))))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "b")))) ; 
 
theorem :: XCMPLX_1:21 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b"))))) ; 
 
theorem :: XCMPLX_1:22 (Bool  "for" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "c"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )))) ; 
 
theorem :: XCMPLX_1:23 (Bool  "for" (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "c"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "a")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "c"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "a"))))) ; 
 
theorem :: XCMPLX_1:24 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "c"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "d"))))) "holds"  (Bool (Set (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "d"))))) ; 
 
theorem :: XCMPLX_1:25 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )))) ; 
 
theorem :: XCMPLX_1:26 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b"))))) ; 
 
theorem :: XCMPLX_1:27 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b"))))) ; 
 
theorem :: XCMPLX_1:28 (Bool  "for" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "c"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )))) ; 
 
theorem :: XCMPLX_1:29 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b"))))) ; 
 
theorem :: XCMPLX_1:30 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "c"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "a"))))) ; 
 
theorem :: XCMPLX_1:31 (Bool  "for" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "b"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c")) ")" )))) ; 
 
theorem :: XCMPLX_1:32 (Bool  "for" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "c"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")) ")" )))) ; 
 
theorem :: XCMPLX_1:33 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "c"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "d"))))) "holds"  (Bool (Set (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "d"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b"))))) ; 
 
theorem :: XCMPLX_1:34 (Bool  "for" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "d"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b"))))) "holds"  (Bool (Set (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "c"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "d"))))) ; 
 
theorem :: XCMPLX_1:35 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "c"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "d"))))) "holds"  (Bool (Set (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "d")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "c"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b"))))) ; 
 
theorem :: XCMPLX_1:36 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "b"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "c")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c"))))) ; 
 
theorem :: XCMPLX_1:37 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "b"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "c"))))) ; 
 
theorem :: XCMPLX_1:38 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "b"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "c"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )))) ; 
 
theorem :: XCMPLX_1:39 (Bool  "for" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c")) ")" )))) ; 
 
theorem :: XCMPLX_1:40 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "b"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "c")) ")" )))) ; 
 
theorem :: XCMPLX_1:41 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "c"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "d")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "b"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "a")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "d"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c")) ")" )))) ; 
 
theorem :: XCMPLX_1:42 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "d")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "d")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "b"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "d")) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "c"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "d")) ")" )))) ; 
 
theorem :: XCMPLX_1:43 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "d")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "d")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "d")) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "c"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "d")) ")" )))) ; 
 
theorem :: XCMPLX_1:44 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "c")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "d")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "d")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "b"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "d")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "c"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "d")) ")" )))) ; 
 
theorem :: XCMPLX_1:45 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "c"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "d")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "c")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "d")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "c")) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "b"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "d")) ")" )))) ; 
 
theorem :: XCMPLX_1:46 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "c"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "d")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "c")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "d")) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "b"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "c")) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "b"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "d")) ")" )))) ; 
 
theorem :: XCMPLX_1:47 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "e")) "," (Set (Var "d")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "e"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "d")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "e")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "d")) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "b"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "e")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "d")) ")" )))) ; 
 
theorem :: XCMPLX_1:48 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "c")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b"))))) ; 
 
theorem :: XCMPLX_1:49 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: XCMPLX_1:50 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: XCMPLX_1:51 (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set (Var "b"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")) ")" )))) ; 
 
theorem :: XCMPLX_1:52 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "b")))) ; 
 
theorem :: XCMPLX_1:53 (Bool  "for" (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "c"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "c"))))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "b")))) ; 
 
theorem :: XCMPLX_1:54 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")) ")" )))) ; 
 
theorem :: XCMPLX_1:55 (Bool  "for" (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "c"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "c")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set (Var "b"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "c")) ")" )))) ; 
 
theorem :: XCMPLX_1:56 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Num 1)  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Num 1)  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "a")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "a")))) ; 
 
theorem :: XCMPLX_1:57 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Num 1)  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "a"))))) ; 
 
theorem :: XCMPLX_1:58 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Num 1))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "b")))) ; 
 
theorem :: XCMPLX_1:59 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Num 1)  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b"))))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "b")))) ; 
 
theorem :: XCMPLX_1:60 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: XCMPLX_1:61 (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "b"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "b")))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: XCMPLX_1:62 (Bool  "for" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "c")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "c")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "c"))))) ; 
 
theorem :: XCMPLX_1:63 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "e")) "," (Set (Var "d")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "e")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "d")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "d")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "d")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "e"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "d")) ")" )))) ; 
 
theorem :: XCMPLX_1:64 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "a")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Num 2))  ($#r1_hidden :::"="::: )  (Set (Var "a")))) ; 
 
theorem :: XCMPLX_1:65 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Num 2) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Num 2) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "a")))) ; 
 
theorem :: XCMPLX_1:66 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Num 2)))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "b")))) ; 
 
theorem :: XCMPLX_1:67 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "a")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "a")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Num 3))  ($#r1_hidden :::"="::: )  (Set (Var "a")))) ; 
 
theorem :: XCMPLX_1:68 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Num 3) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Num 3) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Num 3) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "a")))) ; 
 
theorem :: XCMPLX_1:69 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "a")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "a")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "a")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Num 4))  ($#r1_hidden :::"="::: )  (Set (Var "a")))) ; 
 
theorem :: XCMPLX_1:70 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Num 4) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Num 4) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Num 4) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Num 4) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "a")))) ; 
 
theorem :: XCMPLX_1:71 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Num 4) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Num 4) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Num 2)))) ; 
 
theorem :: XCMPLX_1:72 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "a")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Num 4))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Num 2)))) ; 
 
theorem :: XCMPLX_1:73 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Num 1))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b"))))) ; 
 
theorem :: XCMPLX_1:74 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "b"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "c")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "c"))))) ; 
 
theorem :: XCMPLX_1:75 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "e")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "e")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "e"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a"))))) ; 
 
theorem :: XCMPLX_1:76 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "c"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "d")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "c")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set (Var "b"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "d")) ")" )))) ; 
 
theorem :: XCMPLX_1:77 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set (Var "b"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "c")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "c")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b"))))) ; 
 
theorem :: XCMPLX_1:78 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set (Var "b"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "c")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "c"))))) ; 
 
theorem :: XCMPLX_1:79 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set (Var "b"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "c")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "c"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")) ")" )))) ; 
 
theorem :: XCMPLX_1:80 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set (Var "b"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "c")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "c"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a"))))) ; 
 
theorem :: XCMPLX_1:81 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "e")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set (Var "b"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "e")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "e"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")) ")" )))) ; 
 
theorem :: XCMPLX_1:82 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set (Var "b"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "c")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "c"))))) ; 
 
theorem :: XCMPLX_1:83 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set (Var "c"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "d")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "c")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "d"))))) ; 
 
theorem :: XCMPLX_1:84 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set (Var "c"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "d")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "d")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set (Var "b"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "c")) ")" )))) ; 
 
theorem :: XCMPLX_1:85 (Bool  "for" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b")) "," (Set (Var "d")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "c")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "b"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "d")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "d")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "b"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "c")) ")" )))) ; 
 
theorem :: XCMPLX_1:86 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set  "(" (Set (Var "b"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "c")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "d"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "e")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "e"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "c")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set (Var "b"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "d")) ")" ) ")" )))) ; 
 
theorem :: XCMPLX_1:87 (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Var "a")))) ; 
 
theorem :: XCMPLX_1:88 (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "b"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")) ")" )))) ; 
 
theorem :: XCMPLX_1:89 (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b"))))) ; 
 
theorem :: XCMPLX_1:90 (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "c"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")) ")" )))) ; 
 
theorem :: XCMPLX_1:91 (Bool  "for" (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "c"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "c")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set (Var "b"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "c")) ")" )))) ; 
 
theorem :: XCMPLX_1:92 (Bool  "for" (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "c"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set (Var "b"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "c")) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "c"))))) ; 
 
theorem :: XCMPLX_1:93 (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set (Var "b"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "c")) ")" )))) ; 
 
theorem :: XCMPLX_1:94 (Bool  "for" (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "c"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "d"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "d"))))) "holds"  (Bool (Set (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "d")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "c"))))) ; 
 
theorem :: XCMPLX_1:95 (Bool  "for" (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "c"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "d"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "d")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "c"))))) "holds"  (Bool (Set (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "d"))))) ; 
 
theorem :: XCMPLX_1:96 (Bool  "for" (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "c"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "d"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "d"))))) "holds"  (Bool (Set (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "d")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "c"))))) ; 
 
theorem :: XCMPLX_1:97 (Bool  "for" (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "c"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "c"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "c")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")) ")" )))) ; 
 
theorem :: XCMPLX_1:98 (Bool  "for" (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "c"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "c")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "c"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")) ")" )))) ; 
 
theorem :: XCMPLX_1:99 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Num 1)  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b"))))) ; 
 
theorem :: XCMPLX_1:100 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Num 1)  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b"))))) ; 
 
theorem :: XCMPLX_1:101 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Num 1)  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "c")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a"))))) ; 
 
theorem :: XCMPLX_1:102 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Num 1)  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "a")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Num 1)  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")) ")" )))) ; 
 
theorem :: XCMPLX_1:103 (Bool  "for" (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Num 1)  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "c")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set (Var "b"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "c")) ")" )))) ; 
 
theorem :: XCMPLX_1:104 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 1)  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "c")) ")" )))) ; 
 
theorem :: XCMPLX_1:105 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 1)  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "c")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")) ")" )))) ; 
 
theorem :: XCMPLX_1:106 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Num 1)  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "a")) ")" ))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: XCMPLX_1:107 (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Num 1)  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")) ")" )))) ; 
 
theorem :: XCMPLX_1:108 (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set  "(" (Num 1)  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")) ")" )))) ; 
 
theorem :: XCMPLX_1:109 (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Num 1)  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b"))))) ; 
 
theorem :: XCMPLX_1:110 (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set (Var "b"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Num 1)  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")) ")" ) ")" )))) ; 
 
theorem :: XCMPLX_1:111 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Num 1)  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: XCMPLX_1:112 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "b"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "a")) ")" ))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: XCMPLX_1:113 (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "c")) ")" ) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b"))))) ; 
 
theorem :: XCMPLX_1:114 (Bool  "for" (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "c"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "c"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "c")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "c")) ")" ) ")" )))) ; 
 
theorem :: XCMPLX_1:115 (Bool  "for" (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "c"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "c")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "c")) ")" ) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "c"))))) ; 
 
theorem :: XCMPLX_1:116 (Bool  "for" (Set (Var "b")) "," (Set (Var "d")) "," (Set (Var "a")) "," (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "d"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "c"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "d")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "d")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "c"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")) ")" ) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set (Var "b"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "d")) ")" )))) ; 
 
theorem :: XCMPLX_1:117 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Num 1)  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "a")) ")" ) ")" )))) ; 
 
theorem :: XCMPLX_1:118 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b"))))) ; 
 
theorem :: XCMPLX_1:119 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")) ")" ) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b"))))) ; 
 
theorem :: XCMPLX_1:120 (Bool  "for" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "c")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "b"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "c")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "c"))))) ; 
 
theorem :: XCMPLX_1:121 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Num 2) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Num 2)))) ; 
 
theorem :: XCMPLX_1:122 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "d")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "d")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "b"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "d")) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "c"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "d")) ")" )))) ; 
 
theorem :: XCMPLX_1:123 (Bool  "for" (Set (Var "b")) "," (Set (Var "d")) "," (Set (Var "a")) "," (Set (Var "e")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "d"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set (Var "d"))) & (Bool (Set (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "e"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "d"))))) "holds"  (Bool (Set (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "e")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set (Var "b"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "d")) ")" )))) ; 
 
theorem :: XCMPLX_1:124 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "e")) "," (Set (Var "d")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "e")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "d")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "d")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "d")) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "e"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "d")) ")" )))) ; 
 
theorem :: XCMPLX_1:125 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "e")) "," (Set (Var "d")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "e")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "d")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "d")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "b"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "d")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "e"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "d")) ")" )))) ; 
 
theorem :: XCMPLX_1:126 (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "e")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "e")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "e"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")) ")" ) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b"))))) ; 
 
theorem :: XCMPLX_1:127 (Bool  "for" (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "c"))  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "c"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "a")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b"))))) ; 
 
theorem :: XCMPLX_1:128 (Bool  "for" (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "c"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "c"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "c")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "b"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "c")) ")" ) ")" )))) ; 
 
theorem :: XCMPLX_1:129 (Bool  "for" (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "c"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "c")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "b"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "c")) ")" ) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "c"))))) ; 
 
theorem :: XCMPLX_1:130 (Bool  "for" (Set (Var "b")) "," (Set (Var "d")) "," (Set (Var "a")) "," (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "d"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "c"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "d")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "d")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "c"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")) ")" ) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set (Var "b"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "d")) ")" )))) ; 
 
theorem :: XCMPLX_1:131 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Num 1)  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "b"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "a")) ")" ) ")" )))) ; 
 
theorem :: XCMPLX_1:132 (Bool  "for" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Var "c"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "c")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "a"))))) ; 
 
theorem :: XCMPLX_1:133 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "b"))))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "b")))) ; 
 
theorem :: XCMPLX_1:134 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: XCMPLX_1:135 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "b")))) ; 
 
theorem :: XCMPLX_1:136 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )))) ; 
 
theorem :: XCMPLX_1:137 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" ) ")" )))) ; 
 
theorem :: XCMPLX_1:138 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "a")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b"))))) ; 
 
theorem :: XCMPLX_1:139 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )))) ; 
 
theorem :: XCMPLX_1:140 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )))) ; 
 
theorem :: XCMPLX_1:141 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" ) ")" )))) ; 
 
theorem :: XCMPLX_1:142 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "a"))))) ; 
 
theorem :: XCMPLX_1:143 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "a"))))) ; 
 
theorem :: XCMPLX_1:144 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )))) ; 
 
theorem :: XCMPLX_1:145 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b"))))) ; 
 
theorem :: XCMPLX_1:146 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "a"))))) ; 
 
theorem :: XCMPLX_1:147 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "c")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "a"))))) ; 
 
theorem :: XCMPLX_1:148 (Bool  "for" (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "c"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "a")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "c"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )))) ; 
 
theorem :: XCMPLX_1:149 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  ($#k6_numbers :::"0"::: ) )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a"))))) ; 
 
theorem :: XCMPLX_1:150 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )))) ; 
 
theorem :: XCMPLX_1:151 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "b"))  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" ) ")" )))) ; 
 
theorem :: XCMPLX_1:152 (Bool  "for" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "c")) ")" )))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "b")))) ; 
 
theorem :: XCMPLX_1:153 (Bool  "for" (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "c"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "c"))  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "b")))) ; 
 
theorem :: XCMPLX_1:154 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "c")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "a")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b"))))) ; 
 
theorem :: XCMPLX_1:155 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "c")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "a"))))) ; 
 
theorem :: XCMPLX_1:156 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "c"))))) ; 
 
theorem :: XCMPLX_1:157 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "a"))))) ; 
 
theorem :: XCMPLX_1:158 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "c")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "a")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b"))))) ; 
 
theorem :: XCMPLX_1:159 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "c")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "a"))))) ; 
 
theorem :: XCMPLX_1:160 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "a"))))) ; 
 
theorem :: XCMPLX_1:161 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b"))))) ; 
 
theorem :: XCMPLX_1:162 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b"))))) ; 
 
theorem :: XCMPLX_1:163 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )))) ; 
 
theorem :: XCMPLX_1:164 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "c")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "a"))))) ; 
 
theorem :: XCMPLX_1:165 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "c")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "a")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b"))))) ; 
 
theorem :: XCMPLX_1:166 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "c")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c"))))) ; 
 
theorem :: XCMPLX_1:167 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "c"))))) ; 
 
theorem :: XCMPLX_1:168 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "c")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c"))))) ; 
 
theorem :: XCMPLX_1:169 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "c"))))) ; 
 
theorem :: XCMPLX_1:170 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "c")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c"))))) ; 
 
theorem :: XCMPLX_1:171 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "c"))))) ; 
 
theorem :: XCMPLX_1:172 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "c")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c"))))) ; 
 
theorem :: XCMPLX_1:173 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "c"))))) ; 
 
theorem :: XCMPLX_1:174 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")) ")" )))) ; 
 
theorem :: XCMPLX_1:175 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )))) ; 
 
theorem :: XCMPLX_1:176 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b"))))) ; 
 
theorem :: XCMPLX_1:177 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b"))))) ; 
 
theorem :: XCMPLX_1:178 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b"))))) ; 
 
theorem :: XCMPLX_1:179 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Num 1) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a"))))) ; 
 
theorem :: XCMPLX_1:180 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "a")))) ; 
 
theorem :: XCMPLX_1:181 (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "b"))))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Num 1)))) ; 
 
theorem :: XCMPLX_1:182 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "holds"  (Bool  "("   "not" (Bool (Set (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Num 1)) "or" (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Num 1)) "or" (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Num 1)))  ")" )) ; 
 
theorem :: XCMPLX_1:183 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "a")))) ; 
 
theorem :: XCMPLX_1:184 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "b"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "a")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "c")) ")" )))) ; 
 
theorem :: XCMPLX_1:185 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Set (Var "b"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "a")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "c")) ")" )))) ; 
 
theorem :: XCMPLX_1:186 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a"))))) ; 
 
theorem :: XCMPLX_1:187 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b"))))) ; 
 
theorem :: XCMPLX_1:188 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")) ")" )))) ; 
 
theorem :: XCMPLX_1:189 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b"))))) ; 
 
theorem :: XCMPLX_1:190 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b"))))) ; 
 
theorem :: XCMPLX_1:191 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b"))))) ; 
 
theorem :: XCMPLX_1:192 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )))) ; 
 
theorem :: XCMPLX_1:193 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Num 1) ")" )))) ; 
 
theorem :: XCMPLX_1:194 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Num 1) ")" )))) ; 
 
theorem :: XCMPLX_1:195 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Num 1)))) "holds"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "b")))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a"))))  ")" )) ; 
 
theorem :: XCMPLX_1:196 (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "b"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "b"))))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Num 1)))) ; 
 
theorem :: XCMPLX_1:197 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Num 1)))) ; 
 
theorem :: XCMPLX_1:198 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Num 1)))) ; 
 
theorem :: XCMPLX_1:199 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "a")))) & (Bool (Bool  "not" (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Num 1)))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Num 1)))) ; 
 
theorem :: XCMPLX_1:200 (Bool  "for" (Set (Var "b")) "," (Set (Var "d")) "," (Set (Var "a")) "," (Set (Var "e")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "d"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "d")))) & (Bool (Set (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "e"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "d"))))) "holds"  (Bool (Set (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "e")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set (Var "b"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "d")) ")" )))) ; 
 
theorem :: XCMPLX_1:201 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "a"))  ($#k5_xcmplx_0 :::"""::: )  )  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k5_xcmplx_0 :::"""::: )  ))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "b")))) ; 
 
theorem :: XCMPLX_1:202 (Bool (Set (Set  ($#k6_numbers :::"0"::: ) )  ($#k5_xcmplx_0 :::"""::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) ; 
 
theorem :: XCMPLX_1:203 (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "b"))  ($#k5_xcmplx_0 :::"""::: )  ")" )))) ; 
 
theorem :: XCMPLX_1:204 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k5_xcmplx_0 :::"""::: )  ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "b"))  ($#k5_xcmplx_0 :::"""::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")) ")" )  ($#k5_xcmplx_0 :::"""::: )  ))) ; 
 
theorem :: XCMPLX_1:205 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "b"))  ($#k5_xcmplx_0 :::"""::: )  ")" ) ")" )  ($#k5_xcmplx_0 :::"""::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k5_xcmplx_0 :::"""::: )  ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b"))))) ; 
 
theorem :: XCMPLX_1:206 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k5_xcmplx_0 :::"""::: )  ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "b"))  ($#k5_xcmplx_0 :::"""::: )  ")" ) ")" )  ($#k5_xcmplx_0 :::"""::: )  )  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b"))))) ; 
 
theorem :: XCMPLX_1:207 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "b"))  ($#k5_xcmplx_0 :::"""::: )  ")" ))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: XCMPLX_1:208 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k5_xcmplx_0 :::"""::: )  ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "b"))  ($#k5_xcmplx_0 :::"""::: )  ")" ))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: XCMPLX_1:209 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "b"))  ($#k5_xcmplx_0 :::"""::: )  ")" ))  ($#r1_hidden :::"="::: )  (Num 1))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "b")))) ; 
 
theorem :: XCMPLX_1:210 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Num 1))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k5_xcmplx_0 :::"""::: )  ))) ; 
 
theorem :: XCMPLX_1:211 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k5_xcmplx_0 :::"""::: )  ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k5_xcmplx_0 :::"""::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")) ")" )  ($#k5_xcmplx_0 :::"""::: )  ")" )))) ; 
 
theorem :: XCMPLX_1:212 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k5_xcmplx_0 :::"""::: )  ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "b"))  ($#k5_xcmplx_0 :::"""::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "b"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "a")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")) ")" )  ($#k5_xcmplx_0 :::"""::: )  ")" )))) ; 
 
theorem :: XCMPLX_1:213 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")) ")" )  ($#k5_xcmplx_0 :::"""::: )  )  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "a"))))) ; 
 
theorem :: XCMPLX_1:214 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k5_xcmplx_0 :::"""::: )  ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set (Var "b"))  ($#k5_xcmplx_0 :::"""::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "a"))))) ; 
 
theorem :: XCMPLX_1:215 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Num 1)  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k5_xcmplx_0 :::"""::: )  ))) ; 
 
theorem :: XCMPLX_1:216 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Num 1)  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set (Var "a"))  ($#k5_xcmplx_0 :::"""::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "a")))) ; 
 
theorem :: XCMPLX_1:217 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Num 1)  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "a")) ")" )  ($#k5_xcmplx_0 :::"""::: )  )  ($#r1_hidden :::"="::: )  (Set (Var "a")))) ; 
 
theorem :: XCMPLX_1:218 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Num 1)  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k5_xcmplx_0 :::"""::: )  ))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "b")))) ; 
 
theorem :: XCMPLX_1:219 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set (Var "b"))  ($#k5_xcmplx_0 :::"""::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b"))))) ; 
 
theorem :: XCMPLX_1:220 (Bool  "for" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k5_xcmplx_0 :::"""::: )  ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "c"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "c"))  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")) ")" )))) ; 
 
theorem :: XCMPLX_1:221 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k5_xcmplx_0 :::"""::: )  ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")) ")" )  ($#k5_xcmplx_0 :::"""::: )  ))) ; 
 
theorem :: XCMPLX_1:222 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a")) ")" )  ($#k5_xcmplx_0 :::"""::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "a"))  ($#k5_xcmplx_0 :::"""::: )  ")" )))) ; 
 
theorem :: XCMPLX_1:223 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k5_xcmplx_0 :::"""::: )  )) & (Bool (Bool  "not" (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Num 1)))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Num 1)))) ; 
 begin  
theorem :: XCMPLX_1:224 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "c")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "c"))))) ; 
 
theorem :: XCMPLX_1:225 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "c")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "c"))))) ; 
 
theorem :: XCMPLX_1:226 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c"))))) ; 
 
theorem :: XCMPLX_1:227 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c"))))) ; 
 
theorem :: XCMPLX_1:228 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "a")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "b"))))) ; 
 
theorem :: XCMPLX_1:229 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "a")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "b"))))) ; 
 
theorem :: XCMPLX_1:230 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "b"))))) ; 
 
theorem :: XCMPLX_1:231 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "b"))))) ; 
 begin  
theorem :: XCMPLX_1:232 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "ex" (Set (Var "e")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "st" (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "e")))))) ; 
 
theorem :: XCMPLX_1:233 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set  "(" (Set (Var "b"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "c")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "d"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "e")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "e"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "c")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set (Var "b"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "d")) ")" ) ")" )))) ; 
 
theorem :: XCMPLX_1:234 (Bool  "for" (Set (Var "d")) "," (Set (Var "c")) "," (Set (Var "b")) "," (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "d"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Num 1)  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "c")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "d")) ")" )))) ; 
 
theorem :: XCMPLX_1:235 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "b"))  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "c"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "a")) ")" ) ")" )))) ;