:: BINOP_2 semantic presentation begin scheme :: BINOP_2:sch 1 FuncDefUniq{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3( ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" )) -> ($#m1_hidden :::"set"::: ) } : (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool (Set (Set (Var "f1")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "x")) ")" )) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool (Set (Set (Var "f2")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "x")) ")" )) ")" )) "holds" (Bool (Set (Var "f1")) ($#r2_funct_2 :::"="::: ) (Set (Var "f2")))) proof end; scheme :: BINOP_2:sch 2 BinOpDefuniq{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2( ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "," ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" )) -> ($#m1_hidden :::"set"::: ) } : (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set F1 "(" ")" ) "st" (Bool (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool (Set (Set (Var "o1")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set F2 "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool (Set (Set (Var "o2")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set F2 "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) ")" )) "holds" (Bool (Set (Var "o1")) ($#r8_binop_1 :::"="::: ) (Set (Var "o2")))) proof end; scheme :: BINOP_2:sch 3 CFuncDefUniq{ F1( ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "f1")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set F1 "(" (Set (Var "x")) ")" )) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "f2")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set F1 "(" (Set (Var "x")) ")" )) ")" )) "holds" (Bool (Set (Var "f1")) ($#r2_funct_2 :::"="::: ) (Set (Var "f2")))) proof end; scheme :: BINOP_2:sch 4 RFuncDefUniq{ F1( ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "f1")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set F1 "(" (Set (Var "x")) ")" )) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "f2")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set F1 "(" (Set (Var "x")) ")" )) ")" )) "holds" (Bool (Set (Var "f1")) ($#r2_funct_2 :::"="::: ) (Set (Var "f2")))) proof end; registration cluster -> ($#v1_rat_1 :::"rational"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_numbers :::"RAT"::: ) ); end; scheme :: BINOP_2:sch 5 WFuncDefUniq{ F1( ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k3_numbers :::"RAT"::: ) ) "," (Set ($#k3_numbers :::"RAT"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "f1")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set F1 "(" (Set (Var "x")) ")" )) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "f2")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set F1 "(" (Set (Var "x")) ")" )) ")" )) "holds" (Bool (Set (Var "f1")) ($#r2_funct_2 :::"="::: ) (Set (Var "f2")))) proof end; scheme :: BINOP_2:sch 6 IFuncDefUniq{ F1( ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k4_numbers :::"INT"::: ) ) "," (Set ($#k4_numbers :::"INT"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "f1")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set F1 "(" (Set (Var "x")) ")" )) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "f2")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set F1 "(" (Set (Var "x")) ")" )) ")" )) "holds" (Bool (Set (Var "f1")) ($#r2_funct_2 :::"="::: ) (Set (Var "f2")))) proof end; scheme :: BINOP_2:sch 7 NFuncDefUniq{ F1( ($#m1_hidden :::"Nat":::)) -> ($#m1_hidden :::"set"::: ) } : (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "f1")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set F1 "(" (Set (Var "x")) ")" )) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "f2")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set F1 "(" (Set (Var "x")) ")" )) ")" )) "holds" (Bool (Set (Var "f1")) ($#r2_funct_2 :::"="::: ) (Set (Var "f2")))) proof end; scheme :: BINOP_2:sch 8 CBinOpDefuniq{ F1( ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "," ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "o1")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set F1 "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "o2")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set F1 "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) ")" )) "holds" (Bool (Set (Var "o1")) ($#r8_binop_1 :::"="::: ) (Set (Var "o2")))) proof end; scheme :: BINOP_2:sch 9 RBinOpDefuniq{ F1( ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "," ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "o1")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set F1 "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "o2")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set F1 "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) ")" )) "holds" (Bool (Set (Var "o1")) ($#r8_binop_1 :::"="::: ) (Set (Var "o2")))) proof end; scheme :: BINOP_2:sch 10 WBinOpDefuniq{ F1( ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) "," ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k3_numbers :::"RAT"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "o1")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set F1 "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "o2")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set F1 "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) ")" )) "holds" (Bool (Set (Var "o1")) ($#r8_binop_1 :::"="::: ) (Set (Var "o2")))) proof end; scheme :: BINOP_2:sch 11 IBinOpDefuniq{ F1( ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) "," ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k4_numbers :::"INT"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "o1")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set F1 "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "o2")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set F1 "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) ")" )) "holds" (Bool (Set (Var "o1")) ($#r8_binop_1 :::"="::: ) (Set (Var "o2")))) proof end; scheme :: BINOP_2:sch 12 NBinOpDefuniq{ F1( ($#m1_hidden :::"Nat":::) "," ($#m1_hidden :::"Nat":::)) -> ($#m1_hidden :::"set"::: ) } : (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "o1")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set F1 "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "o2")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set F1 "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) ")" )) "holds" (Bool (Set (Var "o1")) ($#r8_binop_1 :::"="::: ) (Set (Var "o2")))) proof end; scheme :: BINOP_2:sch 13 CLambda2D{ F1( ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "," ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ) -> ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "f")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set F1 "(" (Set (Var "x")) "," (Set (Var "y")) ")" )))) proof end; scheme :: BINOP_2:sch 14 RLambda2D{ F1( ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "," ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ) -> ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "f")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set F1 "(" (Set (Var "x")) "," (Set (Var "y")) ")" )))) proof end; scheme :: BINOP_2:sch 15 WLambda2D{ F1( ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) "," ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) ) -> ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k3_numbers :::"RAT"::: ) ) "," (Set ($#k3_numbers :::"RAT"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k3_numbers :::"RAT"::: ) ) "st" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "f")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set F1 "(" (Set (Var "x")) "," (Set (Var "y")) ")" )))) proof end; scheme :: BINOP_2:sch 16 ILambda2D{ F1( ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) "," ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) ) -> ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k4_numbers :::"INT"::: ) ) "," (Set ($#k4_numbers :::"INT"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k4_numbers :::"INT"::: ) ) "st" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "f")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set F1 "(" (Set (Var "x")) "," (Set (Var "y")) ")" )))) proof end; scheme :: BINOP_2:sch 17 NLambda2D{ F1( ($#m1_hidden :::"Nat":::) "," ($#m1_hidden :::"Nat":::)) -> ($#m1_hidden :::"Nat":::) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k5_numbers :::"NAT"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "f")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set F1 "(" (Set (Var "x")) "," (Set (Var "y")) ")" )))) proof end; scheme :: BINOP_2:sch 18 CLambdaD{ F1( ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ) -> ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool "for" (Set (Var "x")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set F1 "(" (Set (Var "x")) ")" )))) proof end; scheme :: BINOP_2:sch 19 RLambdaD{ F1( ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ) -> ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set F1 "(" (Set (Var "x")) ")" )))) proof end; scheme :: BINOP_2:sch 20 WLambdaD{ F1( ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) ) -> ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k3_numbers :::"RAT"::: ) ) "," (Set ($#k3_numbers :::"RAT"::: ) ) "st" (Bool "for" (Set (Var "x")) "being" ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set F1 "(" (Set (Var "x")) ")" )))) proof end; scheme :: BINOP_2:sch 21 ILambdaD{ F1( ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) ) -> ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k4_numbers :::"INT"::: ) ) "," (Set ($#k4_numbers :::"INT"::: ) ) "st" (Bool "for" (Set (Var "x")) "being" ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set F1 "(" (Set (Var "x")) ")" )))) proof end; scheme :: BINOP_2:sch 22 NLambdaD{ F1( ($#m1_hidden :::"Nat":::)) -> ($#m1_hidden :::"Nat":::) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set F1 "(" (Set (Var "x")) ")" )))) proof end; definitionlet "c1" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"-"::: redefine func :::"-"::: "c1" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ); :: original: :::"""::: redefine func "c1" :::"""::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ); let "c2" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"+"::: redefine func "c1" :::"+"::: "c2" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ); :: original: :::"-"::: redefine func "c1" :::"-"::: "c2" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ); :: original: :::"*"::: redefine func "c1" :::"*"::: "c2" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ); :: original: :::"/"::: redefine func "c1" :::"/"::: "c2" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ); end; definitionlet "r1" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"-"::: redefine func :::"-"::: "r1" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ); :: original: :::"""::: redefine func "r1" :::"""::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ); let "r2" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"+"::: redefine func "r1" :::"+"::: "r2" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ); :: original: :::"-"::: redefine func "r1" :::"-"::: "r2" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ); :: original: :::"*"::: redefine func "r1" :::"*"::: "r2" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ); :: original: :::"/"::: redefine func "r1" :::"/"::: "r2" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ); end; definitionlet "w1" be ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"-"::: redefine func :::"-"::: "w1" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_numbers :::"RAT"::: ) ); :: original: :::"""::: redefine func "w1" :::"""::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_numbers :::"RAT"::: ) ); let "w2" be ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"+"::: redefine func "w1" :::"+"::: "w2" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_numbers :::"RAT"::: ) ); :: original: :::"-"::: redefine func "w1" :::"-"::: "w2" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_numbers :::"RAT"::: ) ); :: original: :::"*"::: redefine func "w1" :::"*"::: "w2" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_numbers :::"RAT"::: ) ); :: original: :::"/"::: redefine func "w1" :::"/"::: "w2" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_numbers :::"RAT"::: ) ); end; definitionlet "i1" be ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"-"::: redefine func :::"-"::: "i1" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ); let "i2" be ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"+"::: redefine func "i1" :::"+"::: "i2" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ); :: original: :::"-"::: redefine func "i1" :::"-"::: "i2" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ); :: original: :::"*"::: redefine func "i1" :::"*"::: "i2" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ); end; definitionlet "n1", "n2" be ($#m1_hidden :::"Nat":::); :: original: :::"+"::: redefine func "n1" :::"+"::: "n2" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); :: original: :::"*"::: redefine func "n1" :::"*"::: "n2" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); end; definitionfunc :::"compcomplex"::: -> ($#m1_subset_1 :::"UnOp":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) means :: BINOP_2:def 1 (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set ($#k1_binop_2 :::"-"::: ) (Set (Var "c"))))); func :::"invcomplex"::: -> ($#m1_subset_1 :::"UnOp":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) means :: BINOP_2:def 2 (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "c")) ($#k2_binop_2 :::"""::: ) ))); func :::"addcomplex"::: -> ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) means :: BINOP_2:def 3 (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set it ($#k1_binop_1 :::"."::: ) "(" (Set (Var "c1")) "," (Set (Var "c2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "c1")) ($#k3_binop_2 :::"+"::: ) (Set (Var "c2"))))); func :::"diffcomplex"::: -> ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) means :: BINOP_2:def 4 (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set it ($#k1_binop_1 :::"."::: ) "(" (Set (Var "c1")) "," (Set (Var "c2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "c1")) ($#k4_binop_2 :::"-"::: ) (Set (Var "c2"))))); func :::"multcomplex"::: -> ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) means :: BINOP_2:def 5 (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set it ($#k1_binop_1 :::"."::: ) "(" (Set (Var "c1")) "," (Set (Var "c2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "c1")) ($#k5_binop_2 :::"*"::: ) (Set (Var "c2"))))); func :::"divcomplex"::: -> ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) means :: BINOP_2:def 6 (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set it ($#k1_binop_1 :::"."::: ) "(" (Set (Var "c1")) "," (Set (Var "c2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "c1")) ($#k6_binop_2 :::"/"::: ) (Set (Var "c2"))))); end; :: deftheorem defines :::"compcomplex"::: BINOP_2:def 1 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k25_binop_2 :::"compcomplex"::: ) )) "iff" (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set ($#k1_binop_2 :::"-"::: ) (Set (Var "c"))))) ")" )); :: deftheorem defines :::"invcomplex"::: BINOP_2:def 2 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k26_binop_2 :::"invcomplex"::: ) )) "iff" (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "c")) ($#k2_binop_2 :::"""::: ) ))) ")" )); :: deftheorem defines :::"addcomplex"::: BINOP_2:def 3 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k27_binop_2 :::"addcomplex"::: ) )) "iff" (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "c1")) "," (Set (Var "c2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "c1")) ($#k3_binop_2 :::"+"::: ) (Set (Var "c2"))))) ")" )); :: deftheorem defines :::"diffcomplex"::: BINOP_2:def 4 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k28_binop_2 :::"diffcomplex"::: ) )) "iff" (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "c1")) "," (Set (Var "c2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "c1")) ($#k4_binop_2 :::"-"::: ) (Set (Var "c2"))))) ")" )); :: deftheorem defines :::"multcomplex"::: BINOP_2:def 5 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k29_binop_2 :::"multcomplex"::: ) )) "iff" (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "c1")) "," (Set (Var "c2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "c1")) ($#k5_binop_2 :::"*"::: ) (Set (Var "c2"))))) ")" )); :: deftheorem defines :::"divcomplex"::: BINOP_2:def 6 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k30_binop_2 :::"divcomplex"::: ) )) "iff" (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "c1")) "," (Set (Var "c2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "c1")) ($#k6_binop_2 :::"/"::: ) (Set (Var "c2"))))) ")" )); definitionfunc :::"compreal"::: -> ($#m1_subset_1 :::"UnOp":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) means :: BINOP_2:def 7 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set ($#k7_binop_2 :::"-"::: ) (Set (Var "r"))))); func :::"invreal"::: -> ($#m1_subset_1 :::"UnOp":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) means :: BINOP_2:def 8 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k8_binop_2 :::"""::: ) ))); func :::"addreal"::: -> ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) means :: BINOP_2:def 9 (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set it ($#k1_binop_1 :::"."::: ) "(" (Set (Var "r1")) "," (Set (Var "r2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "r1")) ($#k9_binop_2 :::"+"::: ) (Set (Var "r2"))))); func :::"diffreal"::: -> ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) means :: BINOP_2:def 10 (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set it ($#k1_binop_1 :::"."::: ) "(" (Set (Var "r1")) "," (Set (Var "r2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "r1")) ($#k10_binop_2 :::"-"::: ) (Set (Var "r2"))))); func :::"multreal"::: -> ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) means :: BINOP_2:def 11 (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set it ($#k1_binop_1 :::"."::: ) "(" (Set (Var "r1")) "," (Set (Var "r2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "r1")) ($#k11_binop_2 :::"*"::: ) (Set (Var "r2"))))); func :::"divreal"::: -> ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) means :: BINOP_2:def 12 (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set it ($#k1_binop_1 :::"."::: ) "(" (Set (Var "r1")) "," (Set (Var "r2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "r1")) ($#k12_binop_2 :::"/"::: ) (Set (Var "r2"))))); end; :: deftheorem defines :::"compreal"::: BINOP_2:def 7 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k31_binop_2 :::"compreal"::: ) )) "iff" (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set ($#k7_binop_2 :::"-"::: ) (Set (Var "r"))))) ")" )); :: deftheorem defines :::"invreal"::: BINOP_2:def 8 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k32_binop_2 :::"invreal"::: ) )) "iff" (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k8_binop_2 :::"""::: ) ))) ")" )); :: deftheorem defines :::"addreal"::: BINOP_2:def 9 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k33_binop_2 :::"addreal"::: ) )) "iff" (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "r1")) "," (Set (Var "r2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "r1")) ($#k9_binop_2 :::"+"::: ) (Set (Var "r2"))))) ")" )); :: deftheorem defines :::"diffreal"::: BINOP_2:def 10 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k34_binop_2 :::"diffreal"::: ) )) "iff" (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "r1")) "," (Set (Var "r2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "r1")) ($#k10_binop_2 :::"-"::: ) (Set (Var "r2"))))) ")" )); :: deftheorem defines :::"multreal"::: BINOP_2:def 11 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k35_binop_2 :::"multreal"::: ) )) "iff" (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "r1")) "," (Set (Var "r2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "r1")) ($#k11_binop_2 :::"*"::: ) (Set (Var "r2"))))) ")" )); :: deftheorem defines :::"divreal"::: BINOP_2:def 12 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k36_binop_2 :::"divreal"::: ) )) "iff" (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "r1")) "," (Set (Var "r2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "r1")) ($#k12_binop_2 :::"/"::: ) (Set (Var "r2"))))) ")" )); definitionfunc :::"comprat"::: -> ($#m1_subset_1 :::"UnOp":::) "of" (Set ($#k3_numbers :::"RAT"::: ) ) means :: BINOP_2:def 13 (Bool "for" (Set (Var "w")) "being" ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Set ($#k13_binop_2 :::"-"::: ) (Set (Var "w"))))); func :::"invrat"::: -> ($#m1_subset_1 :::"UnOp":::) "of" (Set ($#k3_numbers :::"RAT"::: ) ) means :: BINOP_2:def 14 (Bool "for" (Set (Var "w")) "being" ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "w")) ($#k14_binop_2 :::"""::: ) ))); func :::"addrat"::: -> ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k3_numbers :::"RAT"::: ) ) means :: BINOP_2:def 15 (Bool "for" (Set (Var "w1")) "," (Set (Var "w2")) "being" ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set it ($#k1_binop_1 :::"."::: ) "(" (Set (Var "w1")) "," (Set (Var "w2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "w1")) ($#k15_binop_2 :::"+"::: ) (Set (Var "w2"))))); func :::"diffrat"::: -> ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k3_numbers :::"RAT"::: ) ) means :: BINOP_2:def 16 (Bool "for" (Set (Var "w1")) "," (Set (Var "w2")) "being" ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set it ($#k1_binop_1 :::"."::: ) "(" (Set (Var "w1")) "," (Set (Var "w2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "w1")) ($#k16_binop_2 :::"-"::: ) (Set (Var "w2"))))); func :::"multrat"::: -> ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k3_numbers :::"RAT"::: ) ) means :: BINOP_2:def 17 (Bool "for" (Set (Var "w1")) "," (Set (Var "w2")) "being" ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set it ($#k1_binop_1 :::"."::: ) "(" (Set (Var "w1")) "," (Set (Var "w2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "w1")) ($#k17_binop_2 :::"*"::: ) (Set (Var "w2"))))); func :::"divrat"::: -> ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k3_numbers :::"RAT"::: ) ) means :: BINOP_2:def 18 (Bool "for" (Set (Var "w1")) "," (Set (Var "w2")) "being" ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set it ($#k1_binop_1 :::"."::: ) "(" (Set (Var "w1")) "," (Set (Var "w2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "w1")) ($#k18_binop_2 :::"/"::: ) (Set (Var "w2"))))); end; :: deftheorem defines :::"comprat"::: BINOP_2:def 13 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set ($#k3_numbers :::"RAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k37_binop_2 :::"comprat"::: ) )) "iff" (Bool "for" (Set (Var "w")) "being" ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Set ($#k13_binop_2 :::"-"::: ) (Set (Var "w"))))) ")" )); :: deftheorem defines :::"invrat"::: BINOP_2:def 14 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set ($#k3_numbers :::"RAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k38_binop_2 :::"invrat"::: ) )) "iff" (Bool "for" (Set (Var "w")) "being" ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "w")) ($#k14_binop_2 :::"""::: ) ))) ")" )); :: deftheorem defines :::"addrat"::: BINOP_2:def 15 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k3_numbers :::"RAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k39_binop_2 :::"addrat"::: ) )) "iff" (Bool "for" (Set (Var "w1")) "," (Set (Var "w2")) "being" ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "w1")) "," (Set (Var "w2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "w1")) ($#k15_binop_2 :::"+"::: ) (Set (Var "w2"))))) ")" )); :: deftheorem defines :::"diffrat"::: BINOP_2:def 16 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k3_numbers :::"RAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k40_binop_2 :::"diffrat"::: ) )) "iff" (Bool "for" (Set (Var "w1")) "," (Set (Var "w2")) "being" ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "w1")) "," (Set (Var "w2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "w1")) ($#k16_binop_2 :::"-"::: ) (Set (Var "w2"))))) ")" )); :: deftheorem defines :::"multrat"::: BINOP_2:def 17 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k3_numbers :::"RAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k41_binop_2 :::"multrat"::: ) )) "iff" (Bool "for" (Set (Var "w1")) "," (Set (Var "w2")) "being" ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "w1")) "," (Set (Var "w2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "w1")) ($#k17_binop_2 :::"*"::: ) (Set (Var "w2"))))) ")" )); :: deftheorem defines :::"divrat"::: BINOP_2:def 18 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k3_numbers :::"RAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k42_binop_2 :::"divrat"::: ) )) "iff" (Bool "for" (Set (Var "w1")) "," (Set (Var "w2")) "being" ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "w1")) "," (Set (Var "w2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "w1")) ($#k18_binop_2 :::"/"::: ) (Set (Var "w2"))))) ")" )); definitionfunc :::"compint"::: -> ($#m1_subset_1 :::"UnOp":::) "of" (Set ($#k4_numbers :::"INT"::: ) ) means :: BINOP_2:def 19 (Bool "for" (Set (Var "i")) "being" ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k19_binop_2 :::"-"::: ) (Set (Var "i"))))); func :::"addint"::: -> ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k4_numbers :::"INT"::: ) ) means :: BINOP_2:def 20 (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "being" ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set it ($#k1_binop_1 :::"."::: ) "(" (Set (Var "i1")) "," (Set (Var "i2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "i1")) ($#k20_binop_2 :::"+"::: ) (Set (Var "i2"))))); func :::"diffint"::: -> ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k4_numbers :::"INT"::: ) ) means :: BINOP_2:def 21 (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "being" ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set it ($#k1_binop_1 :::"."::: ) "(" (Set (Var "i1")) "," (Set (Var "i2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "i1")) ($#k21_binop_2 :::"-"::: ) (Set (Var "i2"))))); func :::"multint"::: -> ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k4_numbers :::"INT"::: ) ) means :: BINOP_2:def 22 (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "being" ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set it ($#k1_binop_1 :::"."::: ) "(" (Set (Var "i1")) "," (Set (Var "i2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "i1")) ($#k22_binop_2 :::"*"::: ) (Set (Var "i2"))))); end; :: deftheorem defines :::"compint"::: BINOP_2:def 19 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set ($#k4_numbers :::"INT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k43_binop_2 :::"compint"::: ) )) "iff" (Bool "for" (Set (Var "i")) "being" ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k19_binop_2 :::"-"::: ) (Set (Var "i"))))) ")" )); :: deftheorem defines :::"addint"::: BINOP_2:def 20 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k4_numbers :::"INT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k44_binop_2 :::"addint"::: ) )) "iff" (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "being" ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "i1")) "," (Set (Var "i2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "i1")) ($#k20_binop_2 :::"+"::: ) (Set (Var "i2"))))) ")" )); :: deftheorem defines :::"diffint"::: BINOP_2:def 21 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k4_numbers :::"INT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k45_binop_2 :::"diffint"::: ) )) "iff" (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "being" ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "i1")) "," (Set (Var "i2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "i1")) ($#k21_binop_2 :::"-"::: ) (Set (Var "i2"))))) ")" )); :: deftheorem defines :::"multint"::: BINOP_2:def 22 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k4_numbers :::"INT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k46_binop_2 :::"multint"::: ) )) "iff" (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "being" ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "i1")) "," (Set (Var "i2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "i1")) ($#k22_binop_2 :::"*"::: ) (Set (Var "i2"))))) ")" )); definitionfunc :::"addnat"::: -> ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: BINOP_2:def 23 (Bool "for" (Set (Var "n1")) "," (Set (Var "n2")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k1_binop_1 :::"."::: ) "(" (Set (Var "n1")) "," (Set (Var "n2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "n1")) ($#k23_binop_2 :::"+"::: ) (Set (Var "n2"))))); func :::"multnat"::: -> ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: BINOP_2:def 24 (Bool "for" (Set (Var "n1")) "," (Set (Var "n2")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k1_binop_1 :::"."::: ) "(" (Set (Var "n1")) "," (Set (Var "n2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "n1")) ($#k24_binop_2 :::"*"::: ) (Set (Var "n2"))))); end; :: deftheorem defines :::"addnat"::: BINOP_2:def 23 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k47_binop_2 :::"addnat"::: ) )) "iff" (Bool "for" (Set (Var "n1")) "," (Set (Var "n2")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b1")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "n1")) "," (Set (Var "n2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "n1")) ($#k23_binop_2 :::"+"::: ) (Set (Var "n2"))))) ")" )); :: deftheorem defines :::"multnat"::: BINOP_2:def 24 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k48_binop_2 :::"multnat"::: ) )) "iff" (Bool "for" (Set (Var "n1")) "," (Set (Var "n2")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b1")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "n1")) "," (Set (Var "n2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "n1")) ($#k24_binop_2 :::"*"::: ) (Set (Var "n2"))))) ")" )); registration cluster (Set ($#k27_binop_2 :::"addcomplex"::: ) ) -> ($#v1_binop_1 :::"commutative"::: ) ($#v2_binop_1 :::"associative"::: ) ; cluster (Set ($#k29_binop_2 :::"multcomplex"::: ) ) -> ($#v1_binop_1 :::"commutative"::: ) ($#v2_binop_1 :::"associative"::: ) ; cluster (Set ($#k33_binop_2 :::"addreal"::: ) ) -> ($#v1_binop_1 :::"commutative"::: ) ($#v2_binop_1 :::"associative"::: ) ; cluster (Set ($#k35_binop_2 :::"multreal"::: ) ) -> ($#v1_binop_1 :::"commutative"::: ) ($#v2_binop_1 :::"associative"::: ) ; cluster (Set ($#k39_binop_2 :::"addrat"::: ) ) -> ($#v1_binop_1 :::"commutative"::: ) ($#v2_binop_1 :::"associative"::: ) ; cluster (Set ($#k41_binop_2 :::"multrat"::: ) ) -> ($#v1_binop_1 :::"commutative"::: ) ($#v2_binop_1 :::"associative"::: ) ; cluster (Set ($#k44_binop_2 :::"addint"::: ) ) -> ($#v1_binop_1 :::"commutative"::: ) ($#v2_binop_1 :::"associative"::: ) ; cluster (Set ($#k46_binop_2 :::"multint"::: ) ) -> ($#v1_binop_1 :::"commutative"::: ) ($#v2_binop_1 :::"associative"::: ) ; cluster (Set ($#k47_binop_2 :::"addnat"::: ) ) -> ($#v1_binop_1 :::"commutative"::: ) ($#v2_binop_1 :::"associative"::: ) ; cluster (Set ($#k48_binop_2 :::"multnat"::: ) ) -> ($#v1_binop_1 :::"commutative"::: ) ($#v2_binop_1 :::"associative"::: ) ; end; registration cluster (Set ($#k27_binop_2 :::"addcomplex"::: ) ) -> ($#v1_setwiseo :::"having_a_unity"::: ) ; cluster (Set ($#k33_binop_2 :::"addreal"::: ) ) -> ($#v1_setwiseo :::"having_a_unity"::: ) ; cluster (Set ($#k39_binop_2 :::"addrat"::: ) ) -> ($#v1_setwiseo :::"having_a_unity"::: ) ; cluster (Set ($#k44_binop_2 :::"addint"::: ) ) -> ($#v1_setwiseo :::"having_a_unity"::: ) ; cluster (Set ($#k47_binop_2 :::"addnat"::: ) ) -> ($#v1_setwiseo :::"having_a_unity"::: ) ; cluster (Set ($#k29_binop_2 :::"multcomplex"::: ) ) -> ($#v1_setwiseo :::"having_a_unity"::: ) ; cluster (Set ($#k35_binop_2 :::"multreal"::: ) ) -> ($#v1_setwiseo :::"having_a_unity"::: ) ; cluster (Set ($#k41_binop_2 :::"multrat"::: ) ) -> ($#v1_setwiseo :::"having_a_unity"::: ) ; cluster (Set ($#k46_binop_2 :::"multint"::: ) ) -> ($#v1_setwiseo :::"having_a_unity"::: ) ; cluster (Set ($#k48_binop_2 :::"multnat"::: ) ) -> ($#v1_setwiseo :::"having_a_unity"::: ) ; end; theorem :: BINOP_2:1 (Bool (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set ($#k27_binop_2 :::"addcomplex"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ; theorem :: BINOP_2:2 (Bool (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set ($#k33_binop_2 :::"addreal"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ; theorem :: BINOP_2:3 (Bool (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set ($#k39_binop_2 :::"addrat"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ; theorem :: BINOP_2:4 (Bool (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set ($#k44_binop_2 :::"addint"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ; theorem :: BINOP_2:5 (Bool (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set ($#k47_binop_2 :::"addnat"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ; theorem :: BINOP_2:6 (Bool (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set ($#k29_binop_2 :::"multcomplex"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) ; theorem :: BINOP_2:7 (Bool (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set ($#k35_binop_2 :::"multreal"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) ; theorem :: BINOP_2:8 (Bool (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set ($#k41_binop_2 :::"multrat"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) ; theorem :: BINOP_2:9 (Bool (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set ($#k46_binop_2 :::"multint"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) ; theorem :: BINOP_2:10 (Bool (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set ($#k48_binop_2 :::"multnat"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) ;