:: ENUMSET1 semantic presentation begin definitionlet "x1", "x2", "x3" be ($#m1_hidden :::"set"::: ) ; func :::"{":::"x1" "," "x2" "," "x3":::"}"::: -> ($#m1_hidden :::"set"::: ) means :: ENUMSET1:def 1 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) "x1") "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) "x2") "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) "x3") ")" ) ")" )); end; :: deftheorem defines :::"{"::: ENUMSET1:def 1 : (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "b4")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k1_enumset1 :::"}"::: ) )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b4"))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x1"))) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x2"))) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x3"))) ")" ) ")" )) ")" )); definitionlet "x1", "x2", "x3", "x4" be ($#m1_hidden :::"set"::: ) ; func :::"{":::"x1" "," "x2" "," "x3" "," "x4":::"}"::: -> ($#m1_hidden :::"set"::: ) means :: ENUMSET1:def 2 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) "x1") "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) "x2") "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) "x3") "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) "x4") ")" ) ")" )); end; :: deftheorem defines :::"{"::: ENUMSET1:def 2 : (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "b5")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k2_enumset1 :::"}"::: ) )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b5"))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x1"))) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x2"))) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x3"))) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x4"))) ")" ) ")" )) ")" )); definitionlet "x1", "x2", "x3", "x4", "x5" be ($#m1_hidden :::"set"::: ) ; func :::"{":::"x1" "," "x2" "," "x3" "," "x4" "," "x5":::"}"::: -> ($#m1_hidden :::"set"::: ) means :: ENUMSET1:def 3 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) "x1") "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) "x2") "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) "x3") "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) "x4") "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) "x5") ")" ) ")" )); end; :: deftheorem defines :::"{"::: ENUMSET1:def 3 : (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "b6")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set ($#k3_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) ($#k3_enumset1 :::"}"::: ) )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b6"))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x1"))) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x2"))) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x3"))) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x4"))) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x5"))) ")" ) ")" )) ")" )); definitionlet "x1", "x2", "x3", "x4", "x5", "x6" be ($#m1_hidden :::"set"::: ) ; func :::"{":::"x1" "," "x2" "," "x3" "," "x4" "," "x5" "," "x6":::"}"::: -> ($#m1_hidden :::"set"::: ) means :: ENUMSET1:def 4 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) "x1") "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) "x2") "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) "x3") "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) "x4") "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) "x5") "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) "x6") ")" ) ")" )); end; :: deftheorem defines :::"{"::: ENUMSET1:def 4 : (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "b7")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b7")) ($#r1_hidden :::"="::: ) (Set ($#k4_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) ($#k4_enumset1 :::"}"::: ) )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b7"))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x1"))) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x2"))) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x3"))) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x4"))) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x5"))) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x6"))) ")" ) ")" )) ")" )); definitionlet "x1", "x2", "x3", "x4", "x5", "x6", "x7" be ($#m1_hidden :::"set"::: ) ; func :::"{":::"x1" "," "x2" "," "x3" "," "x4" "," "x5" "," "x6" "," "x7":::"}"::: -> ($#m1_hidden :::"set"::: ) means :: ENUMSET1:def 5 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) "x1") "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) "x2") "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) "x3") "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) "x4") "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) "x5") "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) "x6") "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) "x7") ")" ) ")" )); end; :: deftheorem defines :::"{"::: ENUMSET1:def 5 : (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "," (Set (Var "b8")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b8")) ($#r1_hidden :::"="::: ) (Set ($#k5_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) ($#k5_enumset1 :::"}"::: ) )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b8"))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x1"))) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x2"))) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x3"))) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x4"))) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x5"))) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x6"))) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x7"))) ")" ) ")" )) ")" )); definitionlet "x1", "x2", "x3", "x4", "x5", "x6", "x7", "x8" be ($#m1_hidden :::"set"::: ) ; func :::"{":::"x1" "," "x2" "," "x3" "," "x4" "," "x5" "," "x6" "," "x7" "," "x8":::"}"::: -> ($#m1_hidden :::"set"::: ) means :: ENUMSET1:def 6 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) "x1") "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) "x2") "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) "x3") "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) "x4") "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) "x5") "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) "x6") "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) "x7") "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) "x8") ")" ) ")" )); end; :: deftheorem defines :::"{"::: ENUMSET1:def 6 : (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "," (Set (Var "x8")) "," (Set (Var "b9")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b9")) ($#r1_hidden :::"="::: ) (Set ($#k6_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "," (Set (Var "x8")) ($#k6_enumset1 :::"}"::: ) )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b9"))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x1"))) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x2"))) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x3"))) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x4"))) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x5"))) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x6"))) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x7"))) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x8"))) ")" ) ")" )) ")" )); definitionlet "x1", "x2", "x3", "x4", "x5", "x6", "x7", "x8", "x9" be ($#m1_hidden :::"set"::: ) ; func :::"{":::"x1" "," "x2" "," "x3" "," "x4" "," "x5" "," "x6" "," "x7" "," "x8" "," "x9":::"}"::: -> ($#m1_hidden :::"set"::: ) means :: ENUMSET1:def 7 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) "x1") "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) "x2") "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) "x3") "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) "x4") "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) "x5") "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) "x6") "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) "x7") "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) "x8") "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) "x9") ")" ) ")" )); end; :: deftheorem defines :::"{"::: ENUMSET1:def 7 : (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "," (Set (Var "x8")) "," (Set (Var "x9")) "," (Set (Var "b10")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b10")) ($#r1_hidden :::"="::: ) (Set ($#k7_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "," (Set (Var "x8")) "," (Set (Var "x9")) ($#k7_enumset1 :::"}"::: ) )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b10"))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x1"))) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x2"))) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x3"))) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x4"))) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x5"))) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x6"))) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x7"))) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x8"))) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x9"))) ")" ) ")" )) ")" )); definitionlet "x1", "x2", "x3", "x4", "x5", "x6", "x7", "x8", "x9", "x10" be ($#m1_hidden :::"set"::: ) ; func :::"{":::"x1" "," "x2" "," "x3" "," "x4" "," "x5" "," "x6" "," "x7" "," "x8" "," "x9" "," "x10":::"}"::: -> ($#m1_hidden :::"set"::: ) means :: ENUMSET1:def 8 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) "x1") "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) "x2") "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) "x3") "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) "x4") "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) "x5") "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) "x6") "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) "x7") "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) "x8") "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) "x9") "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) "x10") ")" ) ")" )); end; :: deftheorem defines :::"{"::: ENUMSET1:def 8 : (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "," (Set (Var "x8")) "," (Set (Var "x9")) "," (Set (Var "x10")) "," (Set (Var "b11")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b11")) ($#r1_hidden :::"="::: ) (Set ($#k8_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "," (Set (Var "x8")) "," (Set (Var "x9")) "," (Set (Var "x10")) ($#k8_enumset1 :::"}"::: ) )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b11"))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x1"))) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x2"))) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x3"))) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x4"))) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x5"))) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x6"))) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x7"))) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x8"))) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x9"))) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x10"))) ")" ) ")" )) ")" )); theorem :: ENUMSET1:1 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_tarski :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k2_tarski :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_tarski :::"{"::: ) (Set (Var "x1")) ($#k1_tarski :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x2")) ($#k1_tarski :::"}"::: ) )))) ; theorem :: ENUMSET1:2 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k1_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_tarski :::"{"::: ) (Set (Var "x1")) ($#k1_tarski :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "x2")) "," (Set (Var "x3")) ($#k2_tarski :::"}"::: ) )))) ; theorem :: ENUMSET1:3 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k1_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_tarski :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k2_tarski :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x3")) ($#k1_tarski :::"}"::: ) )))) ; theorem :: ENUMSET1:4 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k2_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_tarski :::"{"::: ) (Set (Var "x1")) ($#k1_tarski :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k1_enumset1 :::"}"::: ) )))) ; theorem :: ENUMSET1:5 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k2_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_tarski :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k2_tarski :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "x3")) "," (Set (Var "x4")) ($#k2_tarski :::"}"::: ) )))) ; theorem :: ENUMSET1:6 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k2_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k1_enumset1 :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x4")) ($#k1_tarski :::"}"::: ) )))) ; theorem :: ENUMSET1:7 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) ($#k3_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_tarski :::"{"::: ) (Set (Var "x1")) ($#k1_tarski :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) ($#k2_enumset1 :::"}"::: ) )))) ; theorem :: ENUMSET1:8 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) ($#k3_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_tarski :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k2_tarski :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) ($#k1_enumset1 :::"}"::: ) )))) ; theorem :: ENUMSET1:9 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) ($#k3_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k1_enumset1 :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "x4")) "," (Set (Var "x5")) ($#k2_tarski :::"}"::: ) )))) ; theorem :: ENUMSET1:10 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) ($#k3_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k2_enumset1 :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x5")) ($#k1_tarski :::"}"::: ) )))) ; theorem :: ENUMSET1:11 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) ($#k4_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_tarski :::"{"::: ) (Set (Var "x1")) ($#k1_tarski :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k3_enumset1 :::"{"::: ) (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) ($#k3_enumset1 :::"}"::: ) )))) ; theorem :: ENUMSET1:12 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) ($#k4_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_tarski :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k2_tarski :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) ($#k2_enumset1 :::"}"::: ) )))) ; theorem :: ENUMSET1:13 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) ($#k4_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k1_enumset1 :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) ($#k1_enumset1 :::"}"::: ) )))) ; theorem :: ENUMSET1:14 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) ($#k4_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k2_enumset1 :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "x5")) "," (Set (Var "x6")) ($#k2_tarski :::"}"::: ) )))) ; theorem :: ENUMSET1:15 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) ($#k4_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k3_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) ($#k3_enumset1 :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x6")) ($#k1_tarski :::"}"::: ) )))) ; theorem :: ENUMSET1:16 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k5_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) ($#k5_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_tarski :::"{"::: ) (Set (Var "x1")) ($#k1_tarski :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k4_enumset1 :::"{"::: ) (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) ($#k4_enumset1 :::"}"::: ) )))) ; theorem :: ENUMSET1:17 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k5_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) ($#k5_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_tarski :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k2_tarski :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k3_enumset1 :::"{"::: ) (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) ($#k3_enumset1 :::"}"::: ) )))) ; theorem :: ENUMSET1:18 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k5_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) ($#k5_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k1_enumset1 :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) ($#k2_enumset1 :::"}"::: ) )))) ; theorem :: ENUMSET1:19 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k5_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) ($#k5_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k2_enumset1 :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) ($#k1_enumset1 :::"}"::: ) )))) ; theorem :: ENUMSET1:20 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k5_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) ($#k5_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k3_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) ($#k3_enumset1 :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "x6")) "," (Set (Var "x7")) ($#k2_tarski :::"}"::: ) )))) ; theorem :: ENUMSET1:21 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k5_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) ($#k5_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k4_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) ($#k4_enumset1 :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x7")) ($#k1_tarski :::"}"::: ) )))) ; theorem :: ENUMSET1:22 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "," (Set (Var "x8")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k6_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "," (Set (Var "x8")) ($#k6_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_tarski :::"{"::: ) (Set (Var "x1")) ($#k1_tarski :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k5_enumset1 :::"{"::: ) (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "," (Set (Var "x8")) ($#k5_enumset1 :::"}"::: ) )))) ; theorem :: ENUMSET1:23 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "," (Set (Var "x8")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k6_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "," (Set (Var "x8")) ($#k6_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_tarski :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k2_tarski :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k4_enumset1 :::"{"::: ) (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "," (Set (Var "x8")) ($#k4_enumset1 :::"}"::: ) )))) ; theorem :: ENUMSET1:24 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "," (Set (Var "x8")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k6_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "," (Set (Var "x8")) ($#k6_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k1_enumset1 :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k3_enumset1 :::"{"::: ) (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "," (Set (Var "x8")) ($#k3_enumset1 :::"}"::: ) )))) ; theorem :: ENUMSET1:25 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "," (Set (Var "x8")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k6_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "," (Set (Var "x8")) ($#k6_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k2_enumset1 :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "," (Set (Var "x8")) ($#k2_enumset1 :::"}"::: ) )))) ; theorem :: ENUMSET1:26 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "," (Set (Var "x8")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k6_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "," (Set (Var "x8")) ($#k6_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k3_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) ($#k3_enumset1 :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "x6")) "," (Set (Var "x7")) "," (Set (Var "x8")) ($#k1_enumset1 :::"}"::: ) )))) ; theorem :: ENUMSET1:27 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "," (Set (Var "x8")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k6_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "," (Set (Var "x8")) ($#k6_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k4_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) ($#k4_enumset1 :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "x7")) "," (Set (Var "x8")) ($#k2_tarski :::"}"::: ) )))) ; theorem :: ENUMSET1:28 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "," (Set (Var "x8")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k6_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "," (Set (Var "x8")) ($#k6_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k5_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) ($#k5_enumset1 :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x8")) ($#k1_tarski :::"}"::: ) )))) ; theorem :: ENUMSET1:29 (Bool "for" (Set (Var "x1")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_tarski :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x1")) ($#k2_tarski :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x1")) ($#k1_tarski :::"}"::: ) ))) ; theorem :: ENUMSET1:30 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x2")) ($#k1_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k2_tarski :::"}"::: ) ))) ; theorem :: ENUMSET1:31 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k2_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k1_enumset1 :::"}"::: ) ))) ; theorem :: ENUMSET1:32 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k3_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k2_enumset1 :::"}"::: ) ))) ; theorem :: ENUMSET1:33 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) ($#k4_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k3_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) ($#k3_enumset1 :::"}"::: ) ))) ; theorem :: ENUMSET1:34 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k5_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) ($#k5_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) ($#k4_enumset1 :::"}"::: ) ))) ; theorem :: ENUMSET1:35 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k6_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) ($#k6_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k5_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) ($#k5_enumset1 :::"}"::: ) ))) ; theorem :: ENUMSET1:36 (Bool "for" (Set (Var "x1")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x1")) ($#k1_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x1")) ($#k1_tarski :::"}"::: ) ))) ; theorem :: ENUMSET1:37 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x2")) ($#k2_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k2_tarski :::"}"::: ) ))) ; theorem :: ENUMSET1:38 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k3_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k1_enumset1 :::"}"::: ) ))) ; theorem :: ENUMSET1:39 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k4_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k2_enumset1 :::"}"::: ) ))) ; theorem :: ENUMSET1:40 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k5_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) ($#k5_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k3_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) ($#k3_enumset1 :::"}"::: ) ))) ; theorem :: ENUMSET1:41 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k6_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) ($#k6_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) ($#k4_enumset1 :::"}"::: ) ))) ; theorem :: ENUMSET1:42 (Bool "for" (Set (Var "x1")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x1")) ($#k2_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x1")) ($#k1_tarski :::"}"::: ) ))) ; theorem :: ENUMSET1:43 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x2")) ($#k3_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k2_tarski :::"}"::: ) ))) ; theorem :: ENUMSET1:44 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k4_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k1_enumset1 :::"}"::: ) ))) ; theorem :: ENUMSET1:45 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k5_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k5_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k2_enumset1 :::"}"::: ) ))) ; theorem :: ENUMSET1:46 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k6_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) ($#k6_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k3_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) ($#k3_enumset1 :::"}"::: ) ))) ; theorem :: ENUMSET1:47 (Bool "for" (Set (Var "x1")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x1")) ($#k3_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x1")) ($#k1_tarski :::"}"::: ) ))) ; theorem :: ENUMSET1:48 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x2")) ($#k4_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k2_tarski :::"}"::: ) ))) ; theorem :: ENUMSET1:49 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k5_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k5_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k1_enumset1 :::"}"::: ) ))) ; theorem :: ENUMSET1:50 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k6_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k6_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k2_enumset1 :::"}"::: ) ))) ; theorem :: ENUMSET1:51 (Bool "for" (Set (Var "x1")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x1")) ($#k4_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x1")) ($#k1_tarski :::"}"::: ) ))) ; theorem :: ENUMSET1:52 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k5_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x2")) ($#k5_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k2_tarski :::"}"::: ) ))) ; theorem :: ENUMSET1:53 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k6_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k6_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k1_enumset1 :::"}"::: ) ))) ; theorem :: ENUMSET1:54 (Bool "for" (Set (Var "x1")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k5_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x1")) ($#k5_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x1")) ($#k1_tarski :::"}"::: ) ))) ; theorem :: ENUMSET1:55 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k6_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x2")) ($#k6_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k2_tarski :::"}"::: ) ))) ; theorem :: ENUMSET1:56 (Bool "for" (Set (Var "x1")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k6_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x1")) "," (Set (Var "x1")) ($#k6_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x1")) ($#k1_tarski :::"}"::: ) ))) ; theorem :: ENUMSET1:57 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k1_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x3")) "," (Set (Var "x2")) ($#k1_enumset1 :::"}"::: ) ))) ; theorem :: ENUMSET1:58 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k1_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "x2")) "," (Set (Var "x1")) "," (Set (Var "x3")) ($#k1_enumset1 :::"}"::: ) ))) ; theorem :: ENUMSET1:59 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k1_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x1")) ($#k1_enumset1 :::"}"::: ) ))) ; theorem :: ENUMSET1:60 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k1_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "x3")) "," (Set (Var "x2")) "," (Set (Var "x1")) ($#k1_enumset1 :::"}"::: ) ))) ; theorem :: ENUMSET1:61 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k2_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x4")) "," (Set (Var "x3")) ($#k2_enumset1 :::"}"::: ) ))) ; theorem :: ENUMSET1:62 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k2_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x3")) "," (Set (Var "x2")) "," (Set (Var "x4")) ($#k2_enumset1 :::"}"::: ) ))) ; theorem :: ENUMSET1:63 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k2_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x2")) ($#k2_enumset1 :::"}"::: ) ))) ; theorem :: ENUMSET1:64 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k2_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x4")) "," (Set (Var "x3")) "," (Set (Var "x2")) ($#k2_enumset1 :::"}"::: ) ))) ; theorem :: ENUMSET1:65 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k2_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "x2")) "," (Set (Var "x1")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k2_enumset1 :::"}"::: ) ))) ; theorem :: ENUMSET1:66 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k2_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "x2")) "," (Set (Var "x1")) "," (Set (Var "x4")) "," (Set (Var "x3")) ($#k2_enumset1 :::"}"::: ) ))) ; theorem :: ENUMSET1:67 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k2_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x1")) "," (Set (Var "x4")) ($#k2_enumset1 :::"}"::: ) ))) ; theorem :: ENUMSET1:68 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k2_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x1")) ($#k2_enumset1 :::"}"::: ) ))) ; theorem :: ENUMSET1:69 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k2_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "x2")) "," (Set (Var "x4")) "," (Set (Var "x1")) "," (Set (Var "x3")) ($#k2_enumset1 :::"}"::: ) ))) ; theorem :: ENUMSET1:70 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k2_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "x2")) "," (Set (Var "x4")) "," (Set (Var "x3")) "," (Set (Var "x1")) ($#k2_enumset1 :::"}"::: ) ))) ; theorem :: ENUMSET1:71 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k2_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "x3")) "," (Set (Var "x2")) "," (Set (Var "x1")) "," (Set (Var "x4")) ($#k2_enumset1 :::"}"::: ) ))) ; theorem :: ENUMSET1:72 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k2_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "x3")) "," (Set (Var "x2")) "," (Set (Var "x4")) "," (Set (Var "x1")) ($#k2_enumset1 :::"}"::: ) ))) ; theorem :: ENUMSET1:73 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k2_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x1")) "," (Set (Var "x2")) ($#k2_enumset1 :::"}"::: ) ))) ; theorem :: ENUMSET1:74 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k2_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x2")) "," (Set (Var "x1")) ($#k2_enumset1 :::"}"::: ) ))) ; theorem :: ENUMSET1:75 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k2_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "x4")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x1")) ($#k2_enumset1 :::"}"::: ) ))) ; theorem :: ENUMSET1:76 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k2_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "x4")) "," (Set (Var "x3")) "," (Set (Var "x2")) "," (Set (Var "x1")) ($#k2_enumset1 :::"}"::: ) ))) ; theorem :: ENUMSET1:77 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "," (Set (Var "x8")) "," (Set (Var "x9")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k7_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "," (Set (Var "x8")) "," (Set (Var "x9")) ($#k7_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_tarski :::"{"::: ) (Set (Var "x1")) ($#k1_tarski :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k6_enumset1 :::"{"::: ) (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "," (Set (Var "x8")) "," (Set (Var "x9")) ($#k6_enumset1 :::"}"::: ) )))) ; theorem :: ENUMSET1:78 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "," (Set (Var "x8")) "," (Set (Var "x9")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k7_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "," (Set (Var "x8")) "," (Set (Var "x9")) ($#k7_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_tarski :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k2_tarski :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k5_enumset1 :::"{"::: ) (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "," (Set (Var "x8")) "," (Set (Var "x9")) ($#k5_enumset1 :::"}"::: ) )))) ; theorem :: ENUMSET1:79 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "," (Set (Var "x8")) "," (Set (Var "x9")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k7_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "," (Set (Var "x8")) "," (Set (Var "x9")) ($#k7_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k1_enumset1 :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k4_enumset1 :::"{"::: ) (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "," (Set (Var "x8")) "," (Set (Var "x9")) ($#k4_enumset1 :::"}"::: ) )))) ; theorem :: ENUMSET1:80 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "," (Set (Var "x8")) "," (Set (Var "x9")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k7_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "," (Set (Var "x8")) "," (Set (Var "x9")) ($#k7_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k2_enumset1 :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k3_enumset1 :::"{"::: ) (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "," (Set (Var "x8")) "," (Set (Var "x9")) ($#k3_enumset1 :::"}"::: ) )))) ; theorem :: ENUMSET1:81 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "," (Set (Var "x8")) "," (Set (Var "x9")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k7_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "," (Set (Var "x8")) "," (Set (Var "x9")) ($#k7_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k3_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) ($#k3_enumset1 :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "x6")) "," (Set (Var "x7")) "," (Set (Var "x8")) "," (Set (Var "x9")) ($#k2_enumset1 :::"}"::: ) )))) ; theorem :: ENUMSET1:82 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "," (Set (Var "x8")) "," (Set (Var "x9")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k7_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "," (Set (Var "x8")) "," (Set (Var "x9")) ($#k7_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k4_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) ($#k4_enumset1 :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "x7")) "," (Set (Var "x8")) "," (Set (Var "x9")) ($#k1_enumset1 :::"}"::: ) )))) ; theorem :: ENUMSET1:83 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "," (Set (Var "x8")) "," (Set (Var "x9")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k7_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "," (Set (Var "x8")) "," (Set (Var "x9")) ($#k7_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k5_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) ($#k5_enumset1 :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "x8")) "," (Set (Var "x9")) ($#k2_tarski :::"}"::: ) )))) ; theorem :: ENUMSET1:84 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "," (Set (Var "x8")) "," (Set (Var "x9")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k7_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "," (Set (Var "x8")) "," (Set (Var "x9")) ($#k7_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k6_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "," (Set (Var "x8")) ($#k6_enumset1 :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x9")) ($#k1_tarski :::"}"::: ) )))) ; theorem :: ENUMSET1:85 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "," (Set (Var "x8")) "," (Set (Var "x9")) "," (Set (Var "x10")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k8_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "," (Set (Var "x8")) "," (Set (Var "x9")) "," (Set (Var "x10")) ($#k8_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k7_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "," (Set (Var "x8")) "," (Set (Var "x9")) ($#k7_enumset1 :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x10")) ($#k1_tarski :::"}"::: ) )))) ; begin theorem :: ENUMSET1:86 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "z")))) "holds" (Bool (Set (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k1_enumset1 :::"}"::: ) ) ($#k4_xboole_0 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k2_tarski :::"}"::: ) ))) ; theorem :: ENUMSET1:87 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set ($#k2_tarski :::"{"::: ) (Set (Var "x2")) "," (Set (Var "x1")) ($#k2_tarski :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "x3")) "," (Set (Var "x1")) ($#k2_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k1_enumset1 :::"}"::: ) ))) ;