:: BVFUNC_3 semantic presentation begin theorem :: BVFUNC_3: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 "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 (Var "a")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "b"))) ($#r1_bvfunc_1 :::"'<'"::: ) (Set (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (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")) ")" ")" ))))))) ; theorem :: BVFUNC_3: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 "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")) ")" ")" ) ($#k2_bvfunc_1 :::"'&'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "b")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" )) ($#r1_bvfunc_1 :::"'<'"::: ) (Set (Set (Var "a")) ($#k2_bvfunc_1 :::"'&'"::: ) (Set (Var "b")))))))) ; theorem :: BVFUNC_3: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 "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 (Var "a")) ($#k2_bvfunc_1 :::"'&'"::: ) (Set (Var "b"))) ($#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_3: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 "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 ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ) ($#k2_bvfunc_1 :::"'&'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "b")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ) ($#k5_bvfunc_1 :::"'or'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "b")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ))))))) ; theorem :: BVFUNC_3: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_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 "(" (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")) ")" ")" ) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ) ($#k5_bvfunc_1 :::"'or'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "b")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ))))))) ; theorem :: BVFUNC_3: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_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 (Set (Var "a")) ($#k5_bvfunc_1 :::"'or'"::: ) (Set (Var "b")))))))) ; theorem :: BVFUNC_3: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_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 "a")) ($#k5_bvfunc_1 :::"'or'"::: ) (Set (Var "b"))) ($#r1_bvfunc_1 :::"'<'"::: ) (Set (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ) ($#k5_bvfunc_1 :::"'or'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "b")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ))))))) ; theorem :: BVFUNC_3: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_bvfunc_2 :::"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 (Var "a")) ($#k6_bvfunc_1 :::"'xor'"::: ) (Set (Var "b"))) ($#r1_bvfunc_1 :::"'<'"::: ) (Set (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (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")) ")" ")" ) ")" ) ")" ) ($#k5_bvfunc_1 :::"'or'"::: ) (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (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 "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "b")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ) ")" ) ")" ))))))) ; theorem :: BVFUNC_3: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_bvfunc_2 :::"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")) ($#k5_bvfunc_1 :::"'or'"::: ) (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")) ")" ")" ) ($#k5_bvfunc_1 :::"'or'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "b")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ))))))) ; theorem :: BVFUNC_3: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_bvfunc_2 :::"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")) ($#k5_bvfunc_1 :::"'or'"::: ) (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")) ")" ")" ) ($#k5_bvfunc_1 :::"'or'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "b")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ))))))) ; theorem :: BVFUNC_3: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_bvfunc_2 :::"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")) ($#k5_bvfunc_1 :::"'or'"::: ) (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")) ")" ")" ) ($#k5_bvfunc_1 :::"'or'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "b")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ))))))) ; theorem :: BVFUNC_3: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_bvfunc_2 :::"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")) ")" ")" ) ($#k2_bvfunc_1 :::"'&'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "b")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" )) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" (Set (Var "a")) ($#k2_bvfunc_1 :::"'&'"::: ) (Set (Var "b")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC_3: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_bvfunc_2 :::"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")) ")" ")" ) ($#k2_bvfunc_1 :::"'&'"::: ) (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")) ($#k2_bvfunc_1 :::"'&'"::: ) (Set (Var "b")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC_3: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_bvfunc_2 :::"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 "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "b")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ))))))) ; theorem :: BVFUNC_3:15 (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_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 "(" ($#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")) ")" ")" ))))))) ; theorem :: BVFUNC_3: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_bvfunc_2 :::"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 "(" ($#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")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "b")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC_3: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_bvfunc_2 :::"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 (Var "a")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "b"))) ($#r1_bvfunc_1 :::"'<'"::: ) (Set (Set (Var "a")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "b")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ))))))) ; theorem :: BVFUNC_3: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_bvfunc_2 :::"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 (Var "a")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "b"))) ($#r1_bvfunc_1 :::"'<'"::: ) (Set (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "b")))))))) ; theorem :: BVFUNC_3: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_bvfunc_2 :::"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 ($#k7_bvfunc_2 :::"Ex"::: ) "(" (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 "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "b")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ))))))) ; theorem :: BVFUNC_3: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_bvfunc_2 :::"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 (Var "a")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ) ($#r1_bvfunc_1 :::"'<'"::: ) (Set (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "b")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" (Set (Var "a")) ($#k2_bvfunc_1 :::"'&'"::: ) (Set (Var "b")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ))))))) ; theorem :: BVFUNC_3: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_bvfunc_2 :::"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")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "a")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ) ($#r1_bvfunc_1 :::"'<'"::: ) (Set (Set (Var "u")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ))))))) ; theorem :: BVFUNC_3: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_bvfunc_2 :::"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")) ($#k9_bvfunc_1 :::"'imp'"::: ) (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")) ")" ")" ) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "u")))))))) ; theorem :: BVFUNC_3: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_bvfunc_2 :::"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")) ")" ")" ) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "b")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" (Set (Var "a")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "b")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC_3: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_bvfunc_2 :::"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")) ")" ")" ) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (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 "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "b")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ))))))) ; theorem :: BVFUNC_3: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_bvfunc_2 :::"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 (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (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")) ")" ")" ))))))) ; theorem :: BVFUNC_3: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_bvfunc_2 :::"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")) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ) ($#k5_bvfunc_1 :::"'or'"::: ) (Set (Var "b")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC_3: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_bvfunc_2 :::"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")) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" (Set (Var "a")) ($#k2_bvfunc_1 :::"'&'"::: ) (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "b")) ")" ) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ))))))) ; theorem :: BVFUNC_3: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_bvfunc_2 :::"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 ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" (Set (Var "a")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "b")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ) ($#k2_bvfunc_1 :::"'&'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" (Set (Var "a")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "b")) ")" ) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ) ")" ))))))) ; theorem :: BVFUNC_3: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_bvfunc_2 :::"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 ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" (Set (Var "a")) ($#k2_bvfunc_1 :::"'&'"::: ) (Set (Var "b")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ) ")" ) ($#k2_bvfunc_1 :::"'&'"::: ) (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" (Set (Var "a")) ($#k2_bvfunc_1 :::"'&'"::: ) (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "b")) ")" ) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ) ")" ) ")" ))))))) ; theorem :: BVFUNC_3: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_bvfunc_2 :::"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")) ")" ")" ) ($#k2_bvfunc_1 :::"'&'"::: ) (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 ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" (Set (Var "a")) ($#k2_bvfunc_1 :::"'&'"::: ) (Set (Var "b")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC_3: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_bvfunc_2 :::"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")) ")" ")" ) ($#k2_bvfunc_1 :::"'&'"::: ) (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (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 ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" (Set (Var "a")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "b")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ))))))) ; theorem :: BVFUNC_3: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_bvfunc_2 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "a")) "," (Set (Var "c")) "," (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 "(" (Set (Var "a")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "c")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ) ($#k2_bvfunc_1 :::"'&'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" (Set (Var "c")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "b")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" )) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" (Set (Var "a")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "b")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC_3: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_bvfunc_2 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "c")) "," (Set (Var "b")) "," (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 "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" (Set (Var "c")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "b")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ) ($#k2_bvfunc_1 :::"'&'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" (Set (Var "a")) ($#k2_bvfunc_1 :::"'&'"::: ) (Set (Var "c")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" )) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" (Set (Var "a")) ($#k2_bvfunc_1 :::"'&'"::: ) (Set (Var "b")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC_3: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_bvfunc_2 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "b")) "," (Set (Var "c")) "," (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 "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" (Set (Var "b")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "c")) ")" ) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ) ($#k2_bvfunc_1 :::"'&'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" (Set (Var "a")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "c")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" )) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" (Set (Var "a")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "b")) ")" ) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC_3: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_bvfunc_2 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "b")) "," (Set (Var "c")) "," (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 "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" (Set (Var "b")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "c")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ) ($#k2_bvfunc_1 :::"'&'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" (Set (Var "a")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "c")) ")" ) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" )) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" (Set (Var "a")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "b")) ")" ) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC_3: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_bvfunc_2 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "b")) "," (Set (Var "c")) "," (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 "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" (Set (Var "b")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "c")) ")" ) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ) ($#k2_bvfunc_1 :::"'&'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" (Set (Var "a")) ($#k2_bvfunc_1 :::"'&'"::: ) (Set (Var "c")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" )) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" (Set (Var "a")) ($#k2_bvfunc_1 :::"'&'"::: ) (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "b")) ")" ) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC_3: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_bvfunc_2 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "b")) "," (Set (Var "c")) "," (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 "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" (Set (Var "b")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "c")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ) ($#k2_bvfunc_1 :::"'&'"::: ) (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" (Set (Var "a")) ($#k2_bvfunc_1 :::"'&'"::: ) (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "c")) ")" ) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" )) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" (Set (Var "a")) ($#k2_bvfunc_1 :::"'&'"::: ) (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "b")) ")" ) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC_3: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_bvfunc_2 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "c")) "," (Set (Var "b")) "," (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 "(" (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "c")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ) ($#k2_bvfunc_1 :::"'&'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" (Set (Var "c")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "b")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ) ")" ) ($#k2_bvfunc_1 :::"'&'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" (Set (Var "c")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "a")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" )) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" (Set (Var "a")) ($#k2_bvfunc_1 :::"'&'"::: ) (Set (Var "b")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC_3: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_bvfunc_2 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "b")) "," (Set (Var "c")) "," (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 "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" (Set (Var "b")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "c")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ) ($#k2_bvfunc_1 :::"'&'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" (Set (Var "c")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" )) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" (Set (Var "a")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "b")) ")" ) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC_3:40 (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")) "," (Set (Var "c")) "," (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 "(" (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "b")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ) ($#k2_bvfunc_1 :::"'&'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" (Set (Var "b")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "c")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ) ")" ) ($#k2_bvfunc_1 :::"'&'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" (Set (Var "c")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "a")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" )) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" (Set (Var "a")) ($#k2_bvfunc_1 :::"'&'"::: ) (Set (Var "b")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" )))))) ; theorem :: BVFUNC_3:41 (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 "c")) "," (Set (Var "b")) "," (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 "(" (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "c")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ) ($#k2_bvfunc_1 :::"'&'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" (Set (Var "b")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "c")) ")" ) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" ) ")" ) ($#k2_bvfunc_1 :::"'&'"::: ) (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" (Set (Var "c")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "a")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" ")" )) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" (Set (Var "a")) ($#k2_bvfunc_1 :::"'&'"::: ) (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "b")) ")" ) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" )))))) ;