:: XREAL_0  semantic presentation begin  definitionlet "r" be    ($#m1_hidden :::"number"::: )  ; attr "r" is  :::"real":::  means :: XREAL_0:def 1 (Bool "r"  ($#r2_hidden :::"in"::: )  (Set   ($#k1_numbers :::"REAL"::: )  )); end; 




:: deftheorem    defines :::"real"::: XREAL_0:def 1 :  (Bool  "for" (Set (Var "r")) "being"    ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set (Var "r")) "is"   ($#v1_xreal_0 :::"real"::: )  ) "iff" (Bool (Set (Var "r"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_numbers :::"REAL"::: )  ))  ")" )); 
 registration
cluster   ->   ($#v1_xreal_0 :::"real"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ); 
end; registration
cluster (Set   ($#k2_xxreal_0 :::"-infty"::: )  ) ->  ($#~v1_xreal_0  "non"   ($#v1_xreal_0 :::"real"::: )   )  ; 

cluster (Set   ($#k1_xxreal_0 :::"+infty"::: )  ) ->  ($#~v1_xreal_0  "non"   ($#v1_xreal_0 :::"real"::: )   )  ; 
end; registration
cluster   ($#v7_ordinal1 :::"natural"::: )    ->   ($#v1_xreal_0 :::"real"::: )    for    ($#m1_hidden :::"set"::: )  ; 

cluster   ($#v1_xreal_0 :::"real"::: )    ->   ($#v1_xcmplx_0 :::"complex"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; registration
cluster   ($#v1_xreal_0 :::"real"::: )    for    ($#m1_hidden :::"set"::: )  ; 

cluster   ($#v1_xreal_0 :::"real"::: )    ->   ($#v1_xxreal_0 :::"ext-real"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; registrationlet "x" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set   ($#k4_xcmplx_0 :::"-"::: )  "x") ->   ($#v1_xreal_0 :::"real"::: )   ; 

cluster (Set "x"  ($#k5_xcmplx_0 :::"""::: )  ) ->   ($#v1_xreal_0 :::"real"::: )   ; 
let "y" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set "x"  ($#k2_xcmplx_0 :::"+"::: )  "y") ->   ($#v1_xreal_0 :::"real"::: )   ; 

cluster (Set "x"  ($#k3_xcmplx_0 :::"*"::: )  "y") ->   ($#v1_xreal_0 :::"real"::: )   ; 
end; registrationlet "x", "y" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set "x"  ($#k6_xcmplx_0 :::"-"::: )  "y") ->   ($#v1_xreal_0 :::"real"::: )   ; 

cluster (Set "x"  ($#k7_xcmplx_0 :::"/"::: )  "y") ->   ($#v1_xreal_0 :::"real"::: )   ; 
end; begin  




registration
cluster   ($#v1_xcmplx_0 :::"complex"::: )     ($#v1_xxreal_0 :::"ext-real"::: )     ($#v2_xxreal_0 :::"positive"::: )     ($#v1_xreal_0 :::"real"::: )    for    ($#m1_hidden :::"set"::: )  ; 

cluster   ($#v1_xcmplx_0 :::"complex"::: )     ($#v1_xxreal_0 :::"ext-real"::: )     ($#v3_xxreal_0 :::"negative"::: )     ($#v1_xreal_0 :::"real"::: )    for    ($#m1_hidden :::"set"::: )  ; 

cluster   ($#v1_xboole_0 :::"zero"::: )     ($#v1_xcmplx_0 :::"complex"::: )     ($#v1_xxreal_0 :::"ext-real"::: )     ($#v1_xreal_0 :::"real"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; registrationlet "r", "s" be  ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )    ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set "r"  ($#k2_xcmplx_0 :::"+"::: )  "s") ->  ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )  ; 
end; registrationlet "r", "s" be  ($#~v2_xxreal_0  "non"   ($#v2_xxreal_0 :::"positive"::: )   )    ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set "r"  ($#k2_xcmplx_0 :::"+"::: )  "s") ->  ($#~v2_xxreal_0  "non"   ($#v2_xxreal_0 :::"positive"::: )   )  ; 
end; registrationlet "r" be   ($#v2_xxreal_0 :::"positive"::: )     ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; let "s" be  ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )    ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set "r"  ($#k2_xcmplx_0 :::"+"::: )  "s") ->   ($#v2_xxreal_0 :::"positive"::: )   ; 

cluster (Set "s"  ($#k2_xcmplx_0 :::"+"::: )  "r") ->   ($#v2_xxreal_0 :::"positive"::: )   ; 
end; registrationlet "r" be   ($#v3_xxreal_0 :::"negative"::: )     ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; let "s" be  ($#~v2_xxreal_0  "non"   ($#v2_xxreal_0 :::"positive"::: )   )    ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set "r"  ($#k2_xcmplx_0 :::"+"::: )  "s") ->   ($#v3_xxreal_0 :::"negative"::: )   ; 

cluster (Set "s"  ($#k2_xcmplx_0 :::"+"::: )  "r") ->   ($#v3_xxreal_0 :::"negative"::: )   ; 
end; registrationlet "r" be  ($#~v2_xxreal_0  "non"   ($#v2_xxreal_0 :::"positive"::: )   )    ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set   ($#k4_xcmplx_0 :::"-"::: )  "r") ->  ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )  ; 
end; registrationlet "r" be  ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )    ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set   ($#k4_xcmplx_0 :::"-"::: )  "r") ->  ($#~v2_xxreal_0  "non"   ($#v2_xxreal_0 :::"positive"::: )   )  ; 
end; registrationlet "r" be  ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )    ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; let "s" be  ($#~v2_xxreal_0  "non"   ($#v2_xxreal_0 :::"positive"::: )   )    ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set "r"  ($#k6_xcmplx_0 :::"-"::: )  "s") ->  ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )  ; 

cluster (Set "s"  ($#k6_xcmplx_0 :::"-"::: )  "r") ->  ($#~v2_xxreal_0  "non"   ($#v2_xxreal_0 :::"positive"::: )   )  ; 
end; registrationlet "r" be   ($#v2_xxreal_0 :::"positive"::: )     ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; let "s" be  ($#~v2_xxreal_0  "non"   ($#v2_xxreal_0 :::"positive"::: )   )    ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set "r"  ($#k6_xcmplx_0 :::"-"::: )  "s") ->   ($#v2_xxreal_0 :::"positive"::: )   ; 

cluster (Set "s"  ($#k6_xcmplx_0 :::"-"::: )  "r") ->   ($#v3_xxreal_0 :::"negative"::: )   ; 
end; registrationlet "r" be   ($#v3_xxreal_0 :::"negative"::: )     ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; let "s" be  ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )    ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set "r"  ($#k6_xcmplx_0 :::"-"::: )  "s") ->   ($#v3_xxreal_0 :::"negative"::: )   ; 

cluster (Set "s"  ($#k6_xcmplx_0 :::"-"::: )  "r") ->   ($#v2_xxreal_0 :::"positive"::: )   ; 
end; registrationlet "r" be  ($#~v2_xxreal_0  "non"   ($#v2_xxreal_0 :::"positive"::: )   )    ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; let "s" be  ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )    ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set "r"  ($#k3_xcmplx_0 :::"*"::: )  "s") ->  ($#~v2_xxreal_0  "non"   ($#v2_xxreal_0 :::"positive"::: )   )  ; 

cluster (Set "s"  ($#k3_xcmplx_0 :::"*"::: )  "r") ->  ($#~v2_xxreal_0  "non"   ($#v2_xxreal_0 :::"positive"::: )   )  ; 
end; registrationlet "r", "s" be  ($#~v2_xxreal_0  "non"   ($#v2_xxreal_0 :::"positive"::: )   )    ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set "r"  ($#k3_xcmplx_0 :::"*"::: )  "s") ->  ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )  ; 
end; registrationlet "r", "s" be  ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )    ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set "r"  ($#k3_xcmplx_0 :::"*"::: )  "s") ->  ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )  ; 
end; registrationlet "r" be   ($#v2_xxreal_0 :::"positive"::: )     ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set "r"  ($#k5_xcmplx_0 :::"""::: )  ) ->   ($#v2_xxreal_0 :::"positive"::: )   ; 
end; registrationlet "r" be  ($#~v2_xxreal_0  "non"   ($#v2_xxreal_0 :::"positive"::: )   )    ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set "r"  ($#k5_xcmplx_0 :::"""::: )  ) ->  ($#~v2_xxreal_0  "non"   ($#v2_xxreal_0 :::"positive"::: )   )  ; 
end; registrationlet "r" be   ($#v3_xxreal_0 :::"negative"::: )     ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set "r"  ($#k5_xcmplx_0 :::"""::: )  ) ->   ($#v3_xxreal_0 :::"negative"::: )   ; 
end; registrationlet "r" be  ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )    ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set "r"  ($#k5_xcmplx_0 :::"""::: )  ) ->  ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )  ; 
end; registrationlet "r" be  ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )    ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; let "s" be  ($#~v2_xxreal_0  "non"   ($#v2_xxreal_0 :::"positive"::: )   )    ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set "r"  ($#k7_xcmplx_0 :::"/"::: )  "s") ->  ($#~v2_xxreal_0  "non"   ($#v2_xxreal_0 :::"positive"::: )   )  ; 

cluster (Set "s"  ($#k7_xcmplx_0 :::"/"::: )  "r") ->  ($#~v2_xxreal_0  "non"   ($#v2_xxreal_0 :::"positive"::: )   )  ; 
end; registrationlet "r", "s" be  ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )    ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set "r"  ($#k7_xcmplx_0 :::"/"::: )  "s") ->  ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )  ; 
end; registrationlet "r", "s" be  ($#~v2_xxreal_0  "non"   ($#v2_xxreal_0 :::"positive"::: )   )    ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set "r"  ($#k7_xcmplx_0 :::"/"::: )  "s") ->  ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )  ; 
end; begin  registrationlet "r", "s" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set   ($#k3_xxreal_0 :::"min"::: )   "(" "r" "," "s" ")" ) ->   ($#v1_xreal_0 :::"real"::: )   ; 

cluster (Set   ($#k4_xxreal_0 :::"max"::: )   "(" "r" "," "s" ")" ) ->   ($#v1_xreal_0 :::"real"::: )   ; 
end; definitionlet "r", "s" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; func "r" :::"-'"::: "s" ->    ($#m1_hidden :::"set"::: )   equals :: XREAL_0:def 2 (Set "r"  ($#k6_xcmplx_0 :::"-"::: )  "s") if (Bool (Set "r"  ($#k6_xcmplx_0 :::"-"::: )  "s")  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  otherwise (Set   ($#k6_numbers :::"0"::: )  ); end; 






:: deftheorem    defines :::"-'"::: XREAL_0:def 2 :  (Bool  "for" (Set (Var "r")) "," (Set (Var "s")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("   "("  (Bool (Bool (Set (Set (Var "r"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "s")))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool (Set (Set (Var "r"))  ($#k1_xreal_0 :::"-'"::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "s"))))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Set (Var "r"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "s")))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )))) "implies" (Bool (Set (Set (Var "r"))  ($#k1_xreal_0 :::"-'"::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")"   ")" )); 
 registrationlet "r", "s" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set "r"  ($#k1_xreal_0 :::"-'"::: )  "s") ->   ($#v1_xreal_0 :::"real"::: )   ; 
end; registrationlet "r", "s" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set "r"  ($#k1_xreal_0 :::"-'"::: )  "s") ->  ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )    ($#v1_xreal_0 :::"real"::: )    for  ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
end;