:: BVFUNC11 semantic presentation begin theorem :: BVFUNC11:1 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) (Bool "for" (Set (Var "PA")) "," (Set (Var "PB")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "PA")) ($#r1_setfam_1 :::"'<'"::: ) (Set (Var "PB")))) "holds" (Bool (Set ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "z")) "," (Set (Var "PA")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "z")) "," (Set (Var "PB")) ")" ))))) ; theorem :: BVFUNC11:2 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) (Bool "for" (Set (Var "PA")) "," (Set (Var "PB")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "z")) "," (Set (Var "PA")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "z")) "," (Set "(" (Set (Var "PA")) ($#k3_partit1 :::"'\/'"::: ) (Set (Var "PB")) ")" ) ")" ))))) ; theorem :: BVFUNC11:3 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) (Bool "for" (Set (Var "PA")) "," (Set (Var "PB")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "z")) "," (Set "(" (Set (Var "PA")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "PB")) ")" ) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "z")) "," (Set (Var "PA")) ")" ))))) ; theorem :: BVFUNC11:4 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool "(" (Bool (Set ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "z")) "," (Set (Var "PA")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "z")) "," (Set "(" ($#k6_partit1 :::"%O"::: ) (Set (Var "Y")) ")" ) ")" )) & (Bool (Set ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "z")) "," (Set "(" ($#k10_eqrel_1 :::"%I"::: ) (Set (Var "Y")) ")" ) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "z")) "," (Set (Var "PA")) ")" )) ")" )))) ; theorem :: BVFUNC11: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")) ")" ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) ) & (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_tarski :::"}"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B")))) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool (Set (Var "a")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "b"))))))) ; theorem :: BVFUNC11: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")) ")" ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) ) & (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_tarski :::"}"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k2_bvfunc_2 :::"'/\'"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "B"))))))) ; theorem :: BVFUNC11: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_bvfunc_2 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_tarski :::"}"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "A")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "B")))))) ; begin theorem :: BVFUNC11:8 (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 "A")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "a")) ($#r1_bvfunc_1 :::"'<'"::: ) (Set (Var "b")))) "holds" (Bool (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) "," (Set (Var "G")) ")" ) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "b")) "," (Set (Var "A")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC11: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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) )) "holds" (Bool (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC11: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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC11:11 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) )) "holds" (Bool (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC11:12 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC11:13 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" )) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC11:14 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) )) "holds" (Bool (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC11:15 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) )) "holds" (Bool (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC11:16 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) )) "holds" (Bool (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC11:17 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) )) "holds" (Bool (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC11:18 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) )) "holds" (Bool (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" )) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC11:19 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC11:20 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC11:21 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC11:22 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) )) "holds" (Bool (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC11:23 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC11:24 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC11:25 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC11:26 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) )) "holds" (Bool (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ))))))) ; theorem :: BVFUNC11:27 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ))))))) ; theorem :: BVFUNC11:28 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ))))))) ; theorem :: BVFUNC11:29 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) )) "holds" (Bool (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ))))))) ; theorem :: BVFUNC11:30 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) )) "holds" (Bool (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ))))))) ; theorem :: BVFUNC11:31 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) )) "holds" (Bool (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ))))))) ; theorem :: BVFUNC11:32 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) )) "holds" (Bool (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" )) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ))))))) ; theorem :: BVFUNC11:33 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) )) "holds" (Bool (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" )) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ))))))) ; theorem :: BVFUNC11:34 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" )) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ))))))) ; theorem :: BVFUNC11:35 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) )) "holds" (Bool (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" )) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ))))))) ; theorem :: BVFUNC11:36 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) )) "holds" (Bool (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" )) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ))))))) ; theorem :: BVFUNC11:37 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" )) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ))))))) ; theorem :: BVFUNC11:38 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) )) "holds" (Bool (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" )) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC11:39 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) )) "holds" (Bool (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" )) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC11:40 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" )) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC11:41 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) )) "holds" (Bool (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" )) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC11:42 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) )) "holds" (Bool (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" )) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC11:43 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" )) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC11:44 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) )) "holds" (Bool (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC11:45 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) )) "holds" (Bool (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" )) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC11:46 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" )) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC11:47 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) )) "holds" (Bool (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" )) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC11:48 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) )) "holds" (Bool (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" )) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC11:49 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" )) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC11:50 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) )) "holds" (Bool (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC11:51 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) )) "holds" (Bool (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ))))))) ; theorem :: BVFUNC11:52 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ))))))) ; theorem :: BVFUNC11:53 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ))))))) ; theorem :: BVFUNC11:54 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) )) "holds" (Bool (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ))))))) ; theorem :: BVFUNC11:55 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) )) "holds" (Bool (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC11:56 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) )) "holds" (Bool (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC11:57 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) )) "holds" (Bool (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC11:58 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC11:59 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) )) "holds" (Bool (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC11:60 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) )) "holds" (Bool (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC11:61 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC11:62 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) )) "holds" (Bool (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC11:63 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) )) "holds" (Bool (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC11:64 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC11:65 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) )) "holds" (Bool (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC11:66 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) )) "holds" (Bool (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC11:67 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC11:68 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) )) "holds" (Bool (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC11:69 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) )) "holds" (Bool (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ))))))) ; theorem :: BVFUNC11:70 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) )) "holds" (Bool (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ))))))) ; theorem :: BVFUNC11:71 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ))))))) ; theorem :: BVFUNC11:72 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) )) "holds" (Bool (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ))))))) ; theorem :: BVFUNC11:73 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) )) "holds" (Bool (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC11:74 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) )) "holds" (Bool (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC11:75 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) )) "holds" (Bool (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC11:76 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC11:77 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) )) "holds" (Bool (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC11:78 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) )) "holds" (Bool (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC11:79 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC11:80 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) )) "holds" (Bool (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC11:81 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC11:82 (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 "A")) "," (Set (Var "B")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) )) "holds" (Bool (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ) "," (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "A")) "," (Set (Var "G")) ")" )))))) ;