% lem1: if xb is a basis for x, then the topology generated by xb forms % a topological space with x set(binary_res). assign(max_seconds,3600). set(unit_deletion). set(factor). list(axioms). % top_space definition: top_space(x,xt) | -el_s(0,xt) | -el_s(x,xt) | el_s(f1(x,xt),xt) | subset_c(f3(x,xt),xt). top_space(x,xt) | -el_s(0,xt) | -el_s(x,xt) | el_s(f1(x,xt),xt) | -el_s(sigma(f3(x,xt)),xt). top_space(x,xt) | -el_s(0,xt) | -el_s(x,xt) | el_s(f2(x,xt),xt) | subset_c(f3(x,xt),xt). top_space(x,xt) | -el_s(0,xt) | -el_s(x,xt) | el_s(f2(x,xt),xt) | -el_s(sigma(f3(x,xt)),xt). top_space(x,xt) | -el_s(0,xt) | -el_s(x,xt) | -el_s(inter_s(f1(x,xt),f2(x,xt)),xt) | subset_c(f3(x,xt),xt). top_space(x,xt) | -el_s(0,xt) | -el_s(x,xt) | -el_s(inter_s(f1(x,xt),f2(x,xt)),xt) | -el_s(sigma(f3(x,xt)),xt). % previous lemmas: -basis(xb,x) | el_s(0,top_of_basis(xb)). -basis(xb,x) | el_s(x,top_of_basis(xb)). -basis(xb,x) | -el_s(u,top_of_basis(xb)) | -el_s(v,top_of_basis(xb)) | el_s(inter_s(u,v),top_of_basis(xb)). -basis(xb,x) | -subset_c(xs,top_of_basis(xb)) | el_s(sigma(xs),top_of_basis(xb)). end_of_list. list(sos). % lemma: given a basis, the topology generated and the space form a % topological space. % denial: exists a space, a basis, & the topology gen. that basis, % such that the space and the topology aren't a topological space basis(B,X). -top_space(X,top_of_basis(B)). end_of_list. list(demodulators). eq_s(inter_s(inter_s(x,y),z), inter_s(x,inter_s(y,z))). eq_s(inter_s(x,x),x). eq_s(inter_s(x,0),0). eq_s(inter_s(0,x),0). eq_s(inter_s(x,inter_s(x,y)),inter_s(x,y)). eq_s(inter_s(x,inter_s(y,x)),inter_s(x,y)). end_of_list. weight_list(pick_given). weight(f1(0,0), 1). weight(f2(0,0), 1). weight(f3(0,0), 1). end_of_list.