:: BVFUNC_2 semantic presentation begin definitionlet "X" be ($#m1_hidden :::"set"::: ) ; :: original: :::"PARTITIONS"::: redefine func :::"PARTITIONS"::: "X" -> ($#m1_subset_1 :::"Part-Family":::) "of" "X"; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Part-Family":::) "of" (Set (Const "X")); :: original: :::"Element"::: redefine mode :::"Element"::: "of" "F" -> ($#m1_eqrel_1 :::"a_partition"::: ) "of" "X"; end; theorem :: BVFUNC_2:1 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_partit1 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) (Bool "ex" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool "ex" (Set (Var "h")) "being" ($#m1_hidden :::"Function":::)(Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "Y")) "st" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Var "G"))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Var "F"))) & (Bool "(" "for" (Set (Var "d")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set (Var "G")))) "holds" (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "d"))) ($#r2_hidden :::"in"::: ) (Set (Var "d"))) ")" ) & (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k8_setfam_1 :::"Intersect"::: ) (Set (Var "F")))) & (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ))) ")" ))))) ; definitionlet "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "G" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_bvfunc_2 :::"PARTITIONS"::: ) (Set (Const "Y")) ")" ); func :::"'/\'"::: "G" -> ($#m1_eqrel_1 :::"a_partition"::: ) "of" "Y" means :: BVFUNC_2:def 1 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "h")) "being" ($#m1_hidden :::"Function":::)(Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" "Y" "st" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) "G") & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Var "F"))) & (Bool "(" "for" (Set (Var "d")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) "G")) "holds" (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "d"))) ($#r2_hidden :::"in"::: ) (Set (Var "d"))) ")" ) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k8_setfam_1 :::"Intersect"::: ) (Set (Var "F")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ))) ")" )); end; :: deftheorem defines :::"'/\'"::: BVFUNC_2:def 1 : (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_bvfunc_2 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "b3")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k2_bvfunc_2 :::"'/\'"::: ) (Set (Var "G")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "ex" (Set (Var "h")) "being" ($#m1_hidden :::"Function":::)(Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "Y")) "st" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Var "G"))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Var "F"))) & (Bool "(" "for" (Set (Var "d")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set (Var "G")))) "holds" (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "d"))) ($#r2_hidden :::"in"::: ) (Set (Var "d"))) ")" ) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k8_setfam_1 :::"Intersect"::: ) (Set (Var "F")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ))) ")" )) ")" )))); definitionlet "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "G" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_bvfunc_2 :::"PARTITIONS"::: ) (Set (Const "Y")) ")" ); let "b" be ($#m1_hidden :::"set"::: ) ; pred "b" :::"is_upper_min_depend_of"::: "G" means :: BVFUNC_2:def 2 (Bool "(" (Bool "(" "for" (Set (Var "d")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" "Y" "st" (Bool (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) "G")) "holds" (Bool "b" ($#r1_partit1 :::"is_a_dependent_set_of"::: ) (Set (Var "d"))) ")" ) & (Bool "(" "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r1_tarski :::"c="::: ) "b") & (Bool "(" "for" (Set (Var "d")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" "Y" "st" (Bool (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) "G")) "holds" (Bool (Set (Var "e")) ($#r1_partit1 :::"is_a_dependent_set_of"::: ) (Set (Var "d"))) ")" )) "holds" (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) "b") ")" ) ")" ); end; :: deftheorem defines :::"is_upper_min_depend_of"::: BVFUNC_2:def 2 : (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_bvfunc_2 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b")) ($#r1_bvfunc_2 :::"is_upper_min_depend_of"::: ) (Set (Var "G"))) "iff" (Bool "(" (Bool "(" "for" (Set (Var "d")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set (Var "G")))) "holds" (Bool (Set (Var "b")) ($#r1_partit1 :::"is_a_dependent_set_of"::: ) (Set (Var "d"))) ")" ) & (Bool "(" "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r1_tarski :::"c="::: ) (Set (Var "b"))) & (Bool "(" "for" (Set (Var "d")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set (Var "G")))) "holds" (Bool (Set (Var "e")) ($#r1_partit1 :::"is_a_dependent_set_of"::: ) (Set (Var "d"))) ")" )) "holds" (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" ) ")" ) ")" )))); theorem :: BVFUNC_2:2 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_partit1 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "ex" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "X")) ($#r1_bvfunc_2 :::"is_upper_min_depend_of"::: ) (Set (Var "G"))) ")" ))))) ; definitionlet "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "G" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_bvfunc_2 :::"PARTITIONS"::: ) (Set (Const "Y")) ")" ); func :::"'\/'"::: "G" -> ($#m1_eqrel_1 :::"a_partition"::: ) "of" "Y" means :: BVFUNC_2:def 3 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "x")) ($#r1_bvfunc_2 :::"is_upper_min_depend_of"::: ) "G") ")" )) if (Bool "G" ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) otherwise (Bool it ($#r1_hidden :::"="::: ) (Set ($#k10_eqrel_1 :::"%I"::: ) "Y")); end; :: deftheorem defines :::"'\/'"::: BVFUNC_2:def 3 : (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_bvfunc_2 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "b3")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k3_bvfunc_2 :::"'\/'"::: ) (Set (Var "G")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool (Set (Var "x")) ($#r1_bvfunc_2 :::"is_upper_min_depend_of"::: ) (Set (Var "G"))) ")" )) ")" ) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "G")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) "implies" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k3_bvfunc_2 :::"'\/'"::: ) (Set (Var "G")))) "iff" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k10_eqrel_1 :::"%I"::: ) (Set (Var "Y")))) ")" ) ")" ")" )))); theorem :: BVFUNC_2:3 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_bvfunc_2 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "PA")) ($#r2_hidden :::"in"::: ) (Set (Var "G")))) "holds" (Bool (Set (Var "PA")) ($#r1_setfam_1 :::"'>'"::: ) (Set ($#k2_bvfunc_2 :::"'/\'"::: ) (Set (Var "G"))))))) ; theorem :: BVFUNC_2:4 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_bvfunc_2 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "PA")) ($#r2_hidden :::"in"::: ) (Set (Var "G")))) "holds" (Bool (Set (Var "PA")) ($#r1_setfam_1 :::"'<'"::: ) (Set ($#k3_bvfunc_2 :::"'\/'"::: ) (Set (Var "G"))))))) ; begin definitionlet "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "G" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_bvfunc_2 :::"PARTITIONS"::: ) (Set (Const "Y")) ")" ); attr "G" is :::"generating"::: means :: BVFUNC_2:def 4 (Bool (Set ($#k2_bvfunc_2 :::"'/\'"::: ) "G") ($#r1_hidden :::"="::: ) (Set ($#k10_eqrel_1 :::"%I"::: ) "Y")); end; :: deftheorem defines :::"generating"::: BVFUNC_2:def 4 : (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_bvfunc_2 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#v1_bvfunc_2 :::"generating"::: ) ) "iff" (Bool (Set ($#k2_bvfunc_2 :::"'/\'"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set ($#k10_eqrel_1 :::"%I"::: ) (Set (Var "Y")))) ")" ))); definitionlet "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "G" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_bvfunc_2 :::"PARTITIONS"::: ) (Set (Const "Y")) ")" ); attr "G" is :::"independent"::: means :: BVFUNC_2:def 5 (Bool "for" (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" "Y" "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) "G") & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Var "F"))) & (Bool "(" "for" (Set (Var "d")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) "G")) "holds" (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "d"))) ($#r2_hidden :::"in"::: ) (Set (Var "d"))) ")" )) "holds" (Bool (Set ($#k8_setfam_1 :::"Intersect"::: ) (Set (Var "F"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))); end; :: deftheorem defines :::"independent"::: BVFUNC_2:def 5 : (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_bvfunc_2 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) ) "iff" (Bool "for" (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Var "G"))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Var "F"))) & (Bool "(" "for" (Set (Var "d")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set (Var "G")))) "holds" (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "d"))) ($#r2_hidden :::"in"::: ) (Set (Var "d"))) ")" )) "holds" (Bool (Set ($#k8_setfam_1 :::"Intersect"::: ) (Set (Var "F"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ")" ))); definitionlet "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "G" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_bvfunc_2 :::"PARTITIONS"::: ) (Set (Const "Y")) ")" ); pred "G" :::"is_a_coordinate"::: means :: BVFUNC_2:def 6 (Bool "(" (Bool "G" "is" ($#v2_bvfunc_2 :::"independent"::: ) ) & (Bool "G" "is" ($#v1_bvfunc_2 :::"generating"::: ) ) ")" ); end; :: deftheorem defines :::"is_a_coordinate"::: BVFUNC_2:def 6 : (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_bvfunc_2 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) "holds" (Bool "(" (Bool (Set (Var "G")) ($#r2_bvfunc_2 :::"is_a_coordinate"::: ) ) "iff" (Bool "(" (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) ) & (Bool (Set (Var "G")) "is" ($#v1_bvfunc_2 :::"generating"::: ) ) ")" ) ")" ))); definitionlet "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "PA" be ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Const "Y")); :: original: :::"{"::: redefine func :::"{":::"PA":::"}"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_bvfunc_2 :::"PARTITIONS"::: ) "Y" ")" ); end; definitionlet "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "PA" be ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Const "Y")); let "G" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_bvfunc_2 :::"PARTITIONS"::: ) (Set (Const "Y")) ")" ); func :::"CompF"::: "(" "PA" "," "G" ")" -> ($#m1_eqrel_1 :::"a_partition"::: ) "of" "Y" equals :: BVFUNC_2:def 7 (Set ($#k2_bvfunc_2 :::"'/\'"::: ) (Set "(" "G" ($#k7_subset_1 :::"\"::: ) (Set ($#k4_bvfunc_2 :::"{"::: ) "PA" ($#k4_bvfunc_2 :::"}"::: ) ) ")" )); end; :: deftheorem defines :::"CompF"::: BVFUNC_2:def 7 : (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_bvfunc_2 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) "holds" (Bool (Set ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "PA")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_bvfunc_2 :::"'/\'"::: ) (Set "(" (Set (Var "G")) ($#k7_subset_1 :::"\"::: ) (Set ($#k4_bvfunc_2 :::"{"::: ) (Set (Var "PA")) ($#k4_bvfunc_2 :::"}"::: ) ) ")" )))))); definitionlet "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ); let "G" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_bvfunc_2 :::"PARTITIONS"::: ) (Set (Const "Y")) ")" ); let "PA" be ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Const "Y")); pred "a" :::"is_independent_of"::: "PA" "," "G" means :: BVFUNC_2:def 8 (Bool "a" ($#r2_bvfunc_1 :::"is_dependent_of"::: ) (Set ($#k5_bvfunc_2 :::"CompF"::: ) "(" "PA" "," "G" ")" )); end; :: deftheorem defines :::"is_independent_of"::: BVFUNC_2:def 8 : (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_bvfunc_2 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r3_bvfunc_2 :::"is_independent_of"::: ) (Set (Var "PA")) "," (Set (Var "G"))) "iff" (Bool (Set (Var "a")) ($#r2_bvfunc_1 :::"is_dependent_of"::: ) (Set ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "PA")) "," (Set (Var "G")) ")" )) ")" ))))); definitionlet "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ); let "G" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_bvfunc_2 :::"PARTITIONS"::: ) (Set (Const "Y")) ")" ); let "PA" be ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Const "Y")); func :::"All"::: "(" "a" "," "PA" "," "G" ")" -> ($#m1_subset_1 :::"Function":::) "of" "Y" "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) equals :: BVFUNC_2:def 9 (Set ($#k16_bvfunc_1 :::"B_INF"::: ) "(" "a" "," (Set "(" ($#k5_bvfunc_2 :::"CompF"::: ) "(" "PA" "," "G" ")" ")" ) ")" ); end; :: deftheorem defines :::"All"::: BVFUNC_2:def 9 : (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_bvfunc_2 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k16_bvfunc_1 :::"B_INF"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ) ")" )))))); definitionlet "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ); let "G" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_bvfunc_2 :::"PARTITIONS"::: ) (Set (Const "Y")) ")" ); let "PA" be ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Const "Y")); func :::"Ex"::: "(" "a" "," "PA" "," "G" ")" -> ($#m1_subset_1 :::"Function":::) "of" "Y" "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) equals :: BVFUNC_2:def 10 (Set ($#k17_bvfunc_1 :::"B_SUP"::: ) "(" "a" "," (Set "(" ($#k5_bvfunc_2 :::"CompF"::: ) "(" "PA" "," "G" ")" ")" ) ")" ); end; :: deftheorem defines :::"Ex"::: BVFUNC_2:def 10 : (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_bvfunc_2 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k17_bvfunc_1 :::"B_SUP"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ) ")" )))))); theorem :: BVFUNC_2:5 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_partit1 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ) ($#r2_bvfunc_1 :::"is_dependent_of"::: ) (Set ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "PA")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC_2:6 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_partit1 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ) ($#r2_bvfunc_1 :::"is_dependent_of"::: ) (Set ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "PA")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC_2:7 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_partit1 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k12_bvfunc_1 :::"I_el"::: ) (Set (Var "Y")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k12_bvfunc_1 :::"I_el"::: ) (Set (Var "Y")))))))) ; theorem :: BVFUNC_2:8 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_partit1 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k12_bvfunc_1 :::"I_el"::: ) (Set (Var "Y")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k12_bvfunc_1 :::"I_el"::: ) (Set (Var "Y")))))))) ; theorem :: BVFUNC_2:9 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_partit1 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k11_bvfunc_1 :::"O_el"::: ) (Set (Var "Y")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k11_bvfunc_1 :::"O_el"::: ) (Set (Var "Y")))))))) ; theorem :: BVFUNC_2:10 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_partit1 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k11_bvfunc_1 :::"O_el"::: ) (Set (Var "Y")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k11_bvfunc_1 :::"O_el"::: ) (Set (Var "Y")))))))) ; theorem :: BVFUNC_2:11 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_partit1 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ) ($#r1_bvfunc_1 :::"'<'"::: ) (Set (Var "a"))))))) ; theorem :: BVFUNC_2:12 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_partit1 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set (Var "a")) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC_2:13 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_partit1 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ) ($#k5_bvfunc_1 :::"'or'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "b")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" )) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" (Set (Var "a")) ($#k5_bvfunc_1 :::"'or'"::: ) (Set (Var "b")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC_2:14 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_partit1 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" (Set (Var "a")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "b")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ) ($#r1_bvfunc_1 :::"'<'"::: ) (Set (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "b")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ))))))) ; theorem :: BVFUNC_2:15 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_bvfunc_2 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" (Set (Var "a")) ($#k2_bvfunc_1 :::"'&'"::: ) (Set (Var "b")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ) ($#r1_bvfunc_1 :::"'<'"::: ) (Set (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ) ($#k2_bvfunc_1 :::"'&'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "b")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ))))))) ; theorem :: BVFUNC_2:16 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_partit1 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ) ($#k6_bvfunc_1 :::"'xor'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "b")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" )) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" (Set (Var "a")) ($#k6_bvfunc_1 :::"'xor'"::: ) (Set (Var "b")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC_2:17 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_partit1 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "b")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" )) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" (Set (Var "a")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "b")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC_2:18 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_partit1 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC_2:19 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_partit1 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC_2:20 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_partit1 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "u")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "u")) ($#r3_bvfunc_2 :::"is_independent_of"::: ) (Set (Var "PA")) "," (Set (Var "G")))) "holds" (Bool (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" (Set (Var "u")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "a")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "u")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ))))))) ; theorem :: BVFUNC_2:21 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_partit1 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "u")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "u")) ($#r3_bvfunc_2 :::"is_independent_of"::: ) (Set (Var "PA")) "," (Set (Var "G")))) "holds" (Bool (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" (Set (Var "a")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "u")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "u")))))))) ; theorem :: BVFUNC_2:22 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_partit1 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "u")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "u")) ($#r3_bvfunc_2 :::"is_independent_of"::: ) (Set (Var "PA")) "," (Set (Var "G")))) "holds" (Bool (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" (Set (Var "u")) ($#k5_bvfunc_1 :::"'or'"::: ) (Set (Var "a")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "u")) ($#k5_bvfunc_1 :::"'or'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ))))))) ; theorem :: BVFUNC_2:23 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_partit1 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "u")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "u")) ($#r3_bvfunc_2 :::"is_independent_of"::: ) (Set (Var "PA")) "," (Set (Var "G")))) "holds" (Bool (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" (Set (Var "a")) ($#k5_bvfunc_1 :::"'or'"::: ) (Set (Var "u")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ) ($#k5_bvfunc_1 :::"'or'"::: ) (Set (Var "u")))))))) ; theorem :: BVFUNC_2:24 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_partit1 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "u")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "u")) ($#r3_bvfunc_2 :::"is_independent_of"::: ) (Set (Var "PA")) "," (Set (Var "G")))) "holds" (Bool (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" (Set (Var "a")) ($#k5_bvfunc_1 :::"'or'"::: ) (Set (Var "u")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ) ($#r1_bvfunc_1 :::"'<'"::: ) (Set (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ) ($#k5_bvfunc_1 :::"'or'"::: ) (Set (Var "u")))))))) ; theorem :: BVFUNC_2:25 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_partit1 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "u")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "u")) ($#r3_bvfunc_2 :::"is_independent_of"::: ) (Set (Var "PA")) "," (Set (Var "G")))) "holds" (Bool (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" (Set (Var "u")) ($#k2_bvfunc_1 :::"'&'"::: ) (Set (Var "a")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "u")) ($#k2_bvfunc_1 :::"'&'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ))))))) ; theorem :: BVFUNC_2:26 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_partit1 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "u")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "u")) ($#r3_bvfunc_2 :::"is_independent_of"::: ) (Set (Var "PA")) "," (Set (Var "G")))) "holds" (Bool (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" (Set (Var "a")) ($#k2_bvfunc_1 :::"'&'"::: ) (Set (Var "u")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ) ($#k2_bvfunc_1 :::"'&'"::: ) (Set (Var "u")))))))) ; theorem :: BVFUNC_2:27 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_partit1 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "a")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" (Set (Var "a")) ($#k2_bvfunc_1 :::"'&'"::: ) (Set (Var "u")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ) ($#r1_bvfunc_1 :::"'<'"::: ) (Set (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ) ($#k2_bvfunc_1 :::"'&'"::: ) (Set (Var "u")))))))) ; theorem :: BVFUNC_2:28 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_partit1 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "u")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "u")) ($#r3_bvfunc_2 :::"is_independent_of"::: ) (Set (Var "PA")) "," (Set (Var "G")))) "holds" (Bool (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" (Set (Var "u")) ($#k6_bvfunc_1 :::"'xor'"::: ) (Set (Var "a")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ) ($#r1_bvfunc_1 :::"'<'"::: ) (Set (Set (Var "u")) ($#k6_bvfunc_1 :::"'xor'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ))))))) ; theorem :: BVFUNC_2:29 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_partit1 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "u")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "u")) ($#r3_bvfunc_2 :::"is_independent_of"::: ) (Set (Var "PA")) "," (Set (Var "G")))) "holds" (Bool (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" (Set (Var "a")) ($#k6_bvfunc_1 :::"'xor'"::: ) (Set (Var "u")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ) ($#r1_bvfunc_1 :::"'<'"::: ) (Set (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ) ($#k6_bvfunc_1 :::"'xor'"::: ) (Set (Var "u")))))))) ; theorem :: BVFUNC_2:30 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_partit1 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "u")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "u")) ($#r3_bvfunc_2 :::"is_independent_of"::: ) (Set (Var "PA")) "," (Set (Var "G")))) "holds" (Bool (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" (Set (Var "u")) ($#k10_bvfunc_1 :::"'eqv'"::: ) (Set (Var "a")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ) ($#r1_bvfunc_1 :::"'<'"::: ) (Set (Set (Var "u")) ($#k10_bvfunc_1 :::"'eqv'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ))))))) ; theorem :: BVFUNC_2:31 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_partit1 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "u")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "u")) ($#r3_bvfunc_2 :::"is_independent_of"::: ) (Set (Var "PA")) "," (Set (Var "G")))) "holds" (Bool (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" (Set (Var "a")) ($#k10_bvfunc_1 :::"'eqv'"::: ) (Set (Var "u")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ) ($#r1_bvfunc_1 :::"'<'"::: ) (Set (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ) ($#k10_bvfunc_1 :::"'eqv'"::: ) (Set (Var "u")))))))) ; theorem :: BVFUNC_2:32 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_partit1 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "u")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "u")) ($#r3_bvfunc_2 :::"is_independent_of"::: ) (Set (Var "PA")) "," (Set (Var "G")))) "holds" (Bool (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" (Set (Var "u")) ($#k5_bvfunc_1 :::"'or'"::: ) (Set (Var "a")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "u")) ($#k5_bvfunc_1 :::"'or'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ))))))) ; theorem :: BVFUNC_2:33 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_partit1 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "u")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "u")) ($#r3_bvfunc_2 :::"is_independent_of"::: ) (Set (Var "PA")) "," (Set (Var "G")))) "holds" (Bool (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" (Set (Var "a")) ($#k5_bvfunc_1 :::"'or'"::: ) (Set (Var "u")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ) ($#k5_bvfunc_1 :::"'or'"::: ) (Set (Var "u")))))))) ; theorem :: BVFUNC_2:34 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_partit1 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "u")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "u")) ($#r3_bvfunc_2 :::"is_independent_of"::: ) (Set (Var "PA")) "," (Set (Var "G")))) "holds" (Bool (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" (Set (Var "u")) ($#k2_bvfunc_1 :::"'&'"::: ) (Set (Var "a")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "u")) ($#k2_bvfunc_1 :::"'&'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ))))))) ; theorem :: BVFUNC_2:35 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_partit1 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "u")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "u")) ($#r3_bvfunc_2 :::"is_independent_of"::: ) (Set (Var "PA")) "," (Set (Var "G")))) "holds" (Bool (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" (Set (Var "a")) ($#k2_bvfunc_1 :::"'&'"::: ) (Set (Var "u")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ) ($#k2_bvfunc_1 :::"'&'"::: ) (Set (Var "u")))))))) ; theorem :: BVFUNC_2:36 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_partit1 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "u")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set (Set (Var "u")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" )) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" (Set (Var "u")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "a")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC_2:37 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_partit1 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "a")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "u"))) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" (Set (Var "a")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "u")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC_2:38 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_partit1 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "u")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "u")) ($#r3_bvfunc_2 :::"is_independent_of"::: ) (Set (Var "PA")) "," (Set (Var "G")))) "holds" (Bool (Set (Set (Var "u")) ($#k6_bvfunc_1 :::"'xor'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" )) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" (Set (Var "u")) ($#k6_bvfunc_1 :::"'xor'"::: ) (Set (Var "a")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC_2:39 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_partit1 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "u")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "u")) ($#r3_bvfunc_2 :::"is_independent_of"::: ) (Set (Var "PA")) "," (Set (Var "G")))) "holds" (Bool (Set (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ) ($#k6_bvfunc_1 :::"'xor'"::: ) (Set (Var "u"))) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" (Set (Var "a")) ($#k6_bvfunc_1 :::"'xor'"::: ) (Set (Var "u")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" )))))) ;