:: XREGULAR  semantic presentation begin  

























theorem :: XREGULAR:1 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )   (Bool  "ex" (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "Y"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Var "Y"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "X")))  ")" ))) ; 
 
theorem :: XREGULAR:2 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )   (Bool  "ex" (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "Y"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool  "("   "for" (Set (Var "Y1")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "Y1"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y")))) "holds"  (Bool (Set (Var "Y1"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "X")))  ")" )  ")" ))) ; 
 
theorem :: XREGULAR:3 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )   (Bool  "ex" (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "Y"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool  "("   "for" (Set (Var "Y1")) "," (Set (Var "Y2")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "Y1"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y2"))) & (Bool (Set (Var "Y2"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y")))) "holds"  (Bool (Set (Var "Y1"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "X")))  ")" )  ")" ))) ; 
 
theorem :: XREGULAR:4 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )   (Bool  "ex" (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "Y"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool  "("   "for" (Set (Var "Y1")) "," (Set (Var "Y2")) "," (Set (Var "Y3")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "Y1"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y2"))) & (Bool (Set (Var "Y2"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y3"))) & (Bool (Set (Var "Y3"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y")))) "holds"  (Bool (Set (Var "Y1"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "X")))  ")" )  ")" ))) ; 
 
theorem :: XREGULAR:5 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )   (Bool  "ex" (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "Y"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool  "("   "for" (Set (Var "Y1")) "," (Set (Var "Y2")) "," (Set (Var "Y3")) "," (Set (Var "Y4")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "Y1"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y2"))) & (Bool (Set (Var "Y2"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y3"))) & (Bool (Set (Var "Y3"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y4"))) & (Bool (Set (Var "Y4"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y")))) "holds"  (Bool (Set (Var "Y1"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "X")))  ")" )  ")" ))) ; 
 
theorem :: XREGULAR:6 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )   (Bool  "ex" (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "Y"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool  "("   "for" (Set (Var "Y1")) "," (Set (Var "Y2")) "," (Set (Var "Y3")) "," (Set (Var "Y4")) "," (Set (Var "Y5")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "Y1"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y2"))) & (Bool (Set (Var "Y2"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y3"))) & (Bool (Set (Var "Y3"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y4"))) & (Bool (Set (Var "Y4"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y5"))) & (Bool (Set (Var "Y5"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y")))) "holds"  (Bool (Set (Var "Y1"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "X")))  ")" )  ")" ))) ; 
 
theorem :: XREGULAR:7 (Bool  "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "being"    ($#m1_hidden :::"set"::: )    "holds"  (Bool  "("   "not" (Bool (Set (Var "X1"))  ($#r2_hidden :::"in"::: )  (Set (Var "X2"))) "or"  "not" (Bool (Set (Var "X2"))  ($#r2_hidden :::"in"::: )  (Set (Var "X3"))) "or"  "not" (Bool (Set (Var "X3"))  ($#r2_hidden :::"in"::: )  (Set (Var "X1")))  ")" )) ; 
 
theorem :: XREGULAR:8 (Bool  "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) "being"    ($#m1_hidden :::"set"::: )    "holds"  (Bool  "("   "not" (Bool (Set (Var "X1"))  ($#r2_hidden :::"in"::: )  (Set (Var "X2"))) "or"  "not" (Bool (Set (Var "X2"))  ($#r2_hidden :::"in"::: )  (Set (Var "X3"))) "or"  "not" (Bool (Set (Var "X3"))  ($#r2_hidden :::"in"::: )  (Set (Var "X4"))) "or"  "not" (Bool (Set (Var "X4"))  ($#r2_hidden :::"in"::: )  (Set (Var "X1")))  ")" )) ; 
 
theorem :: XREGULAR:9 (Bool  "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) "," (Set (Var "X5")) "being"    ($#m1_hidden :::"set"::: )    "holds"  (Bool  "("   "not" (Bool (Set (Var "X1"))  ($#r2_hidden :::"in"::: )  (Set (Var "X2"))) "or"  "not" (Bool (Set (Var "X2"))  ($#r2_hidden :::"in"::: )  (Set (Var "X3"))) "or"  "not" (Bool (Set (Var "X3"))  ($#r2_hidden :::"in"::: )  (Set (Var "X4"))) "or"  "not" (Bool (Set (Var "X4"))  ($#r2_hidden :::"in"::: )  (Set (Var "X5"))) "or"  "not" (Bool (Set (Var "X5"))  ($#r2_hidden :::"in"::: )  (Set (Var "X1")))  ")" )) ; 
 
theorem :: XREGULAR:10 (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  "("   "not" (Bool (Set (Var "X1"))  ($#r2_hidden :::"in"::: )  (Set (Var "X2"))) "or"  "not" (Bool (Set (Var "X2"))  ($#r2_hidden :::"in"::: )  (Set (Var "X3"))) "or"  "not" (Bool (Set (Var "X3"))  ($#r2_hidden :::"in"::: )  (Set (Var "X4"))) "or"  "not" (Bool (Set (Var "X4"))  ($#r2_hidden :::"in"::: )  (Set (Var "X5"))) "or"  "not" (Bool (Set (Var "X5"))  ($#r2_hidden :::"in"::: )  (Set (Var "X6"))) "or"  "not" (Bool (Set (Var "X6"))  ($#r2_hidden :::"in"::: )  (Set (Var "X1")))  ")" )) ;