:: DECOMP_1 semantic presentation begin definitionlet "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; mode :::"alpha-set"::: "of" "T" -> ($#m1_subset_1 :::"Subset":::) "of" "T" means :: DECOMP_1:def 1 (Bool it ($#r1_tarski :::"c="::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) it ")" ) ")" ))); let "IT" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); attr "IT" is :::"semi-open"::: means :: DECOMP_1:def 2 (Bool "IT" ($#r1_tarski :::"c="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) "IT" ")" ))); attr "IT" is :::"pre-open"::: means :: DECOMP_1:def 3 (Bool "IT" ($#r1_tarski :::"c="::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) "IT" ")" ))); attr "IT" is :::"pre-semi-open"::: means :: DECOMP_1:def 4 (Bool "IT" ($#r1_tarski :::"c="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) "IT" ")" ) ")" ))); attr "IT" is :::"semi-pre-open"::: means :: DECOMP_1:def 5 (Bool "IT" ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) "IT" ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) "IT" ")" ) ")" ))); end; :: deftheorem defines :::"alpha-set"::: DECOMP_1:def 1 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_decomp_1 :::"alpha-set"::: ) "of" (Set (Var "T"))) "iff" (Bool (Set (Var "b2")) ($#r1_tarski :::"c="::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "b2")) ")" ) ")" ))) ")" ))); :: deftheorem defines :::"semi-open"::: DECOMP_1:def 2 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_decomp_1 :::"semi-open"::: ) ) "iff" (Bool (Set (Var "IT")) ($#r1_tarski :::"c="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "IT")) ")" ))) ")" ))); :: deftheorem defines :::"pre-open"::: DECOMP_1:def 3 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_decomp_1 :::"pre-open"::: ) ) "iff" (Bool (Set (Var "IT")) ($#r1_tarski :::"c="::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "IT")) ")" ))) ")" ))); :: deftheorem defines :::"pre-semi-open"::: DECOMP_1:def 4 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v3_decomp_1 :::"pre-semi-open"::: ) ) "iff" (Bool (Set (Var "IT")) ($#r1_tarski :::"c="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "IT")) ")" ) ")" ))) ")" ))); :: deftheorem defines :::"semi-pre-open"::: DECOMP_1:def 5 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v4_decomp_1 :::"semi-pre-open"::: ) ) "iff" (Bool (Set (Var "IT")) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "IT")) ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "IT")) ")" ) ")" ))) ")" ))); definitionlet "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "B" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); func :::"sInt"::: "B" -> ($#m1_subset_1 :::"Subset":::) "of" "T" equals :: DECOMP_1:def 6 (Set "B" ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) "B" ")" ) ")" )); func :::"pInt"::: "B" -> ($#m1_subset_1 :::"Subset":::) "of" "T" equals :: DECOMP_1:def 7 (Set "B" ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) "B" ")" ) ")" )); func :::"alphaInt"::: "B" -> ($#m1_subset_1 :::"Subset":::) "of" "T" equals :: DECOMP_1:def 8 (Set "B" ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) "B" ")" ) ")" ) ")" )); func :::"psInt"::: "B" -> ($#m1_subset_1 :::"Subset":::) "of" "T" equals :: DECOMP_1:def 9 (Set "B" ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) "B" ")" ) ")" ) ")" )); end; :: deftheorem defines :::"sInt"::: DECOMP_1:def 6 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k1_decomp_1 :::"sInt"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "B")) ")" ) ")" ))))); :: deftheorem defines :::"pInt"::: DECOMP_1:def 7 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k2_decomp_1 :::"pInt"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "B")) ")" ) ")" ))))); :: deftheorem defines :::"alphaInt"::: DECOMP_1:def 8 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k3_decomp_1 :::"alphaInt"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "B")) ")" ) ")" ) ")" ))))); :: deftheorem defines :::"psInt"::: DECOMP_1:def 9 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k4_decomp_1 :::"psInt"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "B")) ")" ) ")" ) ")" ))))); definitionlet "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "B" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); func :::"spInt"::: "B" -> ($#m1_subset_1 :::"Subset":::) "of" "T" equals :: DECOMP_1:def 10 (Set (Set "(" ($#k1_decomp_1 :::"sInt"::: ) "B" ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k2_decomp_1 :::"pInt"::: ) "B" ")" )); end; :: deftheorem defines :::"spInt"::: DECOMP_1:def 10 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k5_decomp_1 :::"spInt"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_decomp_1 :::"sInt"::: ) (Set (Var "B")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k2_decomp_1 :::"pInt"::: ) (Set (Var "B")) ")" ))))); definitionlet "T" be ($#l1_pre_topc :::"TopSpace":::); func "T" :::"^alpha"::: -> ($#m1_subset_1 :::"Subset-Family":::) "of" "T" equals :: DECOMP_1:def 11 "{" (Set (Var "B")) where B "is" ($#m1_subset_1 :::"Subset":::) "of" "T" : (Bool (Set (Var "B")) "is" ($#m1_decomp_1 :::"alpha-set"::: ) "of" "T") "}" ; func :::"SO"::: "T" -> ($#m1_subset_1 :::"Subset-Family":::) "of" "T" equals :: DECOMP_1:def 12 "{" (Set (Var "B")) where B "is" ($#m1_subset_1 :::"Subset":::) "of" "T" : (Bool (Set (Var "B")) "is" ($#v1_decomp_1 :::"semi-open"::: ) ) "}" ; func :::"PO"::: "T" -> ($#m1_subset_1 :::"Subset-Family":::) "of" "T" equals :: DECOMP_1:def 13 "{" (Set (Var "B")) where B "is" ($#m1_subset_1 :::"Subset":::) "of" "T" : (Bool (Set (Var "B")) "is" ($#v2_decomp_1 :::"pre-open"::: ) ) "}" ; func :::"SPO"::: "T" -> ($#m1_subset_1 :::"Subset-Family":::) "of" "T" equals :: DECOMP_1:def 14 "{" (Set (Var "B")) where B "is" ($#m1_subset_1 :::"Subset":::) "of" "T" : (Bool (Set (Var "B")) "is" ($#v4_decomp_1 :::"semi-pre-open"::: ) ) "}" ; func :::"PSO"::: "T" -> ($#m1_subset_1 :::"Subset-Family":::) "of" "T" equals :: DECOMP_1:def 15 "{" (Set (Var "B")) where B "is" ($#m1_subset_1 :::"Subset":::) "of" "T" : (Bool (Set (Var "B")) "is" ($#v3_decomp_1 :::"pre-semi-open"::: ) ) "}" ; func :::"D(c,alpha)"::: "T" -> ($#m1_subset_1 :::"Subset-Family":::) "of" "T" equals :: DECOMP_1:def 16 "{" (Set (Var "B")) where B "is" ($#m1_subset_1 :::"Subset":::) "of" "T" : (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k3_decomp_1 :::"alphaInt"::: ) (Set (Var "B")))) "}" ; func :::"D(c,p)"::: "T" -> ($#m1_subset_1 :::"Subset-Family":::) "of" "T" equals :: DECOMP_1:def 17 "{" (Set (Var "B")) where B "is" ($#m1_subset_1 :::"Subset":::) "of" "T" : (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k2_decomp_1 :::"pInt"::: ) (Set (Var "B")))) "}" ; func :::"D(c,s)"::: "T" -> ($#m1_subset_1 :::"Subset-Family":::) "of" "T" equals :: DECOMP_1:def 18 "{" (Set (Var "B")) where B "is" ($#m1_subset_1 :::"Subset":::) "of" "T" : (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k1_decomp_1 :::"sInt"::: ) (Set (Var "B")))) "}" ; func :::"D(c,ps)"::: "T" -> ($#m1_subset_1 :::"Subset-Family":::) "of" "T" equals :: DECOMP_1:def 19 "{" (Set (Var "B")) where B "is" ($#m1_subset_1 :::"Subset":::) "of" "T" : (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k4_decomp_1 :::"psInt"::: ) (Set (Var "B")))) "}" ; func :::"D(alpha,p)"::: "T" -> ($#m1_subset_1 :::"Subset-Family":::) "of" "T" equals :: DECOMP_1:def 20 "{" (Set (Var "B")) where B "is" ($#m1_subset_1 :::"Subset":::) "of" "T" : (Bool (Set ($#k3_decomp_1 :::"alphaInt"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k2_decomp_1 :::"pInt"::: ) (Set (Var "B")))) "}" ; func :::"D(alpha,s)"::: "T" -> ($#m1_subset_1 :::"Subset-Family":::) "of" "T" equals :: DECOMP_1:def 21 "{" (Set (Var "B")) where B "is" ($#m1_subset_1 :::"Subset":::) "of" "T" : (Bool (Set ($#k3_decomp_1 :::"alphaInt"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k1_decomp_1 :::"sInt"::: ) (Set (Var "B")))) "}" ; func :::"D(alpha,ps)"::: "T" -> ($#m1_subset_1 :::"Subset-Family":::) "of" "T" equals :: DECOMP_1:def 22 "{" (Set (Var "B")) where B "is" ($#m1_subset_1 :::"Subset":::) "of" "T" : (Bool (Set ($#k3_decomp_1 :::"alphaInt"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k4_decomp_1 :::"psInt"::: ) (Set (Var "B")))) "}" ; func :::"D(p,sp)"::: "T" -> ($#m1_subset_1 :::"Subset-Family":::) "of" "T" equals :: DECOMP_1:def 23 "{" (Set (Var "B")) where B "is" ($#m1_subset_1 :::"Subset":::) "of" "T" : (Bool (Set ($#k2_decomp_1 :::"pInt"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k5_decomp_1 :::"spInt"::: ) (Set (Var "B")))) "}" ; func :::"D(p,ps)"::: "T" -> ($#m1_subset_1 :::"Subset-Family":::) "of" "T" equals :: DECOMP_1:def 24 "{" (Set (Var "B")) where B "is" ($#m1_subset_1 :::"Subset":::) "of" "T" : (Bool (Set ($#k2_decomp_1 :::"pInt"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k4_decomp_1 :::"psInt"::: ) (Set (Var "B")))) "}" ; func :::"D(sp,ps)"::: "T" -> ($#m1_subset_1 :::"Subset-Family":::) "of" "T" equals :: DECOMP_1:def 25 "{" (Set (Var "B")) where B "is" ($#m1_subset_1 :::"Subset":::) "of" "T" : (Bool (Set ($#k5_decomp_1 :::"spInt"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k4_decomp_1 :::"psInt"::: ) (Set (Var "B")))) "}" ; end; :: deftheorem defines :::"^alpha"::: DECOMP_1:def 11 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set (Set (Var "T")) ($#k6_decomp_1 :::"^alpha"::: ) ) ($#r1_hidden :::"="::: ) "{" (Set (Var "B")) where B "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) : (Bool (Set (Var "B")) "is" ($#m1_decomp_1 :::"alpha-set"::: ) "of" (Set (Var "T"))) "}" )); :: deftheorem defines :::"SO"::: DECOMP_1:def 12 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set ($#k7_decomp_1 :::"SO"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "B")) where B "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) : (Bool (Set (Var "B")) "is" ($#v1_decomp_1 :::"semi-open"::: ) ) "}" )); :: deftheorem defines :::"PO"::: DECOMP_1:def 13 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set ($#k8_decomp_1 :::"PO"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "B")) where B "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) : (Bool (Set (Var "B")) "is" ($#v2_decomp_1 :::"pre-open"::: ) ) "}" )); :: deftheorem defines :::"SPO"::: DECOMP_1:def 14 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set ($#k9_decomp_1 :::"SPO"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "B")) where B "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) : (Bool (Set (Var "B")) "is" ($#v4_decomp_1 :::"semi-pre-open"::: ) ) "}" )); :: deftheorem defines :::"PSO"::: DECOMP_1:def 15 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set ($#k10_decomp_1 :::"PSO"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "B")) where B "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) : (Bool (Set (Var "B")) "is" ($#v3_decomp_1 :::"pre-semi-open"::: ) ) "}" )); :: deftheorem defines :::"D(c,alpha)"::: DECOMP_1:def 16 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set ($#k11_decomp_1 :::"D(c,alpha)"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "B")) where B "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) : (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k3_decomp_1 :::"alphaInt"::: ) (Set (Var "B")))) "}" )); :: deftheorem defines :::"D(c,p)"::: DECOMP_1:def 17 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set ($#k12_decomp_1 :::"D(c,p)"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "B")) where B "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) : (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k2_decomp_1 :::"pInt"::: ) (Set (Var "B")))) "}" )); :: deftheorem defines :::"D(c,s)"::: DECOMP_1:def 18 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set ($#k13_decomp_1 :::"D(c,s)"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "B")) where B "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) : (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k1_decomp_1 :::"sInt"::: ) (Set (Var "B")))) "}" )); :: deftheorem defines :::"D(c,ps)"::: DECOMP_1:def 19 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set ($#k14_decomp_1 :::"D(c,ps)"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "B")) where B "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) : (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k4_decomp_1 :::"psInt"::: ) (Set (Var "B")))) "}" )); :: deftheorem defines :::"D(alpha,p)"::: DECOMP_1:def 20 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set ($#k15_decomp_1 :::"D(alpha,p)"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "B")) where B "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) : (Bool (Set ($#k3_decomp_1 :::"alphaInt"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k2_decomp_1 :::"pInt"::: ) (Set (Var "B")))) "}" )); :: deftheorem defines :::"D(alpha,s)"::: DECOMP_1:def 21 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set ($#k16_decomp_1 :::"D(alpha,s)"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "B")) where B "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) : (Bool (Set ($#k3_decomp_1 :::"alphaInt"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k1_decomp_1 :::"sInt"::: ) (Set (Var "B")))) "}" )); :: deftheorem defines :::"D(alpha,ps)"::: DECOMP_1:def 22 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set ($#k17_decomp_1 :::"D(alpha,ps)"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "B")) where B "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) : (Bool (Set ($#k3_decomp_1 :::"alphaInt"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k4_decomp_1 :::"psInt"::: ) (Set (Var "B")))) "}" )); :: deftheorem defines :::"D(p,sp)"::: DECOMP_1:def 23 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set ($#k18_decomp_1 :::"D(p,sp)"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "B")) where B "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) : (Bool (Set ($#k2_decomp_1 :::"pInt"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k5_decomp_1 :::"spInt"::: ) (Set (Var "B")))) "}" )); :: deftheorem defines :::"D(p,ps)"::: DECOMP_1:def 24 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set ($#k19_decomp_1 :::"D(p,ps)"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "B")) where B "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) : (Bool (Set ($#k2_decomp_1 :::"pInt"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k4_decomp_1 :::"psInt"::: ) (Set (Var "B")))) "}" )); :: deftheorem defines :::"D(sp,ps)"::: DECOMP_1:def 25 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set ($#k20_decomp_1 :::"D(sp,ps)"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "B")) where B "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) : (Bool (Set ($#k5_decomp_1 :::"spInt"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k4_decomp_1 :::"psInt"::: ) (Set (Var "B")))) "}" )); theorem :: DECOMP_1:1 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set ($#k3_decomp_1 :::"alphaInt"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k2_decomp_1 :::"pInt"::: ) (Set (Var "B")))) "iff" (Bool (Set ($#k1_decomp_1 :::"sInt"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k4_decomp_1 :::"psInt"::: ) (Set (Var "B")))) ")" ))) ; theorem :: DECOMP_1:2 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "B")) "is" ($#m1_decomp_1 :::"alpha-set"::: ) "of" (Set (Var "T"))) "iff" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k3_decomp_1 :::"alphaInt"::: ) (Set (Var "B")))) ")" ))) ; theorem :: DECOMP_1:3 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "B")) "is" ($#v1_decomp_1 :::"semi-open"::: ) ) "iff" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k1_decomp_1 :::"sInt"::: ) (Set (Var "B")))) ")" ))) ; theorem :: DECOMP_1:4 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "B")) "is" ($#v2_decomp_1 :::"pre-open"::: ) ) "iff" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k2_decomp_1 :::"pInt"::: ) (Set (Var "B")))) ")" ))) ; theorem :: DECOMP_1:5 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "B")) "is" ($#v3_decomp_1 :::"pre-semi-open"::: ) ) "iff" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k4_decomp_1 :::"psInt"::: ) (Set (Var "B")))) ")" ))) ; theorem :: DECOMP_1:6 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "B")) "is" ($#v4_decomp_1 :::"semi-pre-open"::: ) ) "iff" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k5_decomp_1 :::"spInt"::: ) (Set (Var "B")))) ")" ))) ; theorem :: DECOMP_1:7 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set (Set "(" (Set (Var "T")) ($#k6_decomp_1 :::"^alpha"::: ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k11_decomp_1 :::"D(c,alpha)"::: ) (Set (Var "T")) ")" )) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T"))))) ; theorem :: DECOMP_1:8 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set (Set "(" ($#k7_decomp_1 :::"SO"::: ) (Set (Var "T")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k13_decomp_1 :::"D(c,s)"::: ) (Set (Var "T")) ")" )) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T"))))) ; theorem :: DECOMP_1:9 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set (Set "(" ($#k8_decomp_1 :::"PO"::: ) (Set (Var "T")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k12_decomp_1 :::"D(c,p)"::: ) (Set (Var "T")) ")" )) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T"))))) ; theorem :: DECOMP_1:10 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set (Set "(" ($#k10_decomp_1 :::"PSO"::: ) (Set (Var "T")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k14_decomp_1 :::"D(c,ps)"::: ) (Set (Var "T")) ")" )) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T"))))) ; theorem :: DECOMP_1:11 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set (Set "(" ($#k8_decomp_1 :::"PO"::: ) (Set (Var "T")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k15_decomp_1 :::"D(alpha,p)"::: ) (Set (Var "T")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "T")) ($#k6_decomp_1 :::"^alpha"::: ) ))) ; theorem :: DECOMP_1:12 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set (Set "(" ($#k7_decomp_1 :::"SO"::: ) (Set (Var "T")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k16_decomp_1 :::"D(alpha,s)"::: ) (Set (Var "T")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "T")) ($#k6_decomp_1 :::"^alpha"::: ) ))) ; theorem :: DECOMP_1:13 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set (Set "(" ($#k10_decomp_1 :::"PSO"::: ) (Set (Var "T")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k17_decomp_1 :::"D(alpha,ps)"::: ) (Set (Var "T")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "T")) ($#k6_decomp_1 :::"^alpha"::: ) ))) ; theorem :: DECOMP_1:14 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set (Set "(" ($#k9_decomp_1 :::"SPO"::: ) (Set (Var "T")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k18_decomp_1 :::"D(p,sp)"::: ) (Set (Var "T")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k8_decomp_1 :::"PO"::: ) (Set (Var "T"))))) ; theorem :: DECOMP_1:15 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set (Set "(" ($#k10_decomp_1 :::"PSO"::: ) (Set (Var "T")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k19_decomp_1 :::"D(p,ps)"::: ) (Set (Var "T")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k8_decomp_1 :::"PO"::: ) (Set (Var "T"))))) ; theorem :: DECOMP_1:16 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set (Set "(" ($#k10_decomp_1 :::"PSO"::: ) (Set (Var "T")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k15_decomp_1 :::"D(alpha,p)"::: ) (Set (Var "T")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_decomp_1 :::"SO"::: ) (Set (Var "T"))))) ; theorem :: DECOMP_1:17 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set (Set "(" ($#k10_decomp_1 :::"PSO"::: ) (Set (Var "T")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k20_decomp_1 :::"D(sp,ps)"::: ) (Set (Var "T")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_decomp_1 :::"SPO"::: ) (Set (Var "T"))))) ; definitionlet "X", "Y" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set (Const "Y")); attr "f" is :::"s-continuous"::: means :: DECOMP_1:def 26 (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" "Y" "st" (Bool (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set "f" ($#k8_relset_1 :::"""::: ) (Set (Var "G"))) ($#r2_hidden :::"in"::: ) (Set ($#k7_decomp_1 :::"SO"::: ) "X"))); attr "f" is :::"p-continuous"::: means :: DECOMP_1:def 27 (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" "Y" "st" (Bool (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set "f" ($#k8_relset_1 :::"""::: ) (Set (Var "G"))) ($#r2_hidden :::"in"::: ) (Set ($#k8_decomp_1 :::"PO"::: ) "X"))); attr "f" is :::"alpha-continuous"::: means :: DECOMP_1:def 28 (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" "Y" "st" (Bool (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set "f" ($#k8_relset_1 :::"""::: ) (Set (Var "G"))) ($#r2_hidden :::"in"::: ) (Set "X" ($#k6_decomp_1 :::"^alpha"::: ) ))); attr "f" is :::"ps-continuous"::: means :: DECOMP_1:def 29 (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" "Y" "st" (Bool (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set "f" ($#k8_relset_1 :::"""::: ) (Set (Var "G"))) ($#r2_hidden :::"in"::: ) (Set ($#k10_decomp_1 :::"PSO"::: ) "X"))); attr "f" is :::"sp-continuous"::: means :: DECOMP_1:def 30 (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" "Y" "st" (Bool (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set "f" ($#k8_relset_1 :::"""::: ) (Set (Var "G"))) ($#r2_hidden :::"in"::: ) (Set ($#k9_decomp_1 :::"SPO"::: ) "X"))); attr "f" is :::"(c,alpha)-continuous"::: means :: DECOMP_1:def 31 (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" "Y" "st" (Bool (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set "f" ($#k8_relset_1 :::"""::: ) (Set (Var "G"))) ($#r2_hidden :::"in"::: ) (Set ($#k11_decomp_1 :::"D(c,alpha)"::: ) "X"))); attr "f" is :::"(c,s)-continuous"::: means :: DECOMP_1:def 32 (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" "Y" "st" (Bool (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set "f" ($#k8_relset_1 :::"""::: ) (Set (Var "G"))) ($#r2_hidden :::"in"::: ) (Set ($#k13_decomp_1 :::"D(c,s)"::: ) "X"))); attr "f" is :::"(c,p)-continuous"::: means :: DECOMP_1:def 33 (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" "Y" "st" (Bool (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set "f" ($#k8_relset_1 :::"""::: ) (Set (Var "G"))) ($#r2_hidden :::"in"::: ) (Set ($#k12_decomp_1 :::"D(c,p)"::: ) "X"))); attr "f" is :::"(c,ps)-continuous"::: means :: DECOMP_1:def 34 (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" "Y" "st" (Bool (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set "f" ($#k8_relset_1 :::"""::: ) (Set (Var "G"))) ($#r2_hidden :::"in"::: ) (Set ($#k14_decomp_1 :::"D(c,ps)"::: ) "X"))); attr "f" is :::"(alpha,p)-continuous"::: means :: DECOMP_1:def 35 (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" "Y" "st" (Bool (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set "f" ($#k8_relset_1 :::"""::: ) (Set (Var "G"))) ($#r2_hidden :::"in"::: ) (Set ($#k15_decomp_1 :::"D(alpha,p)"::: ) "X"))); attr "f" is :::"(alpha,s)-continuous"::: means :: DECOMP_1:def 36 (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" "Y" "st" (Bool (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set "f" ($#k8_relset_1 :::"""::: ) (Set (Var "G"))) ($#r2_hidden :::"in"::: ) (Set ($#k16_decomp_1 :::"D(alpha,s)"::: ) "X"))); attr "f" is :::"(alpha,ps)-continuous"::: means :: DECOMP_1:def 37 (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" "Y" "st" (Bool (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set "f" ($#k8_relset_1 :::"""::: ) (Set (Var "G"))) ($#r2_hidden :::"in"::: ) (Set ($#k17_decomp_1 :::"D(alpha,ps)"::: ) "X"))); attr "f" is :::"(p,ps)-continuous"::: means :: DECOMP_1:def 38 (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" "Y" "st" (Bool (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set "f" ($#k8_relset_1 :::"""::: ) (Set (Var "G"))) ($#r2_hidden :::"in"::: ) (Set ($#k19_decomp_1 :::"D(p,ps)"::: ) "X"))); attr "f" is :::"(p,sp)-continuous"::: means :: DECOMP_1:def 39 (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" "Y" "st" (Bool (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set "f" ($#k8_relset_1 :::"""::: ) (Set (Var "G"))) ($#r2_hidden :::"in"::: ) (Set ($#k18_decomp_1 :::"D(p,sp)"::: ) "X"))); attr "f" is :::"(sp,ps)-continuous"::: means :: DECOMP_1:def 40 (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" "Y" "st" (Bool (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set "f" ($#k8_relset_1 :::"""::: ) (Set (Var "G"))) ($#r2_hidden :::"in"::: ) (Set ($#k20_decomp_1 :::"D(sp,ps)"::: ) "X"))); end; :: deftheorem defines :::"s-continuous"::: DECOMP_1:def 26 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v5_decomp_1 :::"s-continuous"::: ) ) "iff" (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set (Var "G"))) ($#r2_hidden :::"in"::: ) (Set ($#k7_decomp_1 :::"SO"::: ) (Set (Var "X"))))) ")" ))); :: deftheorem defines :::"p-continuous"::: DECOMP_1:def 27 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v6_decomp_1 :::"p-continuous"::: ) ) "iff" (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set (Var "G"))) ($#r2_hidden :::"in"::: ) (Set ($#k8_decomp_1 :::"PO"::: ) (Set (Var "X"))))) ")" ))); :: deftheorem defines :::"alpha-continuous"::: DECOMP_1:def 28 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v7_decomp_1 :::"alpha-continuous"::: ) ) "iff" (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set (Var "G"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "X")) ($#k6_decomp_1 :::"^alpha"::: ) ))) ")" ))); :: deftheorem defines :::"ps-continuous"::: DECOMP_1:def 29 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v8_decomp_1 :::"ps-continuous"::: ) ) "iff" (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set (Var "G"))) ($#r2_hidden :::"in"::: ) (Set ($#k10_decomp_1 :::"PSO"::: ) (Set (Var "X"))))) ")" ))); :: deftheorem defines :::"sp-continuous"::: DECOMP_1:def 30 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v9_decomp_1 :::"sp-continuous"::: ) ) "iff" (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set (Var "G"))) ($#r2_hidden :::"in"::: ) (Set ($#k9_decomp_1 :::"SPO"::: ) (Set (Var "X"))))) ")" ))); :: deftheorem defines :::"(c,alpha)-continuous"::: DECOMP_1:def 31 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v10_decomp_1 :::"(c,alpha)-continuous"::: ) ) "iff" (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set (Var "G"))) ($#r2_hidden :::"in"::: ) (Set ($#k11_decomp_1 :::"D(c,alpha)"::: ) (Set (Var "X"))))) ")" ))); :: deftheorem defines :::"(c,s)-continuous"::: DECOMP_1:def 32 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v11_decomp_1 :::"(c,s)-continuous"::: ) ) "iff" (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set (Var "G"))) ($#r2_hidden :::"in"::: ) (Set ($#k13_decomp_1 :::"D(c,s)"::: ) (Set (Var "X"))))) ")" ))); :: deftheorem defines :::"(c,p)-continuous"::: DECOMP_1:def 33 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v12_decomp_1 :::"(c,p)-continuous"::: ) ) "iff" (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set (Var "G"))) ($#r2_hidden :::"in"::: ) (Set ($#k12_decomp_1 :::"D(c,p)"::: ) (Set (Var "X"))))) ")" ))); :: deftheorem defines :::"(c,ps)-continuous"::: DECOMP_1:def 34 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v13_decomp_1 :::"(c,ps)-continuous"::: ) ) "iff" (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set (Var "G"))) ($#r2_hidden :::"in"::: ) (Set ($#k14_decomp_1 :::"D(c,ps)"::: ) (Set (Var "X"))))) ")" ))); :: deftheorem defines :::"(alpha,p)-continuous"::: DECOMP_1:def 35 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v14_decomp_1 :::"(alpha,p)-continuous"::: ) ) "iff" (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set (Var "G"))) ($#r2_hidden :::"in"::: ) (Set ($#k15_decomp_1 :::"D(alpha,p)"::: ) (Set (Var "X"))))) ")" ))); :: deftheorem defines :::"(alpha,s)-continuous"::: DECOMP_1:def 36 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v15_decomp_1 :::"(alpha,s)-continuous"::: ) ) "iff" (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set (Var "G"))) ($#r2_hidden :::"in"::: ) (Set ($#k16_decomp_1 :::"D(alpha,s)"::: ) (Set (Var "X"))))) ")" ))); :: deftheorem defines :::"(alpha,ps)-continuous"::: DECOMP_1:def 37 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v16_decomp_1 :::"(alpha,ps)-continuous"::: ) ) "iff" (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set (Var "G"))) ($#r2_hidden :::"in"::: ) (Set ($#k17_decomp_1 :::"D(alpha,ps)"::: ) (Set (Var "X"))))) ")" ))); :: deftheorem defines :::"(p,ps)-continuous"::: DECOMP_1:def 38 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v17_decomp_1 :::"(p,ps)-continuous"::: ) ) "iff" (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set (Var "G"))) ($#r2_hidden :::"in"::: ) (Set ($#k19_decomp_1 :::"D(p,ps)"::: ) (Set (Var "X"))))) ")" ))); :: deftheorem defines :::"(p,sp)-continuous"::: DECOMP_1:def 39 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v18_decomp_1 :::"(p,sp)-continuous"::: ) ) "iff" (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set (Var "G"))) ($#r2_hidden :::"in"::: ) (Set ($#k18_decomp_1 :::"D(p,sp)"::: ) (Set (Var "X"))))) ")" ))); :: deftheorem defines :::"(sp,ps)-continuous"::: DECOMP_1:def 40 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v19_decomp_1 :::"(sp,ps)-continuous"::: ) ) "iff" (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set (Var "G"))) ($#r2_hidden :::"in"::: ) (Set ($#k20_decomp_1 :::"D(sp,ps)"::: ) (Set (Var "X"))))) ")" ))); theorem :: DECOMP_1:18 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v7_decomp_1 :::"alpha-continuous"::: ) ) "iff" (Bool "(" (Bool (Set (Var "f")) "is" ($#v6_decomp_1 :::"p-continuous"::: ) ) & (Bool (Set (Var "f")) "is" ($#v14_decomp_1 :::"(alpha,p)-continuous"::: ) ) ")" ) ")" ))) ; theorem :: DECOMP_1:19 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v7_decomp_1 :::"alpha-continuous"::: ) ) "iff" (Bool "(" (Bool (Set (Var "f")) "is" ($#v5_decomp_1 :::"s-continuous"::: ) ) & (Bool (Set (Var "f")) "is" ($#v15_decomp_1 :::"(alpha,s)-continuous"::: ) ) ")" ) ")" ))) ; theorem :: DECOMP_1:20 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v7_decomp_1 :::"alpha-continuous"::: ) ) "iff" (Bool "(" (Bool (Set (Var "f")) "is" ($#v8_decomp_1 :::"ps-continuous"::: ) ) & (Bool (Set (Var "f")) "is" ($#v16_decomp_1 :::"(alpha,ps)-continuous"::: ) ) ")" ) ")" ))) ; theorem :: DECOMP_1:21 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v6_decomp_1 :::"p-continuous"::: ) ) "iff" (Bool "(" (Bool (Set (Var "f")) "is" ($#v9_decomp_1 :::"sp-continuous"::: ) ) & (Bool (Set (Var "f")) "is" ($#v18_decomp_1 :::"(p,sp)-continuous"::: ) ) ")" ) ")" ))) ; theorem :: DECOMP_1:22 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v6_decomp_1 :::"p-continuous"::: ) ) "iff" (Bool "(" (Bool (Set (Var "f")) "is" ($#v8_decomp_1 :::"ps-continuous"::: ) ) & (Bool (Set (Var "f")) "is" ($#v17_decomp_1 :::"(p,ps)-continuous"::: ) ) ")" ) ")" ))) ; theorem :: DECOMP_1:23 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v5_decomp_1 :::"s-continuous"::: ) ) "iff" (Bool "(" (Bool (Set (Var "f")) "is" ($#v8_decomp_1 :::"ps-continuous"::: ) ) & (Bool (Set (Var "f")) "is" ($#v14_decomp_1 :::"(alpha,p)-continuous"::: ) ) ")" ) ")" ))) ; theorem :: DECOMP_1:24 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v9_decomp_1 :::"sp-continuous"::: ) ) "iff" (Bool "(" (Bool (Set (Var "f")) "is" ($#v8_decomp_1 :::"ps-continuous"::: ) ) & (Bool (Set (Var "f")) "is" ($#v19_decomp_1 :::"(sp,ps)-continuous"::: ) ) ")" ) ")" ))) ; theorem :: DECOMP_1:25 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ) "iff" (Bool "(" (Bool (Set (Var "f")) "is" ($#v7_decomp_1 :::"alpha-continuous"::: ) ) & (Bool (Set (Var "f")) "is" ($#v10_decomp_1 :::"(c,alpha)-continuous"::: ) ) ")" ) ")" ))) ; theorem :: DECOMP_1:26 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ) "iff" (Bool "(" (Bool (Set (Var "f")) "is" ($#v5_decomp_1 :::"s-continuous"::: ) ) & (Bool (Set (Var "f")) "is" ($#v11_decomp_1 :::"(c,s)-continuous"::: ) ) ")" ) ")" ))) ; theorem :: DECOMP_1:27 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ) "iff" (Bool "(" (Bool (Set (Var "f")) "is" ($#v6_decomp_1 :::"p-continuous"::: ) ) & (Bool (Set (Var "f")) "is" ($#v12_decomp_1 :::"(c,p)-continuous"::: ) ) ")" ) ")" ))) ; theorem :: DECOMP_1:28 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ) "iff" (Bool "(" (Bool (Set (Var "f")) "is" ($#v8_decomp_1 :::"ps-continuous"::: ) ) & (Bool (Set (Var "f")) "is" ($#v13_decomp_1 :::"(c,ps)-continuous"::: ) ) ")" ) ")" ))) ;