:: NUMBERS semantic presentation begin notationsynonym :::"NAT"::: for :::"omega"::: ; synonym :::"0"::: for :::"{}"::: ; end; definitionfunc :::"REAL"::: -> ($#m1_hidden :::"set"::: ) equals :: NUMBERS:def 1 (Set (Set "(" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k1_xboole_0 :::"0"::: ) ) "," (Set ($#k1_xboole_0 :::"0"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) )); end; :: deftheorem defines :::"REAL"::: NUMBERS:def 1 : (Bool (Set ($#k1_numbers :::"REAL"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k1_xboole_0 :::"0"::: ) ) "," (Set ($#k1_xboole_0 :::"0"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ))); registration cluster (Set ($#k1_numbers :::"REAL"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionfunc :::"COMPLEX"::: -> ($#m1_hidden :::"set"::: ) equals :: NUMBERS:def 2 (Set (Set "(" (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set ($#k2_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"0"::: ) ) "," (Num 1) ($#k2_tarski :::"}"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ")" ) ($#k6_subset_1 :::"\"::: ) "{" (Set (Var "x")) where x "is" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set ($#k2_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"0"::: ) ) "," (Num 1) ($#k2_tarski :::"}"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) : (Bool (Set (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"0"::: ) )) "}" ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_numbers :::"REAL"::: ) )); func :::"RAT"::: -> ($#m1_hidden :::"set"::: ) equals :: NUMBERS:def 3 (Set (Set "(" (Set ($#k5_arytm_3 :::"RAT+"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k5_arytm_3 :::"RAT+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k1_xboole_0 :::"0"::: ) ) "," (Set ($#k1_xboole_0 :::"0"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) )); func :::"INT"::: -> ($#m1_hidden :::"set"::: ) equals :: NUMBERS:def 4 (Set (Set "(" (Set ($#k4_ordinal1 :::"NAT"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k4_ordinal1 :::"NAT"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k1_xboole_0 :::"0"::: ) ) "," (Set ($#k1_xboole_0 :::"0"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) )); :: original: :::"NAT"::: redefine func :::"NAT"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ); end; :: deftheorem defines :::"COMPLEX"::: NUMBERS:def 2 : (Bool (Set ($#k2_numbers :::"COMPLEX"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set ($#k2_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"0"::: ) ) "," (Num 1) ($#k2_tarski :::"}"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ")" ) ($#k6_subset_1 :::"\"::: ) "{" (Set (Var "x")) where x "is" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set ($#k2_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"0"::: ) ) "," (Num 1) ($#k2_tarski :::"}"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) : (Bool (Set (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"0"::: ) )) "}" ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_numbers :::"REAL"::: ) ))); :: deftheorem defines :::"RAT"::: NUMBERS:def 3 : (Bool (Set ($#k3_numbers :::"RAT"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k5_arytm_3 :::"RAT+"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k5_arytm_3 :::"RAT+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k1_xboole_0 :::"0"::: ) ) "," (Set ($#k1_xboole_0 :::"0"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ))); :: deftheorem defines :::"INT"::: NUMBERS:def 4 : (Bool (Set ($#k4_numbers :::"INT"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k4_ordinal1 :::"NAT"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k4_ordinal1 :::"NAT"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k1_xboole_0 :::"0"::: ) ) "," (Set ($#k1_xboole_0 :::"0"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ))); registration cluster (Set ($#k2_numbers :::"COMPLEX"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; cluster (Set ($#k3_numbers :::"RAT"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; cluster (Set ($#k4_numbers :::"INT"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definition:: original: :::"0"::: redefine func :::"0"::: -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); end; theorem :: NUMBERS:1 (Bool (Set ($#k1_numbers :::"REAL"::: ) ) ($#r2_xboole_0 :::"c<"::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) )) ; theorem :: NUMBERS:2 (Bool (Set ($#k3_numbers :::"RAT"::: ) ) ($#r2_xboole_0 :::"c<"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) ; theorem :: NUMBERS:3 (Bool (Set ($#k3_numbers :::"RAT"::: ) ) ($#r2_xboole_0 :::"c<"::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) )) ; theorem :: NUMBERS:4 (Bool (Set ($#k4_numbers :::"INT"::: ) ) ($#r2_xboole_0 :::"c<"::: ) (Set ($#k3_numbers :::"RAT"::: ) )) ; theorem :: NUMBERS:5 (Bool (Set ($#k4_numbers :::"INT"::: ) ) ($#r2_xboole_0 :::"c<"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) ; theorem :: NUMBERS:6 (Bool (Set ($#k4_numbers :::"INT"::: ) ) ($#r2_xboole_0 :::"c<"::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) )) ; theorem :: NUMBERS:7 (Bool (Set ($#k5_numbers :::"NAT"::: ) ) ($#r2_xboole_0 :::"c<"::: ) (Set ($#k4_numbers :::"INT"::: ) )) ; theorem :: NUMBERS:8 (Bool (Set ($#k5_numbers :::"NAT"::: ) ) ($#r2_xboole_0 :::"c<"::: ) (Set ($#k3_numbers :::"RAT"::: ) )) ; theorem :: NUMBERS:9 (Bool (Set ($#k5_numbers :::"NAT"::: ) ) ($#r2_xboole_0 :::"c<"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) ; theorem :: NUMBERS:10 (Bool (Set ($#k5_numbers :::"NAT"::: ) ) ($#r2_xboole_0 :::"c<"::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) )) ; begin theorem :: NUMBERS:11 (Bool (Set ($#k1_numbers :::"REAL"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) )) ; theorem :: NUMBERS:12 (Bool (Set ($#k3_numbers :::"RAT"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k1_numbers :::"REAL"::: ) )) ; theorem :: NUMBERS:13 (Bool (Set ($#k3_numbers :::"RAT"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) )) ; theorem :: NUMBERS:14 (Bool (Set ($#k4_numbers :::"INT"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k3_numbers :::"RAT"::: ) )) ; theorem :: NUMBERS:15 (Bool (Set ($#k4_numbers :::"INT"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k1_numbers :::"REAL"::: ) )) ; theorem :: NUMBERS:16 (Bool (Set ($#k4_numbers :::"INT"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) )) ; theorem :: NUMBERS:17 (Bool (Set ($#k5_numbers :::"NAT"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k4_numbers :::"INT"::: ) )) ; theorem :: NUMBERS:18 (Bool (Set ($#k5_numbers :::"NAT"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k3_numbers :::"RAT"::: ) )) ; theorem :: NUMBERS:19 (Bool (Set ($#k5_numbers :::"NAT"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k1_numbers :::"REAL"::: ) )) ; theorem :: NUMBERS:20 (Bool (Set ($#k5_numbers :::"NAT"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) )) ; theorem :: NUMBERS:21 (Bool (Set ($#k1_numbers :::"REAL"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) )) ; theorem :: NUMBERS:22 (Bool (Set ($#k3_numbers :::"RAT"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) ; theorem :: NUMBERS:23 (Bool (Set ($#k3_numbers :::"RAT"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) )) ; theorem :: NUMBERS:24 (Bool (Set ($#k4_numbers :::"INT"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k3_numbers :::"RAT"::: ) )) ; theorem :: NUMBERS:25 (Bool (Set ($#k4_numbers :::"INT"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) ; theorem :: NUMBERS:26 (Bool (Set ($#k4_numbers :::"INT"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) )) ; theorem :: NUMBERS:27 (Bool (Set ($#k5_numbers :::"NAT"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k4_numbers :::"INT"::: ) )) ; theorem :: NUMBERS:28 (Bool (Set ($#k5_numbers :::"NAT"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k3_numbers :::"RAT"::: ) )) ; theorem :: NUMBERS:29 (Bool (Set ($#k5_numbers :::"NAT"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) ; theorem :: NUMBERS:30 (Bool (Set ($#k5_numbers :::"NAT"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) )) ; definitionfunc :::"ExtREAL"::: -> ($#m1_hidden :::"set"::: ) equals :: NUMBERS:def 5 (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_tarski :::"{"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k2_tarski :::"}"::: ) )); end; :: deftheorem defines :::"ExtREAL"::: NUMBERS:def 5 : (Bool (Set ($#k7_numbers :::"ExtREAL"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_tarski :::"{"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k2_tarski :::"}"::: ) ))); registration cluster (Set ($#k7_numbers :::"ExtREAL"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: NUMBERS:31 (Bool (Set ($#k1_numbers :::"REAL"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k7_numbers :::"ExtREAL"::: ) )) ; theorem :: NUMBERS:32 (Bool (Set ($#k1_numbers :::"REAL"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k7_numbers :::"ExtREAL"::: ) )) ; theorem :: NUMBERS:33 (Bool (Set ($#k1_numbers :::"REAL"::: ) ) ($#r2_xboole_0 :::"c<"::: ) (Set ($#k7_numbers :::"ExtREAL"::: ) )) ; registration cluster (Set ($#k4_numbers :::"INT"::: ) ) -> ($#v1_finset_1 :::"infinite"::: ) ; cluster (Set ($#k3_numbers :::"RAT"::: ) ) -> ($#v1_finset_1 :::"infinite"::: ) ; cluster (Set ($#k1_numbers :::"REAL"::: ) ) -> ($#v1_finset_1 :::"infinite"::: ) ; cluster (Set ($#k2_numbers :::"COMPLEX"::: ) ) -> ($#v1_finset_1 :::"infinite"::: ) ; end;