:: BVFUNC25 semantic presentation begin theorem :: BVFUNC25:1 (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"::: ) ) "holds" (Bool (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" (Set (Var "a")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "b")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "a")) ($#k2_bvfunc_1 :::"'&'"::: ) (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "b")) ")" ))))) ; theorem :: BVFUNC25:2 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "b")) ")" ) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ) ")" ) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set "(" (Set (Var "a")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "b")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k12_bvfunc_1 :::"I_el"::: ) (Set (Var "Y")))))) ; theorem :: BVFUNC25:3 (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"::: ) ) "holds" (Bool (Set (Set (Var "a")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "b"))) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "b")) ")" ) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ))))) ; theorem :: BVFUNC25:4 (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"::: ) ) "holds" (Bool (Set (Set (Var "a")) ($#k10_bvfunc_1 :::"'eqv'"::: ) (Set (Var "b"))) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ) ($#k10_bvfunc_1 :::"'eqv'"::: ) (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "b")) ")" ))))) ; theorem :: BVFUNC25:5 (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"::: ) ) "holds" (Bool (Set (Set (Var "a")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "b"))) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "a")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set "(" (Set (Var "a")) ($#k2_bvfunc_1 :::"'&'"::: ) (Set (Var "b")) ")" ))))) ; theorem :: BVFUNC25:6 (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"::: ) ) "holds" (Bool (Set (Set (Var "a")) ($#k10_bvfunc_1 :::"'eqv'"::: ) (Set (Var "b"))) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k5_bvfunc_1 :::"'or'"::: ) (Set (Var "b")) ")" ) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set "(" (Set (Var "a")) ($#k2_bvfunc_1 :::"'&'"::: ) (Set (Var "b")) ")" ))))) ; theorem :: BVFUNC25:7 (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"::: ) ) "holds" (Bool (Set (Set (Var "a")) ($#k10_bvfunc_1 :::"'eqv'"::: ) (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k11_bvfunc_1 :::"O_el"::: ) (Set (Var "Y")))))) ; theorem :: BVFUNC25: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")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set (Var "a")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set "(" (Set (Var "b")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "c")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "b")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set "(" (Set (Var "a")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "c")) ")" ))))) ; theorem :: BVFUNC25:9 (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")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set (Var "a")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set "(" (Set (Var "b")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "c")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "b")) ")" ) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set "(" (Set (Var "a")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "c")) ")" ))))) ; theorem :: BVFUNC25:10 (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"::: ) ) "holds" (Bool (Set (Set (Var "a")) ($#k10_bvfunc_1 :::"'eqv'"::: ) (Set (Var "b"))) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "a")) ($#k6_bvfunc_1 :::"'xor'"::: ) (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "b")) ")" ))))) ; theorem :: BVFUNC25:11 (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")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set (Var "a")) ($#k2_bvfunc_1 :::"'&'"::: ) (Set "(" (Set (Var "b")) ($#k6_bvfunc_1 :::"'xor'"::: ) (Set (Var "c")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k2_bvfunc_1 :::"'&'"::: ) (Set (Var "b")) ")" ) ($#k6_bvfunc_1 :::"'xor'"::: ) (Set "(" (Set (Var "a")) ($#k2_bvfunc_1 :::"'&'"::: ) (Set (Var "c")) ")" ))))) ; theorem :: BVFUNC25:12 (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"::: ) ) "holds" (Bool (Set (Set (Var "a")) ($#k10_bvfunc_1 :::"'eqv'"::: ) (Set (Var "b"))) ($#r2_funct_2 :::"="::: ) (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" (Set (Var "a")) ($#k6_bvfunc_1 :::"'xor'"::: ) (Set (Var "b")) ")" ))))) ; theorem :: BVFUNC25: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"::: ) ) "holds" (Bool (Set (Set (Var "a")) ($#k6_bvfunc_1 :::"'xor'"::: ) (Set (Var "a"))) ($#r2_funct_2 :::"="::: ) (Set ($#k11_bvfunc_1 :::"O_el"::: ) (Set (Var "Y")))))) ; theorem :: BVFUNC25: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"::: ) ) "holds" (Bool (Set (Set (Var "a")) ($#k6_bvfunc_1 :::"'xor'"::: ) (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k12_bvfunc_1 :::"I_el"::: ) (Set (Var "Y")))))) ; theorem :: BVFUNC25:15 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "b")) ")" ) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set "(" (Set (Var "b")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "a")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "b")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "a")))))) ; theorem :: BVFUNC25:16 (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"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k5_bvfunc_1 :::"'or'"::: ) (Set (Var "b")) ")" ) ($#k2_bvfunc_1 :::"'&'"::: ) (Set "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ) ($#k5_bvfunc_1 :::"'or'"::: ) (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "b")) ")" ) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ) ($#k2_bvfunc_1 :::"'&'"::: ) (Set (Var "b")) ")" ) ($#k5_bvfunc_1 :::"'or'"::: ) (Set "(" (Set (Var "a")) ($#k2_bvfunc_1 :::"'&'"::: ) (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "b")) ")" ) ")" ))))) ; theorem :: BVFUNC25:17 (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"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k2_bvfunc_1 :::"'&'"::: ) (Set (Var "b")) ")" ) ($#k5_bvfunc_1 :::"'or'"::: ) (Set "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ) ($#k2_bvfunc_1 :::"'&'"::: ) (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "b")) ")" ) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ) ($#k5_bvfunc_1 :::"'or'"::: ) (Set (Var "b")) ")" ) ($#k2_bvfunc_1 :::"'&'"::: ) (Set "(" (Set (Var "a")) ($#k5_bvfunc_1 :::"'or'"::: ) (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "b")) ")" ) ")" ))))) ; theorem :: BVFUNC25:18 (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")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set (Var "a")) ($#k6_bvfunc_1 :::"'xor'"::: ) (Set "(" (Set (Var "b")) ($#k6_bvfunc_1 :::"'xor'"::: ) (Set (Var "c")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k6_bvfunc_1 :::"'xor'"::: ) (Set (Var "b")) ")" ) ($#k6_bvfunc_1 :::"'xor'"::: ) (Set (Var "c")))))) ; theorem :: BVFUNC25:19 (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")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set (Var "a")) ($#k10_bvfunc_1 :::"'eqv'"::: ) (Set "(" (Set (Var "b")) ($#k10_bvfunc_1 :::"'eqv'"::: ) (Set (Var "c")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k10_bvfunc_1 :::"'eqv'"::: ) (Set (Var "b")) ")" ) ($#k10_bvfunc_1 :::"'eqv'"::: ) (Set (Var "c")))))) ; theorem :: BVFUNC25: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"::: ) ) "holds" (Bool (Set (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ) ")" ) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "a"))) ($#r2_funct_2 :::"="::: ) (Set ($#k12_bvfunc_1 :::"I_el"::: ) (Set (Var "Y")))))) ; theorem :: BVFUNC25:21 (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"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "a")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "b")) ")" ) ($#k2_bvfunc_1 :::"'&'"::: ) (Set (Var "a")) ")" ) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "b"))) ($#r2_funct_2 :::"="::: ) (Set ($#k12_bvfunc_1 :::"I_el"::: ) (Set (Var "Y")))))) ; theorem :: BVFUNC25: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"::: ) ) "holds" (Bool (Set (Set (Var "a")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "a")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k12_bvfunc_1 :::"I_el"::: ) (Set (Var "Y")))))) ; theorem :: BVFUNC25: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"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "a")) ")" ) ($#k10_bvfunc_1 :::"'eqv'"::: ) (Set (Var "a"))) ($#r2_funct_2 :::"="::: ) (Set ($#k12_bvfunc_1 :::"I_el"::: ) (Set (Var "Y")))))) ; theorem :: BVFUNC25:24 (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"::: ) ) "holds" (Bool (Set (Set (Var "a")) ($#k5_bvfunc_1 :::"'or'"::: ) (Set "(" (Set (Var "a")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "b")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k12_bvfunc_1 :::"I_el"::: ) (Set (Var "Y")))))) ; theorem :: BVFUNC25:25 (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")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "b")) ")" ) ($#k5_bvfunc_1 :::"'or'"::: ) (Set "(" (Set (Var "c")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "a")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k12_bvfunc_1 :::"I_el"::: ) (Set (Var "Y")))))) ; theorem :: BVFUNC25:26 (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"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "b")) ")" ) ($#k5_bvfunc_1 :::"'or'"::: ) (Set "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "b")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k12_bvfunc_1 :::"I_el"::: ) (Set (Var "Y")))))) ; theorem :: BVFUNC25:27 (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"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "b")) ")" ) ($#k5_bvfunc_1 :::"'or'"::: ) (Set "(" (Set (Var "a")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "b")) ")" ) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k12_bvfunc_1 :::"I_el"::: ) (Set (Var "Y")))))) ; theorem :: BVFUNC25:28 (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"::: ) ) "holds" (Bool (Set (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "b")) ")" ) ($#k10_bvfunc_1 :::"'eqv'"::: ) (Set "(" (Set (Var "b")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "a")) ")" ) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k12_bvfunc_1 :::"I_el"::: ) (Set (Var "Y")))))) ; theorem :: BVFUNC25:29 (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")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "b")) ")" ) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "c")) ")" ) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "b")) ")" ) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "b")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k12_bvfunc_1 :::"I_el"::: ) (Set (Var "Y")))))) ; theorem :: BVFUNC25:30 (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"::: ) ) "holds" (Bool (Set (Set (Var "a")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "b"))) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "a")) ($#k10_bvfunc_1 :::"'eqv'"::: ) (Set "(" (Set (Var "a")) ($#k2_bvfunc_1 :::"'&'"::: ) (Set (Var "b")) ")" ))))) ; theorem :: BVFUNC25:31 (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"::: ) ) "holds" (Bool "(" (Bool "(" (Bool (Set (Set (Var "a")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "b"))) ($#r2_funct_2 :::"="::: ) (Set ($#k12_bvfunc_1 :::"I_el"::: ) (Set (Var "Y")))) & (Bool (Set (Set (Var "b")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "a"))) ($#r2_funct_2 :::"="::: ) (Set ($#k12_bvfunc_1 :::"I_el"::: ) (Set (Var "Y")))) ")" ) "iff" (Bool (Set (Var "a")) ($#r2_funct_2 :::"="::: ) (Set (Var "b"))) ")" ))) ; theorem :: BVFUNC25: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"::: ) ) "holds" (Bool (Set (Var "a")) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "a")))))) ; theorem :: BVFUNC25:33 (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"::: ) ) "holds" (Bool (Set (Set (Var "a")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "b")) ")" ) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "a")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k12_bvfunc_1 :::"I_el"::: ) (Set (Var "Y")))))) ; theorem :: BVFUNC25:34 (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"::: ) ) "holds" (Bool (Set (Var "a")) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "b")) ")" ) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "a")))))) ; theorem :: BVFUNC25:35 (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"::: ) ) "holds" (Bool (Set (Var "a")) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "b")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "a")) ")" ) ($#k2_bvfunc_1 :::"'&'"::: ) (Set "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "b")) ")" ) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "a")) ")" ))))) ; theorem :: BVFUNC25:36 (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"::: ) ) "holds" (Bool (Set (Set (Var "a")) ($#k2_bvfunc_1 :::"'&'"::: ) (Set (Var "b"))) ($#r2_funct_2 :::"="::: ) (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" (Set (Var "a")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "b")) ")" ) ")" ))))) ; theorem :: BVFUNC25:37 (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"::: ) ) "holds" (Bool (Set (Set (Var "a")) ($#k5_bvfunc_1 :::"'or'"::: ) (Set (Var "b"))) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "b")))))) ; theorem :: BVFUNC25:38 (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"::: ) ) "holds" (Bool (Set (Set (Var "a")) ($#k5_bvfunc_1 :::"'or'"::: ) (Set (Var "b"))) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "b")) ")" ) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "b")))))) ; theorem :: BVFUNC25:39 (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"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "b")) ")" ) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set "(" (Set (Var "a")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "a")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k12_bvfunc_1 :::"I_el"::: ) (Set (Var "Y")))))) ; theorem :: BVFUNC25:40 (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")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set "(" (Set (Var "b")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "c")) ")" ) ")" ) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set "(" (Set "(" (Set (Var "d")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "b")) ")" ) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set "(" (Set (Var "a")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set "(" (Set (Var "d")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "c")) ")" ) ")" ) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k12_bvfunc_1 :::"I_el"::: ) (Set (Var "Y")))))) ; theorem :: BVFUNC25:41 (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")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "b")) ")" ) ($#k2_bvfunc_1 :::"'&'"::: ) (Set (Var "a")) ")" ) ($#k2_bvfunc_1 :::"'&'"::: ) (Set (Var "c")) ")" ) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "b"))) ($#r2_funct_2 :::"="::: ) (Set ($#k12_bvfunc_1 :::"I_el"::: ) (Set (Var "Y")))))) ; theorem :: BVFUNC25:42 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "b")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "c")) ")" ) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k2_bvfunc_1 :::"'&'"::: ) (Set (Var "b")) ")" ) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "c")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k12_bvfunc_1 :::"I_el"::: ) (Set (Var "Y")))))) ; theorem :: BVFUNC25:43 (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")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "a")) ($#k2_bvfunc_1 :::"'&'"::: ) (Set (Var "b")) ")" ) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "c")) ")" ) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k2_bvfunc_1 :::"'&'"::: ) (Set (Var "b")) ")" ) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set "(" (Set (Var "c")) ($#k2_bvfunc_1 :::"'&'"::: ) (Set (Var "b")) ")" ) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k12_bvfunc_1 :::"I_el"::: ) (Set (Var "Y")))))) ; theorem :: BVFUNC25:44 (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")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "b")) ")" ) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k2_bvfunc_1 :::"'&'"::: ) (Set (Var "c")) ")" ) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set "(" (Set (Var "b")) ($#k2_bvfunc_1 :::"'&'"::: ) (Set (Var "c")) ")" ) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k12_bvfunc_1 :::"I_el"::: ) (Set (Var "Y")))))) ; theorem :: BVFUNC25:45 (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")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "a")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "b")) ")" ) ($#k2_bvfunc_1 :::"'&'"::: ) (Set "(" (Set (Var "a")) ($#k2_bvfunc_1 :::"'&'"::: ) (Set (Var "c")) ")" ) ")" ) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set "(" (Set (Var "b")) ($#k2_bvfunc_1 :::"'&'"::: ) (Set (Var "c")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k12_bvfunc_1 :::"I_el"::: ) (Set (Var "Y")))))) ; theorem :: BVFUNC25:46 (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")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k2_bvfunc_1 :::"'&'"::: ) (Set "(" (Set (Var "a")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "b")) ")" ) ")" ) ($#k2_bvfunc_1 :::"'&'"::: ) (Set "(" (Set (Var "b")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "c")) ")" )) ($#r1_bvfunc_1 :::"'<'"::: ) (Set (Var "c"))))) ; theorem :: BVFUNC25:47 (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")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "a")) ($#k5_bvfunc_1 :::"'or'"::: ) (Set (Var "b")) ")" ) ($#k2_bvfunc_1 :::"'&'"::: ) (Set "(" (Set (Var "a")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "c")) ")" ) ")" ) ($#k2_bvfunc_1 :::"'&'"::: ) (Set "(" (Set (Var "b")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "c")) ")" )) ($#r1_bvfunc_1 :::"'<'"::: ) (Set (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set "(" (Set (Var "b")) ($#k5_bvfunc_1 :::"'or'"::: ) (Set (Var "c")) ")" ))))) ;