:: BVFUNC14 semantic presentation begin theorem :: BVFUNC14: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")) "holds" (Bool (Set ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "z")) "," (Set "(" (Set (Var "PA")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "PB")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "z")) "," (Set (Var "PA")) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "z")) "," (Set (Var "PB")) ")" ")" )))))) ; theorem :: BVFUNC14: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_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 ($#k2_bvfunc_2 :::"'/\'"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "B"))))))) ; theorem :: BVFUNC14: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 "B")) "," (Set (Var "C")) "," (Set (Var "D")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) ($#k1_enumset1 :::"}"::: ) )) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k2_bvfunc_2 :::"'/\'"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "B")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "C")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "D"))))))) ; theorem :: BVFUNC14: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")) "," (Set (Var "C")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#k1_enumset1 :::"}"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "A")))) "holds" (Bool (Set ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "A")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "C"))))))) ; theorem :: BVFUNC14: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")) "," (Set (Var "C")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#k1_enumset1 :::"}"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "C")))) "holds" (Bool (Set ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "B")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "C")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "A"))))))) ; theorem :: BVFUNC14: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")) "," (Set (Var "C")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#k1_enumset1 :::"}"::: ) )) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "A")))) "holds" (Bool (Set ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "C")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "B"))))))) ; theorem :: BVFUNC14: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")) "," (Set (Var "C")) "," (Set (Var "D")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) ($#k2_enumset1 :::"}"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "D")))) "holds" (Bool (Set ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "A")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "B")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "C")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "D"))))))) ; theorem :: BVFUNC14: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")) "," (Set (Var "C")) "," (Set (Var "D")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) ($#k2_enumset1 :::"}"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "D")))) "holds" (Bool (Set ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "B")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "C")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "D"))))))) ; theorem :: BVFUNC14: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")) "," (Set (Var "C")) "," (Set (Var "D")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) ($#k2_enumset1 :::"}"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "D")))) "holds" (Bool (Set ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "C")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "B")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "D"))))))) ; theorem :: BVFUNC14: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")) "," (Set (Var "C")) "," (Set (Var "D")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) ($#k2_enumset1 :::"}"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "D")))) "holds" (Bool (Set ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "D")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "C")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "B"))))))) ; theorem :: BVFUNC14:11 (Bool "for" (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "B")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "b")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "C")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "c")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "D")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "d")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) ($#k1_enumset1 :::"}"::: ) ))) ; theorem :: BVFUNC14:12 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "D")))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "C")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "c")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "D")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "d")) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set (Var "c"))))) ; theorem :: BVFUNC14:13 (Bool "for" (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "B")))) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "B")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "b")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "C")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "c")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "D")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "d")) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Var "b")))) ; theorem :: BVFUNC14:14 (Bool "for" (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "B")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "b")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "C")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "c")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "D")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "d")) ")" )))) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set ($#k1_enumset1 :::"{"::: ) (Set "(" (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "B")) ")" ) "," (Set "(" (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "C")) ")" ) "," (Set "(" (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "D")) ")" ) ($#k1_enumset1 :::"}"::: ) )))) ; theorem :: BVFUNC14: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")) "," (Set (Var "C")) "," (Set (Var "D")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) (Bool "for" (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "A9")) "," (Set (Var "B9")) "," (Set (Var "C9")) "," (Set (Var "D9")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "B")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "B9")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "C")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "C9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "D")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "D9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "A")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "A9")) ")" )))) "holds" (Bool "(" (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Var "B9"))) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set (Var "C9"))) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "D"))) ($#r1_hidden :::"="::: ) (Set (Var "D9"))) ")" ))))) ; theorem :: BVFUNC14:16 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "A9")) "," (Set (Var "B9")) "," (Set (Var "C9")) "," (Set (Var "D9")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "B")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "B9")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "C")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "C9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "D")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "D9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "A")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "A9")) ")" )))) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) ($#k2_enumset1 :::"}"::: ) ))))) ; theorem :: BVFUNC14: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")) "," (Set (Var "C")) "," (Set (Var "D")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) (Bool "for" (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "A9")) "," (Set (Var "B9")) "," (Set (Var "C9")) "," (Set (Var "D9")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) ($#k2_enumset1 :::"}"::: ) )) & (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "B")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "B9")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "C")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "C9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "D")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "D9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "A")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "A9")) ")" )))) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set "(" (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "A")) ")" ) "," (Set "(" (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "B")) ")" ) "," (Set "(" (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "C")) ")" ) "," (Set "(" (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "D")) ")" ) ($#k2_enumset1 :::"}"::: ) ))))))) ; theorem :: BVFUNC14: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")) "," (Set (Var "C")) "," (Set (Var "D")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) (Bool "for" (Set (Var "z")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) (Bool "for" (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) ) & (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) ($#k2_enumset1 :::"}"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "D")))) "holds" (Bool (Set ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "u")) "," (Set "(" (Set "(" (Set (Var "B")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "C")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "D")) ")" ) ")" ) ($#r1_xboole_0 :::"meets"::: ) (Set ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "z")) "," (Set (Var "A")) ")" ))))))) ; theorem :: BVFUNC14: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")) "," (Set (Var "C")) "," (Set (Var "D")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) (Bool "for" (Set (Var "z")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) ) & (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) ($#k2_enumset1 :::"}"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "z")) "," (Set "(" (Set (Var "C")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "D")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "u")) "," (Set "(" (Set (Var "C")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "D")) ")" ) ")" ))) "holds" (Bool (Set ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "u")) "," (Set "(" ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) ")" ) ($#r1_xboole_0 :::"meets"::: ) (Set ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "z")) "," (Set "(" ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) ")" )))))) ; theorem :: BVFUNC14: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")) "," (Set (Var "C")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) (Bool "for" (Set (Var "z")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) ) & (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#k1_enumset1 :::"}"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "A"))) & (Bool (Set ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "z")) "," (Set (Var "C")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "u")) "," (Set (Var "C")) ")" ))) "holds" (Bool (Set ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "u")) "," (Set "(" ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) ")" ) ($#r1_xboole_0 :::"meets"::: ) (Set ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "z")) "," (Set "(" ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) ")" )))))) ; theorem :: BVFUNC14: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 "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k3_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) ($#k3_enumset1 :::"}"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "E")))) "holds" (Bool (Set ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "A")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "B")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "C")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "D")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "E"))))))) ; theorem :: BVFUNC14: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 "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k3_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) ($#k3_enumset1 :::"}"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "E")))) "holds" (Bool (Set ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "B")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "A")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "C")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "D")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "E"))))))) ; theorem :: BVFUNC14: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")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k3_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) ($#k3_enumset1 :::"}"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "E")))) "holds" (Bool (Set ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "C")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "A")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "B")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "D")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "E"))))))) ; theorem :: BVFUNC14: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")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k3_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) ($#k3_enumset1 :::"}"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "E")))) "holds" (Bool (Set ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "D")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "A")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "B")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "C")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "E"))))))) ; theorem :: BVFUNC14: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")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k3_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) ($#k3_enumset1 :::"}"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "E")))) "holds" (Bool (Set ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "E")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "A")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "B")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "C")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "D"))))))) ; theorem :: BVFUNC14:26 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "A9")) "," (Set (Var "B9")) "," (Set (Var "C9")) "," (Set (Var "D9")) "," (Set (Var "E9")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "B")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "B9")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "C")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "C9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "D")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "D9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "E")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "E9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "A")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "A9")) ")" )))) "holds" (Bool "(" (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Var "A9"))) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Var "B9"))) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set (Var "C9"))) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "D"))) ($#r1_hidden :::"="::: ) (Set (Var "D9"))) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "E"))) ($#r1_hidden :::"="::: ) (Set (Var "E9"))) ")" )))) ; theorem :: BVFUNC14:27 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "A9")) "," (Set (Var "B9")) "," (Set (Var "C9")) "," (Set (Var "D9")) "," (Set (Var "E9")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "B")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "B9")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "C")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "C9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "D")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "D9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "E")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "E9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "A")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "A9")) ")" )))) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set ($#k3_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) ($#k3_enumset1 :::"}"::: ) ))))) ; theorem :: BVFUNC14:28 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "A9")) "," (Set (Var "B9")) "," (Set (Var "C9")) "," (Set (Var "D9")) "," (Set (Var "E9")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "B")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "B9")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "C")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "C9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "D")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "D9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "E")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "E9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "A")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "A9")) ")" )))) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set ($#k3_enumset1 :::"{"::: ) (Set "(" (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "A")) ")" ) "," (Set "(" (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "B")) ")" ) "," (Set "(" (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "C")) ")" ) "," (Set "(" (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "D")) ")" ) "," (Set "(" (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "E")) ")" ) ($#k3_enumset1 :::"}"::: ) ))))) ; theorem :: BVFUNC14: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")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) (Bool "for" (Set (Var "z")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) (Bool "for" (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) ) & (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k3_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) ($#k3_enumset1 :::"}"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "E")))) "holds" (Bool (Set ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "u")) "," (Set "(" (Set "(" (Set "(" (Set (Var "B")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "C")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "D")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "E")) ")" ) ")" ) ($#r1_xboole_0 :::"meets"::: ) (Set ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "z")) "," (Set (Var "A")) ")" ))))))) ; theorem :: BVFUNC14: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")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) (Bool "for" (Set (Var "z")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) ) & (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k3_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) ($#k3_enumset1 :::"}"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "z")) "," (Set "(" (Set "(" (Set (Var "C")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "D")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "E")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "u")) "," (Set "(" (Set "(" (Set (Var "C")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "D")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "E")) ")" ) ")" ))) "holds" (Bool (Set ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "u")) "," (Set "(" ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) ")" ) ($#r1_xboole_0 :::"meets"::: ) (Set ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "z")) "," (Set "(" ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) ")" )))))) ; theorem :: BVFUNC14: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")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k4_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) ($#k4_enumset1 :::"}"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "F")))) "holds" (Bool (Set ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "A")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "B")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "C")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "D")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "E")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "F"))))))) ; theorem :: BVFUNC14: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 "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k4_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) ($#k4_enumset1 :::"}"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "F")))) "holds" (Bool (Set ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "B")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "A")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "C")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "D")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "E")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "F"))))))) ; theorem :: BVFUNC14: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 "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k4_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) ($#k4_enumset1 :::"}"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "F")))) "holds" (Bool (Set ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "C")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "A")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "B")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "D")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "E")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "F"))))))) ; theorem :: BVFUNC14: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 "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k4_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) ($#k4_enumset1 :::"}"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "F")))) "holds" (Bool (Set ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "D")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "A")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "B")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "C")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "E")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "F"))))))) ; theorem :: BVFUNC14: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 "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k4_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) ($#k4_enumset1 :::"}"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "F")))) "holds" (Bool (Set ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "E")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "A")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "B")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "C")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "D")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "F"))))))) ; theorem :: BVFUNC14: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 "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k4_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) ($#k4_enumset1 :::"}"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "F")))) "holds" (Bool (Set ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "F")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "A")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "B")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "C")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "D")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "E"))))))) ; theorem :: BVFUNC14:37 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "A9")) "," (Set (Var "B9")) "," (Set (Var "C9")) "," (Set (Var "D9")) "," (Set (Var "E9")) "," (Set (Var "F9")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "B")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "B9")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "C")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "C9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "D")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "D9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "E")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "E9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "F")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "F9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "A")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "A9")) ")" )))) "holds" (Bool "(" (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Var "A9"))) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Var "B9"))) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set (Var "C9"))) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "D"))) ($#r1_hidden :::"="::: ) (Set (Var "D9"))) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "E"))) ($#r1_hidden :::"="::: ) (Set (Var "E9"))) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Var "F9"))) ")" )))) ; theorem :: BVFUNC14:38 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "A9")) "," (Set (Var "B9")) "," (Set (Var "C9")) "," (Set (Var "D9")) "," (Set (Var "E9")) "," (Set (Var "F9")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "B")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "B9")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "C")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "C9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "D")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "D9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "E")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "E9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "F")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "F9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "A")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "A9")) ")" )))) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set ($#k4_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) ($#k4_enumset1 :::"}"::: ) ))))) ; theorem :: BVFUNC14:39 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "A9")) "," (Set (Var "B9")) "," (Set (Var "C9")) "," (Set (Var "D9")) "," (Set (Var "E9")) "," (Set (Var "F9")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "B")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "B9")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "C")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "C9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "D")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "D9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "E")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "E9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "F")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "F9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "A")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "A9")) ")" )))) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set ($#k4_enumset1 :::"{"::: ) (Set "(" (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "A")) ")" ) "," (Set "(" (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "B")) ")" ) "," (Set "(" (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "C")) ")" ) "," (Set "(" (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "D")) ")" ) "," (Set "(" (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "E")) ")" ) "," (Set "(" (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "F")) ")" ) ($#k4_enumset1 :::"}"::: ) ))))) ; theorem :: BVFUNC14: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 "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) (Bool "for" (Set (Var "z")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) (Bool "for" (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) ) & (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k4_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) ($#k4_enumset1 :::"}"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "F")))) "holds" (Bool (Set ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "u")) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "B")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "C")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "D")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "E")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "F")) ")" ) ")" ) ($#r1_xboole_0 :::"meets"::: ) (Set ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "z")) "," (Set (Var "A")) ")" ))))))) ; theorem :: BVFUNC14: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 "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) (Bool "for" (Set (Var "z")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) (Bool "for" (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) ) & (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k4_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) ($#k4_enumset1 :::"}"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "z")) "," (Set "(" (Set "(" (Set "(" (Set (Var "C")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "D")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "E")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "F")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "u")) "," (Set "(" (Set "(" (Set "(" (Set (Var "C")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "D")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "E")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "F")) ")" ) ")" ))) "holds" (Bool (Set ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "u")) "," (Set "(" ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) ")" ) ($#r1_xboole_0 :::"meets"::: ) (Set ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "z")) "," (Set "(" ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) ")" ))))))) ; begin theorem :: BVFUNC14:42 (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")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k5_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) ($#k5_enumset1 :::"}"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "J")))) "holds" (Bool (Set ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "A")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "B")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "C")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "D")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "E")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "F")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "J"))))))) ; theorem :: BVFUNC14:43 (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")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k5_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) ($#k5_enumset1 :::"}"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "J")))) "holds" (Bool (Set ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "B")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "A")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "C")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "D")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "E")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "F")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "J"))))))) ; theorem :: BVFUNC14:44 (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")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k5_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) ($#k5_enumset1 :::"}"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "J")))) "holds" (Bool (Set ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "C")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "A")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "B")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "D")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "E")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "F")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "J"))))))) ; theorem :: BVFUNC14:45 (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")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k5_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) ($#k5_enumset1 :::"}"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "J")))) "holds" (Bool (Set ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "D")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "A")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "B")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "C")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "E")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "F")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "J"))))))) ; theorem :: BVFUNC14:46 (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")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k5_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) ($#k5_enumset1 :::"}"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "J")))) "holds" (Bool (Set ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "E")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "A")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "B")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "C")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "D")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "F")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "J"))))))) ; theorem :: BVFUNC14:47 (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")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k5_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) ($#k5_enumset1 :::"}"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "J")))) "holds" (Bool (Set ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "F")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "A")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "B")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "C")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "D")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "E")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "J"))))))) ; theorem :: BVFUNC14:48 (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")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k5_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) ($#k5_enumset1 :::"}"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "J")))) "holds" (Bool (Set ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "J")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "A")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "B")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "C")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "D")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "E")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "F"))))))) ; theorem :: BVFUNC14:49 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "A9")) "," (Set (Var "B9")) "," (Set (Var "C9")) "," (Set (Var "D9")) "," (Set (Var "E9")) "," (Set (Var "F9")) "," (Set (Var "J9")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "B")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "B9")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "C")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "C9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "D")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "D9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "E")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "E9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "F")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "F9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "J")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "J9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "A")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "A9")) ")" )))) "holds" (Bool "(" (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Var "A9"))) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Var "B9"))) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set (Var "C9"))) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "D"))) ($#r1_hidden :::"="::: ) (Set (Var "D9"))) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "E"))) ($#r1_hidden :::"="::: ) (Set (Var "E9"))) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Var "F9"))) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "J"))) ($#r1_hidden :::"="::: ) (Set (Var "J9"))) ")" )))) ; theorem :: BVFUNC14:50 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "A9")) "," (Set (Var "B9")) "," (Set (Var "C9")) "," (Set (Var "D9")) "," (Set (Var "E9")) "," (Set (Var "F9")) "," (Set (Var "J9")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "B")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "B9")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "C")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "C9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "D")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "D9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "E")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "E9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "F")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "F9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "J")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "J9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "A")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "A9")) ")" )))) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set ($#k5_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) ($#k5_enumset1 :::"}"::: ) ))))) ; theorem :: BVFUNC14:51 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "A9")) "," (Set (Var "B9")) "," (Set (Var "C9")) "," (Set (Var "D9")) "," (Set (Var "E9")) "," (Set (Var "F9")) "," (Set (Var "J9")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "B")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "B9")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "C")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "C9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "D")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "D9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "E")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "E9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "F")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "F9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "J")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "J9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "A")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "A9")) ")" )))) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set ($#k5_enumset1 :::"{"::: ) (Set "(" (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "A")) ")" ) "," (Set "(" (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "B")) ")" ) "," (Set "(" (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "C")) ")" ) "," (Set "(" (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "D")) ")" ) "," (Set "(" (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "E")) ")" ) "," (Set "(" (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "F")) ")" ) "," (Set "(" (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "J")) ")" ) ($#k5_enumset1 :::"}"::: ) ))))) ; theorem :: BVFUNC14:52 (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")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) (Bool "for" (Set (Var "z")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) ) & (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k5_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) ($#k5_enumset1 :::"}"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "J")))) "holds" (Bool (Set ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "u")) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "B")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "C")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "D")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "E")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "F")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "J")) ")" ) ")" ) ($#r1_xboole_0 :::"meets"::: ) (Set ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "z")) "," (Set (Var "A")) ")" )))))) ; theorem :: BVFUNC14:53 (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")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) (Bool "for" (Set (Var "z")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) ) & (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k5_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) ($#k5_enumset1 :::"}"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "z")) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "C")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "D")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "E")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "F")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "J")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "u")) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "C")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "D")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "E")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "F")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "J")) ")" ) ")" ))) "holds" (Bool (Set ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "u")) "," (Set "(" ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) ")" ) ($#r1_xboole_0 :::"meets"::: ) (Set ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "z")) "," (Set "(" ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) ")" )))))) ; theorem :: BVFUNC14:54 (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")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) "," (Set (Var "M")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k6_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) "," (Set (Var "M")) ($#k6_enumset1 :::"}"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "J")) ($#r1_hidden :::"<>"::: ) (Set (Var "M")))) "holds" (Bool (Set ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "A")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "B")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "C")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "D")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "E")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "F")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "J")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "M"))))))) ; theorem :: BVFUNC14:55 (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")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) "," (Set (Var "M")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k6_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) "," (Set (Var "M")) ($#k6_enumset1 :::"}"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "J")) ($#r1_hidden :::"<>"::: ) (Set (Var "M")))) "holds" (Bool (Set ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "B")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "A")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "C")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "D")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "E")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "F")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "J")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "M"))))))) ; theorem :: BVFUNC14:56 (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")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) "," (Set (Var "M")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k6_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) "," (Set (Var "M")) ($#k6_enumset1 :::"}"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "J")) ($#r1_hidden :::"<>"::: ) (Set (Var "M")))) "holds" (Bool (Set ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "C")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "A")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "B")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "D")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "E")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "F")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "J")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "M"))))))) ; theorem :: BVFUNC14:57 (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")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) "," (Set (Var "M")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k6_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) "," (Set (Var "M")) ($#k6_enumset1 :::"}"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "J")) ($#r1_hidden :::"<>"::: ) (Set (Var "M")))) "holds" (Bool (Set ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "D")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "A")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "B")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "C")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "E")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "F")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "J")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "M"))))))) ; theorem :: BVFUNC14:58 (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")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) "," (Set (Var "M")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k6_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) "," (Set (Var "M")) ($#k6_enumset1 :::"}"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "J")) ($#r1_hidden :::"<>"::: ) (Set (Var "M")))) "holds" (Bool (Set ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "E")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "A")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "B")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "C")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "D")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "F")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "J")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "M"))))))) ; theorem :: BVFUNC14:59 (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")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) "," (Set (Var "M")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k6_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) "," (Set (Var "M")) ($#k6_enumset1 :::"}"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "J")) ($#r1_hidden :::"<>"::: ) (Set (Var "M")))) "holds" (Bool (Set ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "F")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "A")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "B")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "C")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "D")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "E")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "J")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "M"))))))) ; theorem :: BVFUNC14:60 (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")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) "," (Set (Var "M")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k6_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) "," (Set (Var "M")) ($#k6_enumset1 :::"}"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "J")) ($#r1_hidden :::"<>"::: ) (Set (Var "M")))) "holds" (Bool (Set ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "J")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "A")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "B")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "C")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "D")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "E")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "F")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "M"))))))) ; theorem :: BVFUNC14:61 (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")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) "," (Set (Var "M")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k6_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) "," (Set (Var "M")) ($#k6_enumset1 :::"}"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "J")) ($#r1_hidden :::"<>"::: ) (Set (Var "M")))) "holds" (Bool (Set ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "M")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "A")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "B")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "C")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "D")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "E")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "F")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "J"))))))) ; theorem :: BVFUNC14:62 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) "," (Set (Var "M")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "A9")) "," (Set (Var "B9")) "," (Set (Var "C9")) "," (Set (Var "D9")) "," (Set (Var "E9")) "," (Set (Var "F9")) "," (Set (Var "J9")) "," (Set (Var "M9")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "J")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "B")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "B9")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "C")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "C9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "D")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "D9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "E")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "E9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "F")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "F9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "J")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "J9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "M")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "M9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "A")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "A9")) ")" )))) "holds" (Bool "(" (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Var "B9"))) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set (Var "C9"))) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "D"))) ($#r1_hidden :::"="::: ) (Set (Var "D9"))) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "E"))) ($#r1_hidden :::"="::: ) (Set (Var "E9"))) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Var "F9"))) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "J"))) ($#r1_hidden :::"="::: ) (Set (Var "J9"))) ")" )))) ; theorem :: BVFUNC14:63 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) "," (Set (Var "M")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "A9")) "," (Set (Var "B9")) "," (Set (Var "C9")) "," (Set (Var "D9")) "," (Set (Var "E9")) "," (Set (Var "F9")) "," (Set (Var "J9")) "," (Set (Var "M9")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "B")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "B9")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "C")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "C9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "D")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "D9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "E")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "E9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "F")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "F9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "J")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "J9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "M")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "M9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "A")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "A9")) ")" )))) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set ($#k6_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) "," (Set (Var "M")) ($#k6_enumset1 :::"}"::: ) ))))) ; theorem :: BVFUNC14:64 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) "," (Set (Var "M")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "A9")) "," (Set (Var "B9")) "," (Set (Var "C9")) "," (Set (Var "D9")) "," (Set (Var "E9")) "," (Set (Var "F9")) "," (Set (Var "J9")) "," (Set (Var "M9")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "B")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "B9")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "C")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "C9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "D")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "D9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "E")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "E9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "F")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "F9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "J")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "J9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "M")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "M9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "A")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "A9")) ")" )))) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set ($#k6_enumset1 :::"{"::: ) (Set "(" (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "A")) ")" ) "," (Set "(" (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "B")) ")" ) "," (Set "(" (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "C")) ")" ) "," (Set "(" (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "D")) ")" ) "," (Set "(" (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "E")) ")" ) "," (Set "(" (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "F")) ")" ) "," (Set "(" (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "J")) ")" ) "," (Set "(" (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "M")) ")" ) ($#k6_enumset1 :::"}"::: ) ))))) ; theorem :: BVFUNC14:65 (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")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) "," (Set (Var "M")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) (Bool "for" (Set (Var "z")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) ) & (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k6_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) "," (Set (Var "M")) ($#k6_enumset1 :::"}"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "J")) ($#r1_hidden :::"<>"::: ) (Set (Var "M")))) "holds" (Bool (Set (Set "(" ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "u")) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "B")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "C")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "D")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "E")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "F")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "J")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "M")) ")" ) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "z")) "," (Set (Var "A")) ")" ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))))) ; theorem :: BVFUNC14:66 (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")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) "," (Set (Var "M")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) (Bool "for" (Set (Var "z")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) ) & (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k6_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) "," (Set (Var "M")) ($#k6_enumset1 :::"}"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "J")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "z")) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "C")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "D")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "E")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "F")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "J")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "M")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "u")) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "C")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "D")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "E")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "F")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "J")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "M")) ")" ) ")" ))) "holds" (Bool (Set ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "u")) "," (Set "(" ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) ")" ) ($#r1_xboole_0 :::"meets"::: ) (Set ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "z")) "," (Set "(" ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) ")" )))))) ; theorem :: BVFUNC14:67 (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")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) "," (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k7_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) "," (Set (Var "M")) "," (Set (Var "N")) ($#k7_enumset1 :::"}"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "J")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "J")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "M")) ($#r1_hidden :::"<>"::: ) (Set (Var "N")))) "holds" (Bool (Set ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "A")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "B")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "C")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "D")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "E")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "F")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "J")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "M")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "N"))))))) ; theorem :: BVFUNC14:68 (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")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) "," (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k7_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) "," (Set (Var "M")) "," (Set (Var "N")) ($#k7_enumset1 :::"}"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "J")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "J")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "M")) ($#r1_hidden :::"<>"::: ) (Set (Var "N")))) "holds" (Bool (Set ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "B")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "A")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "C")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "D")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "E")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "F")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "J")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "M")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "N"))))))) ; theorem :: BVFUNC14:69 (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")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) "," (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k7_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) "," (Set (Var "M")) "," (Set (Var "N")) ($#k7_enumset1 :::"}"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "J")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "J")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "M")) ($#r1_hidden :::"<>"::: ) (Set (Var "N")))) "holds" (Bool (Set ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "C")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "A")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "B")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "D")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "E")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "F")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "J")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "M")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "N"))))))) ; theorem :: BVFUNC14:70 (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")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) "," (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k7_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) "," (Set (Var "M")) "," (Set (Var "N")) ($#k7_enumset1 :::"}"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "J")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "J")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "M")) ($#r1_hidden :::"<>"::: ) (Set (Var "N")))) "holds" (Bool (Set ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "D")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "A")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "B")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "C")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "E")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "F")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "J")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "M")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "N"))))))) ; theorem :: BVFUNC14:71 (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")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) "," (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k7_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) "," (Set (Var "M")) "," (Set (Var "N")) ($#k7_enumset1 :::"}"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "J")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "J")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "M")) ($#r1_hidden :::"<>"::: ) (Set (Var "N")))) "holds" (Bool (Set ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "E")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "A")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "B")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "C")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "D")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "F")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "J")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "M")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "N"))))))) ; theorem :: BVFUNC14:72 (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")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) "," (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k7_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) "," (Set (Var "M")) "," (Set (Var "N")) ($#k7_enumset1 :::"}"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "J")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "J")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "M")) ($#r1_hidden :::"<>"::: ) (Set (Var "N")))) "holds" (Bool (Set ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "F")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "A")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "B")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "C")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "D")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "E")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "J")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "M")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "N"))))))) ; theorem :: BVFUNC14:73 (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")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) "," (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k7_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) "," (Set (Var "M")) "," (Set (Var "N")) ($#k7_enumset1 :::"}"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "J")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "J")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "M")) ($#r1_hidden :::"<>"::: ) (Set (Var "N")))) "holds" (Bool (Set ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "J")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "A")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "B")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "C")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "D")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "E")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "F")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "M")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "N"))))))) ; theorem :: BVFUNC14:74 (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")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) "," (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k7_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) "," (Set (Var "M")) "," (Set (Var "N")) ($#k7_enumset1 :::"}"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "J")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "J")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "M")) ($#r1_hidden :::"<>"::: ) (Set (Var "N")))) "holds" (Bool (Set ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "M")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "A")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "B")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "C")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "D")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "E")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "F")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "J")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "N"))))))) ; theorem :: BVFUNC14:75 (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")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) "," (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k7_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) "," (Set (Var "M")) "," (Set (Var "N")) ($#k7_enumset1 :::"}"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "J")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "J")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "M")) ($#r1_hidden :::"<>"::: ) (Set (Var "N")))) "holds" (Bool (Set ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "N")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "A")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "B")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "C")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "D")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "E")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "F")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "J")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "M"))))))) ; theorem :: BVFUNC14:76 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) "," (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "A9")) "," (Set (Var "B9")) "," (Set (Var "C9")) "," (Set (Var "D9")) "," (Set (Var "E9")) "," (Set (Var "F9")) "," (Set (Var "J9")) "," (Set (Var "M9")) "," (Set (Var "N9")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "J")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "J")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "M")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "B")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "B9")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "C")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "C9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "D")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "D9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "E")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "E9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "F")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "F9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "J")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "J9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "M")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "M9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "N")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "N9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "A")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "A9")) ")" )))) "holds" (Bool "(" (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Var "A9"))) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Var "B9"))) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set (Var "C9"))) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "D"))) ($#r1_hidden :::"="::: ) (Set (Var "D9"))) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "E"))) ($#r1_hidden :::"="::: ) (Set (Var "E9"))) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Var "F9"))) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "J"))) ($#r1_hidden :::"="::: ) (Set (Var "J9"))) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set (Var "M9"))) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set (Var "N9"))) ")" )))) ; theorem :: BVFUNC14:77 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) "," (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "A9")) "," (Set (Var "B9")) "," (Set (Var "C9")) "," (Set (Var "D9")) "," (Set (Var "E9")) "," (Set (Var "F9")) "," (Set (Var "J9")) "," (Set (Var "M9")) "," (Set (Var "N9")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "B")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "B9")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "C")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "C9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "D")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "D9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "E")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "E9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "F")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "F9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "J")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "J9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "M")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "M9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "N")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "N9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "A")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "A9")) ")" )))) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set ($#k7_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) "," (Set (Var "M")) "," (Set (Var "N")) ($#k7_enumset1 :::"}"::: ) ))))) ; theorem :: BVFUNC14:78 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) "," (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "A9")) "," (Set (Var "B9")) "," (Set (Var "C9")) "," (Set (Var "D9")) "," (Set (Var "E9")) "," (Set (Var "F9")) "," (Set (Var "J9")) "," (Set (Var "M9")) "," (Set (Var "N9")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "B")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "B9")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "C")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "C9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "D")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "D9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "E")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "E9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "F")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "F9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "J")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "J9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "M")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "M9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "N")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "N9")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "A")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "A9")) ")" )))) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set ($#k7_enumset1 :::"{"::: ) (Set "(" (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "A")) ")" ) "," (Set "(" (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "B")) ")" ) "," (Set "(" (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "C")) ")" ) "," (Set "(" (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "D")) ")" ) "," (Set "(" (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "E")) ")" ) "," (Set "(" (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "F")) ")" ) "," (Set "(" (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "J")) ")" ) "," (Set "(" (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "M")) ")" ) "," (Set "(" (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "N")) ")" ) ($#k7_enumset1 :::"}"::: ) ))))) ; theorem :: BVFUNC14:79 (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")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) "," (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) (Bool "for" (Set (Var "z")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) ) & (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k7_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) "," (Set (Var "M")) "," (Set (Var "N")) ($#k7_enumset1 :::"}"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "J")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "J")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "M")) ($#r1_hidden :::"<>"::: ) (Set (Var "N")))) "holds" (Bool (Set (Set "(" ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "u")) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "B")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "C")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "D")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "E")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "F")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "J")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "M")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "N")) ")" ) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "z")) "," (Set (Var "A")) ")" ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))))) ; theorem :: BVFUNC14:80 (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")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) "," (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) (Bool "for" (Set (Var "z")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) ) & (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k7_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "J")) "," (Set (Var "M")) "," (Set (Var "N")) ($#k7_enumset1 :::"}"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "D"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "E"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "E")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "J"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "J")) ($#r1_hidden :::"<>"::: ) (Set (Var "M"))) & (Bool (Set (Var "J")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "M")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "z")) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "C")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "D")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "E")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "F")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "J")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "M")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "N")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "u")) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "C")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "D")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "E")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "F")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "J")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "M")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "N")) ")" ) ")" ))) "holds" (Bool (Set ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "u")) "," (Set "(" ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "A")) "," (Set (Var "G")) ")" ")" ) ")" ) ($#r1_xboole_0 :::"meets"::: ) (Set ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "z")) "," (Set "(" ($#k5_bvfunc_2 :::"CompF"::: ) "(" (Set (Var "B")) "," (Set (Var "G")) ")" ")" ) ")" )))))) ;