:: BINOP_1 semantic presentation begin definitionlet "f" be ($#m1_hidden :::"Function":::); let "a", "b" be ($#m1_hidden :::"set"::: ) ; func "f" :::"."::: "(" "a" "," "b" ")" -> ($#m1_hidden :::"set"::: ) equals :: BINOP_1:def 1 (Set "f" ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) "a" "," "b" ($#k4_tarski :::"]"::: ) )); end; :: deftheorem defines :::"."::: BINOP_1:def 1 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "f")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ))))); definitionlet "A", "B" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "C" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "A")) "," (Set (Const "B")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Const "C")); let "a" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "A")); let "b" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "B")); :: original: :::"."::: redefine func "f" :::"."::: "(" "a" "," "b" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" "C"; end; theorem :: BINOP_1:1 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "Z")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set (Var "f1")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f2")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) ")" )) "holds" (Bool (Set (Var "f1")) ($#r2_funct_2 :::"="::: ) (Set (Var "f2"))))) ; theorem :: BINOP_1:2 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "Z")) "st" (Bool (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set (Set (Var "f1")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f2")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))) ")" )) "holds" (Bool (Set (Var "f1")) ($#r2_funct_2 :::"="::: ) (Set (Var "f2"))))) ; definitionlet "A" be ($#m1_hidden :::"set"::: ) ; mode UnOp of "A" is ($#m1_subset_1 :::"Function":::) "of" "A" "," "A"; mode BinOp of "A" is ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) "A" "," "A" ($#k2_zfmisc_1 :::":]"::: ) ) "," "A"; end; definitionlet "A" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "A")); let "a", "b" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "A")); :: original: :::"."::: redefine func "f" :::"."::: "(" "a" "," "b" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" "A"; end; scheme :: BINOP_1:sch 1 FuncEx2{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , F3() -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set F3 "(" ")" ) "st" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" ))) "holds" (Bool P1[(Set (Var "x")) "," (Set (Var "y")) "," (Set (Set (Var "f")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )]))) provided (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" ))) "holds" (Bool "ex" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set F3 "(" ")" )) & (Bool P1[(Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z"))]) ")" ))) proof end; scheme :: BINOP_1:sch 2 Lambda2{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , F3() -> ($#m1_hidden :::"set"::: ) , F4( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set F3 "(" ")" ) "st" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" ))) "holds" (Bool (Set (Set (Var "f")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "x")) "," (Set (Var "y")) ")" )))) provided (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" ))) "holds" (Bool (Set F4 "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r2_hidden :::"in"::: ) (Set F3 "(" ")" ))) proof end; scheme :: BINOP_1:sch 3 FuncEx2D{ 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() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set F3 "(" ")" ) "st" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "holds" (Bool P1[(Set (Var "x")) "," (Set (Var "y")) "," (Set (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )])))) provided (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) (Bool "ex" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F3 "(" ")" ) "st" (Bool P1[(Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z"))])))) proof end; scheme :: BINOP_1:sch 4 Lambda2D{ 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() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F4( ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "," ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" )) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F3 "(" ")" ) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set F3 "(" ")" ) "st" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "holds" (Bool (Set (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "x")) "," (Set (Var "y")) ")" ))))) proof end; definitionlet "A" be ($#m1_hidden :::"set"::: ) ; let "o" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "A")); attr "o" is :::"commutative"::: means :: BINOP_1:def 2 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "A" "holds" (Bool (Set "o" ($#k3_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set "o" ($#k3_binop_1 :::"."::: ) "(" (Set (Var "b")) "," (Set (Var "a")) ")" ))); attr "o" is :::"associative"::: means :: BINOP_1:def 3 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "A" "holds" (Bool (Set "o" ($#k3_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set "(" "o" ($#k3_binop_1 :::"."::: ) "(" (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set "o" ($#k3_binop_1 :::"."::: ) "(" (Set "(" "o" ($#k3_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set (Var "c")) ")" ))); attr "o" is :::"idempotent"::: means :: BINOP_1:def 4 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "A" "holds" (Bool (Set "o" ($#k3_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "a")))); end; :: deftheorem defines :::"commutative"::: BINOP_1:def 2 : (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "o")) "is" ($#v1_binop_1 :::"commutative"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "o")) ($#k3_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "o")) ($#k3_binop_1 :::"."::: ) "(" (Set (Var "b")) "," (Set (Var "a")) ")" ))) ")" ))); :: deftheorem defines :::"associative"::: BINOP_1:def 3 : (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "o")) "is" ($#v2_binop_1 :::"associative"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "o")) ($#k3_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set "(" (Set (Var "o")) ($#k3_binop_1 :::"."::: ) "(" (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "o")) ($#k3_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "o")) ($#k3_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set (Var "c")) ")" ))) ")" ))); :: deftheorem defines :::"idempotent"::: BINOP_1:def 4 : (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "o")) "is" ($#v3_binop_1 :::"idempotent"::: ) ) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "o")) ($#k3_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "a")))) ")" ))); registration cluster ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FUNCT_2((Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) )) -> ($#v1_xboole_0 :::"empty"::: ) ($#v1_binop_1 :::"commutative"::: ) ($#v2_binop_1 :::"associative"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )); end; definitionlet "A" be ($#m1_hidden :::"set"::: ) ; let "e" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "A")); let "o" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "A")); pred "e" :::"is_a_left_unity_wrt"::: "o" means :: BINOP_1:def 5 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "A" "holds" (Bool (Set "o" ($#k3_binop_1 :::"."::: ) "(" "e" "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "a")))); pred "e" :::"is_a_right_unity_wrt"::: "o" means :: BINOP_1:def 6 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "A" "holds" (Bool (Set "o" ($#k3_binop_1 :::"."::: ) "(" (Set (Var "a")) "," "e" ")" ) ($#r1_hidden :::"="::: ) (Set (Var "a")))); end; :: deftheorem defines :::"is_a_left_unity_wrt"::: BINOP_1:def 5 : (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "e")) ($#r1_binop_1 :::"is_a_left_unity_wrt"::: ) (Set (Var "o"))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "o")) ($#k3_binop_1 :::"."::: ) "(" (Set (Var "e")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "a")))) ")" )))); :: deftheorem defines :::"is_a_right_unity_wrt"::: BINOP_1:def 6 : (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "e")) ($#r2_binop_1 :::"is_a_right_unity_wrt"::: ) (Set (Var "o"))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "o")) ($#k3_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "e")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "a")))) ")" )))); definitionlet "A" be ($#m1_hidden :::"set"::: ) ; let "e" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "A")); let "o" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "A")); pred "e" :::"is_a_unity_wrt"::: "o" means :: BINOP_1:def 7 (Bool "(" (Bool "e" ($#r1_binop_1 :::"is_a_left_unity_wrt"::: ) "o") & (Bool "e" ($#r2_binop_1 :::"is_a_right_unity_wrt"::: ) "o") ")" ); end; :: deftheorem defines :::"is_a_unity_wrt"::: BINOP_1:def 7 : (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "e")) ($#r3_binop_1 :::"is_a_unity_wrt"::: ) (Set (Var "o"))) "iff" (Bool "(" (Bool (Set (Var "e")) ($#r1_binop_1 :::"is_a_left_unity_wrt"::: ) (Set (Var "o"))) & (Bool (Set (Var "e")) ($#r2_binop_1 :::"is_a_right_unity_wrt"::: ) (Set (Var "o"))) ")" ) ")" )))); theorem :: BINOP_1:3 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "e")) ($#r3_binop_1 :::"is_a_unity_wrt"::: ) (Set (Var "o"))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Set (Var "o")) ($#k3_binop_1 :::"."::: ) "(" (Set (Var "e")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Set (Var "o")) ($#k3_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "e")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" )) ")" )))) ; theorem :: BINOP_1:4 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "o")) "is" ($#v1_binop_1 :::"commutative"::: ) )) "holds" (Bool "(" (Bool (Set (Var "e")) ($#r3_binop_1 :::"is_a_unity_wrt"::: ) (Set (Var "o"))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "o")) ($#k3_binop_1 :::"."::: ) "(" (Set (Var "e")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "a")))) ")" )))) ; theorem :: BINOP_1:5 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "o")) "is" ($#v1_binop_1 :::"commutative"::: ) )) "holds" (Bool "(" (Bool (Set (Var "e")) ($#r3_binop_1 :::"is_a_unity_wrt"::: ) (Set (Var "o"))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "o")) ($#k3_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "e")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "a")))) ")" )))) ; theorem :: BINOP_1:6 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "o")) "is" ($#v1_binop_1 :::"commutative"::: ) )) "holds" (Bool "(" (Bool (Set (Var "e")) ($#r3_binop_1 :::"is_a_unity_wrt"::: ) (Set (Var "o"))) "iff" (Bool (Set (Var "e")) ($#r1_binop_1 :::"is_a_left_unity_wrt"::: ) (Set (Var "o"))) ")" )))) ; theorem :: BINOP_1:7 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "o")) "is" ($#v1_binop_1 :::"commutative"::: ) )) "holds" (Bool "(" (Bool (Set (Var "e")) ($#r3_binop_1 :::"is_a_unity_wrt"::: ) (Set (Var "o"))) "iff" (Bool (Set (Var "e")) ($#r2_binop_1 :::"is_a_right_unity_wrt"::: ) (Set (Var "o"))) ")" )))) ; theorem :: BINOP_1:8 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "o")) "is" ($#v1_binop_1 :::"commutative"::: ) )) "holds" (Bool "(" (Bool (Set (Var "e")) ($#r1_binop_1 :::"is_a_left_unity_wrt"::: ) (Set (Var "o"))) "iff" (Bool (Set (Var "e")) ($#r2_binop_1 :::"is_a_right_unity_wrt"::: ) (Set (Var "o"))) ")" )))) ; theorem :: BINOP_1:9 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "e1")) "," (Set (Var "e2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "e1")) ($#r1_binop_1 :::"is_a_left_unity_wrt"::: ) (Set (Var "o"))) & (Bool (Set (Var "e2")) ($#r2_binop_1 :::"is_a_right_unity_wrt"::: ) (Set (Var "o")))) "holds" (Bool (Set (Var "e1")) ($#r1_hidden :::"="::: ) (Set (Var "e2")))))) ; theorem :: BINOP_1:10 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "e1")) "," (Set (Var "e2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "e1")) ($#r3_binop_1 :::"is_a_unity_wrt"::: ) (Set (Var "o"))) & (Bool (Set (Var "e2")) ($#r3_binop_1 :::"is_a_unity_wrt"::: ) (Set (Var "o")))) "holds" (Bool (Set (Var "e1")) ($#r1_hidden :::"="::: ) (Set (Var "e2")))))) ; definitionlet "A" be ($#m1_hidden :::"set"::: ) ; let "o" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "A")); assume (Bool "ex" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "A")) "st" (Bool (Set (Var "e")) ($#r3_binop_1 :::"is_a_unity_wrt"::: ) (Set (Const "o")))) ; func :::"the_unity_wrt"::: "o" -> ($#m1_subset_1 :::"Element"::: ) "of" "A" means :: BINOP_1:def 8 (Bool it ($#r3_binop_1 :::"is_a_unity_wrt"::: ) "o"); end; :: deftheorem defines :::"the_unity_wrt"::: BINOP_1:def 8 : (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "A")) "st" (Bool (Bool "ex" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "st" (Bool (Set (Var "e")) ($#r3_binop_1 :::"is_a_unity_wrt"::: ) (Set (Var "o"))))) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "o")))) "iff" (Bool (Set (Var "b3")) ($#r3_binop_1 :::"is_a_unity_wrt"::: ) (Set (Var "o"))) ")" )))); definitionlet "A" be ($#m1_hidden :::"set"::: ) ; let "o9", "o" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "A")); pred "o9" :::"is_left_distributive_wrt"::: "o" means :: BINOP_1:def 9 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "A" "holds" (Bool (Set "o9" ($#k3_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set "(" "o" ($#k3_binop_1 :::"."::: ) "(" (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set "o" ($#k3_binop_1 :::"."::: ) "(" (Set "(" "o9" ($#k3_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set "(" "o9" ($#k3_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "c")) ")" ")" ) ")" ))); pred "o9" :::"is_right_distributive_wrt"::: "o" means :: BINOP_1:def 10 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "A" "holds" (Bool (Set "o9" ($#k3_binop_1 :::"."::: ) "(" (Set "(" "o" ($#k3_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set "o" ($#k3_binop_1 :::"."::: ) "(" (Set "(" "o9" ($#k3_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "c")) ")" ")" ) "," (Set "(" "o9" ($#k3_binop_1 :::"."::: ) "(" (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) ")" ))); end; :: deftheorem defines :::"is_left_distributive_wrt"::: BINOP_1:def 9 : (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "o9")) "," (Set (Var "o")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "o9")) ($#r4_binop_1 :::"is_left_distributive_wrt"::: ) (Set (Var "o"))) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "o9")) ($#k3_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set "(" (Set (Var "o")) ($#k3_binop_1 :::"."::: ) "(" (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "o")) ($#k3_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "o9")) ($#k3_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set "(" (Set (Var "o9")) ($#k3_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "c")) ")" ")" ) ")" ))) ")" ))); :: deftheorem defines :::"is_right_distributive_wrt"::: BINOP_1:def 10 : (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "o9")) "," (Set (Var "o")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "o9")) ($#r5_binop_1 :::"is_right_distributive_wrt"::: ) (Set (Var "o"))) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "o9")) ($#k3_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "o")) ($#k3_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "o")) ($#k3_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "o9")) ($#k3_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "c")) ")" ")" ) "," (Set "(" (Set (Var "o9")) ($#k3_binop_1 :::"."::: ) "(" (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) ")" ))) ")" ))); definitionlet "A" be ($#m1_hidden :::"set"::: ) ; let "o9", "o" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "A")); pred "o9" :::"is_distributive_wrt"::: "o" means :: BINOP_1:def 11 (Bool "(" (Bool "o9" ($#r4_binop_1 :::"is_left_distributive_wrt"::: ) "o") & (Bool "o9" ($#r5_binop_1 :::"is_right_distributive_wrt"::: ) "o") ")" ); end; :: deftheorem defines :::"is_distributive_wrt"::: BINOP_1:def 11 : (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "o9")) "," (Set (Var "o")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "o9")) ($#r6_binop_1 :::"is_distributive_wrt"::: ) (Set (Var "o"))) "iff" (Bool "(" (Bool (Set (Var "o9")) ($#r4_binop_1 :::"is_left_distributive_wrt"::: ) (Set (Var "o"))) & (Bool (Set (Var "o9")) ($#r5_binop_1 :::"is_right_distributive_wrt"::: ) (Set (Var "o"))) ")" ) ")" ))); theorem :: BINOP_1:11 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "o9")) "," (Set (Var "o")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "o9")) ($#r6_binop_1 :::"is_distributive_wrt"::: ) (Set (Var "o"))) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Set (Var "o9")) ($#k3_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set "(" (Set (Var "o")) ($#k3_binop_1 :::"."::: ) "(" (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "o")) ($#k3_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "o9")) ($#k3_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set "(" (Set (Var "o9")) ($#k3_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "c")) ")" ")" ) ")" )) & (Bool (Set (Set (Var "o9")) ($#k3_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "o")) ($#k3_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "o")) ($#k3_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "o9")) ($#k3_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "c")) ")" ")" ) "," (Set "(" (Set (Var "o9")) ($#k3_binop_1 :::"."::: ) "(" (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) ")" )) ")" )) ")" ))) ; theorem :: BINOP_1:12 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "o")) "," (Set (Var "o9")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "o9")) "is" ($#v1_binop_1 :::"commutative"::: ) )) "holds" (Bool "(" (Bool (Set (Var "o9")) ($#r6_binop_1 :::"is_distributive_wrt"::: ) (Set (Var "o"))) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "o9")) ($#k3_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set "(" (Set (Var "o")) ($#k3_binop_1 :::"."::: ) "(" (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "o")) ($#k3_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "o9")) ($#k3_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set "(" (Set (Var "o9")) ($#k3_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "c")) ")" ")" ) ")" ))) ")" ))) ; theorem :: BINOP_1:13 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "o")) "," (Set (Var "o9")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "o9")) "is" ($#v1_binop_1 :::"commutative"::: ) )) "holds" (Bool "(" (Bool (Set (Var "o9")) ($#r6_binop_1 :::"is_distributive_wrt"::: ) (Set (Var "o"))) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "o9")) ($#k3_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "o")) ($#k3_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "o")) ($#k3_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "o9")) ($#k3_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "c")) ")" ")" ) "," (Set "(" (Set (Var "o9")) ($#k3_binop_1 :::"."::: ) "(" (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) ")" ))) ")" ))) ; theorem :: BINOP_1:14 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "o")) "," (Set (Var "o9")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "o9")) "is" ($#v1_binop_1 :::"commutative"::: ) )) "holds" (Bool "(" (Bool (Set (Var "o9")) ($#r6_binop_1 :::"is_distributive_wrt"::: ) (Set (Var "o"))) "iff" (Bool (Set (Var "o9")) ($#r4_binop_1 :::"is_left_distributive_wrt"::: ) (Set (Var "o"))) ")" ))) ; theorem :: BINOP_1:15 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "o")) "," (Set (Var "o9")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "o9")) "is" ($#v1_binop_1 :::"commutative"::: ) )) "holds" (Bool "(" (Bool (Set (Var "o9")) ($#r6_binop_1 :::"is_distributive_wrt"::: ) (Set (Var "o"))) "iff" (Bool (Set (Var "o9")) ($#r5_binop_1 :::"is_right_distributive_wrt"::: ) (Set (Var "o"))) ")" ))) ; theorem :: BINOP_1:16 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "o")) "," (Set (Var "o9")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "o9")) "is" ($#v1_binop_1 :::"commutative"::: ) )) "holds" (Bool "(" (Bool (Set (Var "o9")) ($#r5_binop_1 :::"is_right_distributive_wrt"::: ) (Set (Var "o"))) "iff" (Bool (Set (Var "o9")) ($#r4_binop_1 :::"is_left_distributive_wrt"::: ) (Set (Var "o"))) ")" ))) ; definitionlet "A" be ($#m1_hidden :::"set"::: ) ; let "u" be ($#m1_subset_1 :::"UnOp":::) "of" (Set (Const "A")); let "o" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "A")); pred "u" :::"is_distributive_wrt"::: "o" means :: BINOP_1:def 12 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "A" "holds" (Bool (Set "u" ($#k1_funct_1 :::"."::: ) (Set "(" "o" ($#k3_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set "o" ($#k1_binop_1 :::"."::: ) "(" (Set "(" "u" ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set "(" "u" ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" ) ")" ))); end; :: deftheorem defines :::"is_distributive_wrt"::: BINOP_1:def 12 : (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "u")) ($#r7_binop_1 :::"is_distributive_wrt"::: ) (Set (Var "o"))) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "u")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "o")) ($#k3_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "o")) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "u")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set "(" (Set (Var "u")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" ) ")" ))) ")" )))); definitioncanceled; canceled; canceled; let "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "e" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "A")); let "o" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "A")); redefine pred "e" :::"is_a_left_unity_wrt"::: "o" means :: BINOP_1:def 16 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "A" "holds" (Bool (Set "o" ($#k3_binop_1 :::"."::: ) "(" "e" "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "a")))); redefine pred "e" :::"is_a_right_unity_wrt"::: "o" means :: BINOP_1:def 17 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "A" "holds" (Bool (Set "o" ($#k3_binop_1 :::"."::: ) "(" (Set (Var "a")) "," "e" ")" ) ($#r1_hidden :::"="::: ) (Set (Var "a")))); end; :: deftheorem BINOP_1:def 13 : canceled; :: deftheorem BINOP_1:def 14 : canceled; :: deftheorem BINOP_1:def 15 : canceled; :: deftheorem defines :::"is_a_left_unity_wrt"::: BINOP_1:def 16 : (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "e")) ($#r1_binop_1 :::"is_a_left_unity_wrt"::: ) (Set (Var "o"))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "o")) ($#k3_binop_1 :::"."::: ) "(" (Set (Var "e")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "a")))) ")" )))); :: deftheorem defines :::"is_a_right_unity_wrt"::: BINOP_1:def 17 : (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "e")) ($#r2_binop_1 :::"is_a_right_unity_wrt"::: ) (Set (Var "o"))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "o")) ($#k3_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "e")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "a")))) ")" )))); definitionlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "o9", "o" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "A")); redefine pred "o9" :::"is_left_distributive_wrt"::: "o" means :: BINOP_1:def 18 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "A" "holds" (Bool (Set "o9" ($#k3_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set "(" "o" ($#k3_binop_1 :::"."::: ) "(" (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set "o" ($#k3_binop_1 :::"."::: ) "(" (Set "(" "o9" ($#k3_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set "(" "o9" ($#k3_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "c")) ")" ")" ) ")" ))); redefine pred "o9" :::"is_right_distributive_wrt"::: "o" means :: BINOP_1:def 19 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "A" "holds" (Bool (Set "o9" ($#k3_binop_1 :::"."::: ) "(" (Set "(" "o" ($#k3_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set "o" ($#k3_binop_1 :::"."::: ) "(" (Set "(" "o9" ($#k3_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "c")) ")" ")" ) "," (Set "(" "o9" ($#k3_binop_1 :::"."::: ) "(" (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) ")" ))); end; :: deftheorem defines :::"is_left_distributive_wrt"::: BINOP_1:def 18 : (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "o9")) "," (Set (Var "o")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "o9")) ($#r4_binop_1 :::"is_left_distributive_wrt"::: ) (Set (Var "o"))) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "o9")) ($#k3_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set "(" (Set (Var "o")) ($#k3_binop_1 :::"."::: ) "(" (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "o")) ($#k3_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "o9")) ($#k3_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set "(" (Set (Var "o9")) ($#k3_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "c")) ")" ")" ) ")" ))) ")" ))); :: deftheorem defines :::"is_right_distributive_wrt"::: BINOP_1:def 19 : (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "o9")) "," (Set (Var "o")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "o9")) ($#r5_binop_1 :::"is_right_distributive_wrt"::: ) (Set (Var "o"))) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "o9")) ($#k3_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "o")) ($#k3_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "o")) ($#k3_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "o9")) ($#k3_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "c")) ")" ")" ) "," (Set "(" (Set (Var "o9")) ($#k3_binop_1 :::"."::: ) "(" (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) ")" ))) ")" ))); definitionlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "u" be ($#m1_subset_1 :::"UnOp":::) "of" (Set (Const "A")); let "o" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "A")); redefine pred "u" :::"is_distributive_wrt"::: "o" means :: BINOP_1:def 20 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "A" "holds" (Bool (Set "u" ($#k3_funct_2 :::"."::: ) (Set "(" "o" ($#k3_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set "o" ($#k3_binop_1 :::"."::: ) "(" (Set "(" "u" ($#k3_funct_2 :::"."::: ) (Set (Var "a")) ")" ) "," (Set "(" "u" ($#k3_funct_2 :::"."::: ) (Set (Var "b")) ")" ) ")" ))); end; :: deftheorem defines :::"is_distributive_wrt"::: BINOP_1:def 20 : (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "u")) ($#r7_binop_1 :::"is_distributive_wrt"::: ) (Set (Var "o"))) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "u")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "o")) ($#k3_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "o")) ($#k3_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "u")) ($#k3_funct_2 :::"."::: ) (Set (Var "a")) ")" ) "," (Set "(" (Set (Var "u")) ($#k3_funct_2 :::"."::: ) (Set (Var "b")) ")" ) ")" ))) ")" )))); theorem :: BINOP_1:17 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "Z")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) & (Bool (Set (Var "Z")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set (Var "f")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r2_hidden :::"in"::: ) (Set (Var "Z"))))) ; theorem :: BINOP_1:18 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "Z")) (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "Z")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set "(" (Set (Var "g")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "f")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" )))))) ; theorem :: BINOP_1:19 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v3_funct_1 :::"constant"::: ) ) "iff" (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "y1")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) & (Bool (Set (Var "y2")) ($#r2_hidden :::"in"::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) ")" ))) ")" ))) ; theorem :: BINOP_1:20 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "Z")) "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f1"))) ($#r2_relset_1 :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f2")))) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f1"))))) "holds" (Bool (Set (Set (Var "f1")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f2")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) ")" )) "holds" (Bool (Set (Var "f1")) ($#r2_relset_1 :::"="::: ) (Set (Var "f2"))))) ; scheme :: BINOP_1:sch 5 PartFuncEx2{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , F3() -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set F3 "(" ")" ) "st" (Bool "(" (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" )) & (Bool "ex" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool P1[(Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z"))])) ")" ) ")" ) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool P1[(Set (Var "x")) "," (Set (Var "y")) "," (Set (Set (Var "f")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )]) ")" ) ")" )) provided (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" )) & (Bool P1[(Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z"))])) "holds" (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set F3 "(" ")" ))) and (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" )) & (Bool P1[(Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z1"))]) & (Bool P1[(Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z2"))])) "holds" (Bool (Set (Var "z1")) ($#r1_hidden :::"="::: ) (Set (Var "z2")))) proof end; scheme :: BINOP_1:sch 6 LambdaR2{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , F3() -> ($#m1_hidden :::"set"::: ) , F4( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set F3 "(" ")" ) "st" (Bool "(" (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" )) & (Bool P1[(Set (Var "x")) "," (Set (Var "y"))]) ")" ) ")" ) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) ")" ) ")" )) provided (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool P1[(Set (Var "x")) "," (Set (Var "y"))])) "holds" (Bool (Set F4 "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r2_hidden :::"in"::: ) (Set F3 "(" ")" ))) proof end; scheme :: BINOP_1:sch 7 PartLambda2{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , F3() -> ($#m1_hidden :::"set"::: ) , F4( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set F3 "(" ")" ) "st" (Bool "(" (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" )) & (Bool P1[(Set (Var "x")) "," (Set (Var "y"))]) ")" ) ")" ) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) ")" ) ")" )) provided (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" )) & (Bool P1[(Set (Var "x")) "," (Set (Var "y"))])) "holds" (Bool (Set F4 "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r2_hidden :::"in"::: ) (Set F3 "(" ")" ))) proof end; scheme :: BINOP_1:sch 8 Sch8{ 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_hidden :::"set"::: ) , F4( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set F3 "(" ")" ) "st" (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) "iff" (Bool P1[(Set (Var "x")) "," (Set (Var "y"))]) ")" )) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "x")) "," (Set (Var "y")) ")" ))) ")" ) ")" )) provided (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "st" (Bool (Bool P1[(Set (Var "x")) "," (Set (Var "y"))])) "holds" (Bool (Set F4 "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r2_hidden :::"in"::: ) (Set F3 "(" ")" )))) proof end; definitionlet "A" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "A")); let "x", "y" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "A")); :: original: :::"."::: redefine func "f" :::"."::: "(" "x" "," "y" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" "A"; end; definitionlet "X", "Y", "Z" be ($#m1_hidden :::"set"::: ) ; let "f1", "f2" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "X")) "," (Set (Const "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Const "Z")); :: original: :::"="::: redefine pred "f1" :::"="::: "f2" means :: BINOP_1:def 21 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "X") & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) "Y")) "holds" (Bool (Set "f1" ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set "f2" ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ))); end; :: deftheorem defines :::"="::: BINOP_1:def 21 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "Z")) "holds" (Bool "(" (Bool (Set (Var "f1")) ($#r8_binop_1 :::"="::: ) (Set (Var "f2"))) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set (Var "f1")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f2")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ))) ")" )));