:: ABSVALUE  semantic presentation begin  






definitionlet "x" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; redefine func :::"|.":::"x":::".|"::: equals :: ABSVALUE:def 1 "x" if (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  "x")  otherwise (Set   ($#k4_xcmplx_0 :::"-"::: )  "x"); end; 





:: deftheorem    defines :::"|."::: ABSVALUE:def 1 :  (Bool  "for" (Set (Var "x")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("   "("  (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "x")))) "implies" (Bool (Set  ($#k16_complex1 :::"|."::: ) (Set (Var "x")) ($#k16_complex1 :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set (Var "x")))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "x"))))) "implies" (Bool (Set  ($#k16_complex1 :::"|."::: ) (Set (Var "x")) ($#k16_complex1 :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "x"))))  ")"   ")" )); 
 
theorem :: ABSVALUE:1 (Bool  "for" (Set (Var "x")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "holds"  (Bool  "("  (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Var "x"))) "or" (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "x"))))  ")" )) ; 
 
theorem :: ABSVALUE:2 (Bool  "for" (Set (Var "x")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "iff" (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) ; 
 
theorem :: ABSVALUE:3 (Bool  "for" (Set (Var "x")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "x")))) & (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: ABSVALUE:4 (Bool  "for" (Set (Var "x")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set   ($#k1_real_1 :::"-"::: )  (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set (Var "x")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "x"))) & (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k18_complex1 :::"abs"::: )  (Set (Var "x"))))  ")" )) ; 
 
theorem :: ABSVALUE:5 (Bool  "for" (Set (Var "y")) "," (Set (Var "x")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool  "("  (Bool (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "y")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "x"))) & (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "y")))  ")" ) "iff" (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "y")))  ")" )) ; 
 
theorem :: ABSVALUE:6 (Bool  "for" (Set (Var "x")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set (Var "x")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set  "(" (Num 1)  ($#k13_complex1 :::"/"::: )  (Set (Var "x")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: ABSVALUE:7 (Bool  "for" (Set (Var "x")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set  "(" (Num 1)  ($#k13_complex1 :::"/"::: )  (Set (Var "x")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k13_complex1 :::"/"::: )  (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set (Var "x")) ")" )))) ; 
 
theorem :: ABSVALUE:8 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "x"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "y"))))) "holds"  (Bool (Set   ($#k6_square_1 :::"sqrt"::: )  (Set  "(" (Set (Var "x"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set (Var "x")) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set (Var "y")) ")" ) ")" )))) ; 
 
theorem :: ABSVALUE:9 (Bool  "for" (Set (Var "x")) "," (Set (Var "z")) "," (Set (Var "y")) "," (Set (Var "t")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "z"))) & (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set (Var "y")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "t")))) "holds"  (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set (Var "x"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "y")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "z"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "t"))))) ; 
 
theorem :: ABSVALUE:10 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "x"))  ($#k13_complex1 :::"/"::: )  (Set (Var "y"))))) "holds"  (Bool (Set   ($#k6_square_1 :::"sqrt"::: )  (Set  "(" (Set (Var "x"))  ($#k13_complex1 :::"/"::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set (Var "x")) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set (Var "y")) ")" ) ")" )))) ; 
 
theorem :: ABSVALUE:11 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "x"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "y"))))) "holds"  (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set (Var "x"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set (Var "x")) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set (Var "y")) ")" )))) ; 
 
theorem :: ABSVALUE:12 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set (Var "x"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set (Var "x")) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set (Var "y")) ")" )))) "holds"  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "x"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "y"))))) ; 
 
theorem :: ABSVALUE:13 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set (Var "x"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "y")) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Set  "(" (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set (Var "x"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "y")) ")" ) ")" ) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set (Var "x")) ")" )  ($#k13_complex1 :::"/"::: )  (Set  "(" (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set (Var "x")) ")" ) ")" ) ")" )  ($#k8_complex1 :::"+"::: )  (Set  "(" (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set (Var "y")) ")" )  ($#k13_complex1 :::"/"::: )  (Set  "(" (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set (Var "y")) ")" ) ")" ) ")" )))) ; 
 definitionlet "x" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; func  :::"sgn"::: "x" ->   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   equals :: ABSVALUE:def 2 (Num 1) if (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  "x") (Set   ($#k1_real_1 :::"-"::: )  (Num 1)) if (Bool "x"  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  otherwise (Set   ($#k6_numbers :::"0"::: )  ); projectivity  
(Bool  "for" (Set (Var "b1")) "," (Set (Var "b2")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool  "("  (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b2")))) "implies" (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Num 1))  ")"  &  "("  (Bool (Bool (Set (Var "b2"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Num 1)))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b2")))) & (Bool (Bool  "not" (Set (Var "b2"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )))) "implies" (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ) "holds"  (Bool  "("   "("  (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b1")))) "implies" (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Num 1))  ")"  &  "("  (Bool (Bool (Set (Var "b1"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Num 1)))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b1")))) & (Bool (Bool  "not" (Set (Var "b1"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )))) "implies" (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")"   ")" ))
 ; end; 





:: deftheorem    defines :::"sgn"::: ABSVALUE:def 2 :  (Bool  "for" (Set (Var "x")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("   "("  (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "x")))) "implies" (Bool (Set   ($#k1_absvalue :::"sgn"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Num 1))  ")"  &  "("  (Bool (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool (Set   ($#k1_absvalue :::"sgn"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Num 1)))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "x")))) & (Bool (Bool  "not" (Set (Var "x"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )))) "implies" (Bool (Set   ($#k1_absvalue :::"sgn"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")"   ")" )); 
 registrationlet "x" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set   ($#k1_absvalue :::"sgn"::: )  "x") ->   ($#v1_xreal_0 :::"real"::: )     ($#v1_int_1 :::"integer"::: )   ; 
end; definitionlet "x" be   ($#m1_subset_1 :::"Real":::); :: original: :::"sgn"::: redefine func  :::"sgn"::: "x" ->   ($#m1_subset_1 :::"Real":::); end; 
theorem :: ABSVALUE:14 (Bool  "for" (Set (Var "x")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k1_absvalue :::"sgn"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Num 1))) "holds"  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "x")))) ; 
 
theorem :: ABSVALUE:15 (Bool  "for" (Set (Var "x")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k1_absvalue :::"sgn"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Num 1)))) "holds"  (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: ABSVALUE:16 (Bool  "for" (Set (Var "x")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k1_absvalue :::"sgn"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: ABSVALUE:17 (Bool  "for" (Set (Var "x")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set (Var "x")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k1_absvalue :::"sgn"::: )  (Set (Var "x")) ")" )))) ; 
 
theorem :: ABSVALUE:18 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k1_absvalue :::"sgn"::: )  (Set  "(" (Set (Var "x"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_absvalue :::"sgn"::: )  (Set (Var "x")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k1_absvalue :::"sgn"::: )  (Set (Var "y")) ")" )))) ; 
 
theorem :: ABSVALUE:19 canceled; 
 
theorem :: ABSVALUE:20 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k1_absvalue :::"sgn"::: )  (Set  "(" (Set (Var "x"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "y")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set  "("  ($#k1_absvalue :::"sgn"::: )  (Set (Var "x")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k1_absvalue :::"sgn"::: )  (Set (Var "y")) ")" ) ")" )  ($#k3_real_1 :::"+"::: )  (Num 1)))) ; 
 
theorem :: ABSVALUE:21 (Bool  "for" (Set (Var "x")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "("  ($#k1_absvalue :::"sgn"::: )  (Set (Var "x")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k1_absvalue :::"sgn"::: )  (Set  "(" (Num 1)  ($#k13_complex1 :::"/"::: )  (Set (Var "x")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: ABSVALUE:22 (Bool  "for" (Set (Var "x")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Num 1)  ($#k13_complex1 :::"/"::: )  (Set  "("  ($#k1_absvalue :::"sgn"::: )  (Set (Var "x")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_absvalue :::"sgn"::: )  (Set  "(" (Num 1)  ($#k13_complex1 :::"/"::: )  (Set (Var "x")) ")" )))) ; 
 
theorem :: ABSVALUE:23 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k1_absvalue :::"sgn"::: )  (Set (Var "x")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k1_absvalue :::"sgn"::: )  (Set (Var "y")) ")" ) ")" )  ($#k5_real_1 :::"-"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_absvalue :::"sgn"::: )  (Set  "(" (Set (Var "x"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "y")) ")" )))) ; 
 
theorem :: ABSVALUE:24 (Bool  "for" (Set (Var "x")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k1_absvalue :::"sgn"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_absvalue :::"sgn"::: )  (Set  "(" (Num 1)  ($#k13_complex1 :::"/"::: )  (Set (Var "x")) ")" )))) ; 
 
theorem :: ABSVALUE:25 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k1_absvalue :::"sgn"::: )  (Set  "(" (Set (Var "x"))  ($#k13_complex1 :::"/"::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_absvalue :::"sgn"::: )  (Set (Var "x")) ")" )  ($#k13_complex1 :::"/"::: )  (Set  "("  ($#k1_absvalue :::"sgn"::: )  (Set (Var "y")) ")" )))) ; 
 




theorem :: ABSVALUE:26 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "r"))  ($#k3_real_1 :::"+"::: )  (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set (Var "r")) ")" )))) ; 
 
theorem :: ABSVALUE:27 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "r")) ")" )  ($#k3_real_1 :::"+"::: )  (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set (Var "r")) ")" )))) ; 
 
theorem :: ABSVALUE:28 (Bool  "for" (Set (Var "r")) "," (Set (Var "s")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "holds"  (Bool  "("   "not" (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set (Var "r")))  ($#r1_hidden :::"="::: )  (Set   ($#k18_complex1 :::"abs"::: )  (Set (Var "s")))) "or" (Bool (Set (Var "r"))  ($#r1_hidden :::"="::: )  (Set (Var "s"))) "or" (Bool (Set (Var "r"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "s"))))  ")" )) ; 
 
theorem :: ABSVALUE:29 (Bool  "for" (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Var "m"))  ($#r1_hidden :::"="::: )  (Set   ($#k18_complex1 :::"abs"::: )  (Set (Var "m"))))) ; 
 
theorem :: ABSVALUE:30 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set (Var "r")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "r"))))) ;