----- Otter 3.0.4, August 1995 ----- The job was started by ??? on ???, Sun Aug 18 08:32:27 2002 The command was "otter304b". set(ur_res). set(factor). set(unit_deletion). set(para_from). set(para_into). set(dynamic_demod_all). dependent: set(dynamic_demod). dependent: set(order_eq). set(back_demod). set(sos_queue). set(lex_order_vars). set(lrpo). lex([0,id(x),Id,V,omega,OMEGA,FULL,FINITE,DEDEKIND,REGULAR,RUSSELL,UNOPS,Q,BIJ,FUNS,pair(x,x),$c1,$c2,swap(x),first(x),second(x),transposition(x,x),singleton(x),DESCENDING,pairset(x,x),succ(x),union(x,x),cart(x,x),Di,U(x),tc(x),P(x),BIGCUP,POWER,SINGLETON,SUCC,PAIRSET,RANK,CARD,VERTSECT(x),HC,TC,CROSS,IMAGE(x),RC(x),UCLOSURE,ACLOSURE,CUP,CART,CAP,SYMDIF,ZN,cross(x,x),PSM(x),funpart(x),H(x),map(x,x),intersection(x,x),cantor(x),compreln(x),complement(x),fix(x),D(x),R(x),rank(x),card(x),apply(x,x),Uclosure(x),Aclosure(x),image(x,x),IMG,RIGHT(x),LEFT(x),ADJOIN(x),A(x),invar(x),subvar(x),composite(x,x),restrict(x,x,x),LEAST(x),GREATEST(x),GLB(x),LUB(x),LB(x),UPPERBOUND,K,PS,S,UB(x),DISJOINT,subcommutant(x),inverse(x),RIF,COMPOSE,BIGCAP,FIX,IDP,SUPERPOWER,ES,LOWERBOUND,E,ROT,DUP,TWIST,FIRST,ASSOC,SECOND,REVERSE,SWAP,flip(x),rotate(x),sv3(x),sv1(x),sv2(x),bij(x,x),com(x,x,x,x),ind(x),dom(x,x,x),ran(x,x,x),notsub(x,x),ONEONE(x),UNOP(x),FUNCTION(x),thin(x),WELLORDER(x),TOTALORDER(x),PARTIALORDER(x),REFLEXIVE(x),SYMMETRIC(x),TRANSITIVE(x),EQUIVALENCE(x),PARTITION(x),INDUCTIVE(x),Uclosed(x),Aclosed(x),full(x),subcommute(x,x),equal(x,x),member(x,x),subclass(x,x),disjoint(x,x)]). assign(stats_level,1). assign(max_seconds,20). assign(max_weight,20). assign(max_distinct_vars,0). include("U:\AX-A\AX-A-8.USE"). ------- start included file U:\AX-A\AX-A-8.USE------- list(usable). 1 [] -member(x,y)| -subclass(y,z)|member(x,z). 2 [] member(notsub(x,y),x)|subclass(x,y). 3 [] -member(notsub(x,y),y)|subclass(x,y). 4 [] subclass(x,V). 5 [] -subclass(x,y)| -subclass(y,x)|equal(x,y). 6 [] -member(x,pairset(y,z))|equal(x,y)|equal(x,z). 7 [] -member(x,V)|member(x,pairset(x,y)). 8 [] -member(x,V)|member(x,pairset(y,x)). 9 [] member(pairset(x,y),V). 10 [] equal(pairset(x,x),singleton(x)). end_of_list. ------- end included file U:\AX-A\AX-A-8.USE------- include("U:\AX-B\AX-B-16.USE"). ------- start included file U:\AX-B\AX-B-16.USE------- list(usable). 11 [] equal(pairset(singleton(x),pairset(x,singleton(y))),pair(x,y)). 12 [] -member(pair(u,v),cart(x,y))|member(u,x). 13 [] -member(pair(u,v),cart(x,y))|member(v,y). 14 [] member(pair(u,v),cart(x,y))| -member(u,x)| -member(v,y). 15 [] -member(x,cart(y,z))|equal(pair(first(x),second(x)),x). 16 [] subclass(E,cart(V,V)). 17 [] -member(pair(x,y),E)|member(x,y). 18 [] -member(pair(x,y),cart(V,V))| -member(x,y)|member(pair(x,y),E). 19 [] -member(x,intersection(y,z))|member(x,y). 20 [] -member(x,intersection(y,z))|member(x,z). 21 [] -member(x,y)| -member(x,z)|member(x,intersection(y,z)). 22 [] -member(x,complement(y))| -member(x,y). 23 [] -member(x,V)|member(x,y)|member(x,complement(y)). 24 [] equal(complement(intersection(complement(x),complement(y))),union(x,y)). 25 [] equal(symmetricdifference(x,y),intersection(union(x,y),complement(intersection(x,y)))). 26 [] equal(intersection(x,cart(y,z)),restrict(x,y,z)). 27 [] -member(x,D(z))| -equal(restrict(z,singleton(x),V),0). 28 [] member(x,D(z))|equal(restrict(z,singleton(x),V),0). 29 [] subclass(rotate(x),cart(cart(V,V),V)). 30 [] -member(pair(pair(u,v),w),rotate(x))|member(pair(pair(v,w),u),x). 31 [] -member(pair(pair(u,v),w),cart(cart(V,V),V))| -member(pair(pair(v,w),u),x)|member(pair(pair(u,v),w),rotate(x)). 32 [] subclass(flip(x),cart(cart(V,V),V)). 33 [] -member(pair(pair(u,v),w),flip(x))|member(pair(pair(v,u),w),x). 34 [] -member(pair(pair(u,v),w),cart(cart(V,V),V))| -member(pair(pair(v,u),w),x)|member(pair(pair(u,v),w),flip(x)). 35 [] equal(D(flip(cart(x,V))),inverse(x)). 36 [] equal(D(inverse(x)),R(x)). 37 [] equal(first(notsub(restrict(x,y,singleton(z)),0)),dom(x,y,z)). 38 [] equal(second(notsub(restrict(x,singleton(y),z),0)),ran(x,y,z)). 39 [] equal(R(restrict(x,y,V)),image(x,y)). end_of_list. ------- end included file U:\AX-B\AX-B-16.USE------- include("U:\AX-C\AXC.USE"). ------- start included file U:\AX-C\AXC.USE------- list(usable). 40 [] equal(D(intersection(rotate(flip(cart(x,V))),flip(rotate(cart(y,V))))),composite(x,y)). 41 [] equal(intersection(complement(composite(complement(E),inverse(E))),cart(V,V)),S). 42 [] equal(intersection(S,inverse(S)),Id). 43 [] equal(restrict(complement(Id),V,V),Di). 44 [] equal(intersection(E,complement(composite(E,complement(Id)))),SINGLETON). 45 [] equal(union(x,singleton(x)),succ(x)). 46 [] equal(intersection(E,S),ES). 47 [] equal(intersection(complement(Id),S),PS). 48 [] equal(intersection(ES,complement(composite(PS,ES))),SUCC). 49 [] -INDUCTIVE(x)|member(0,x). 50 [] -INDUCTIVE(x)|subclass(image(SUCC,x),x). 51 [] -member(0,x)| -subclass(image(SUCC,x),x)|INDUCTIVE(x). 52 [] member(omega,V). 53 [] INDUCTIVE(omega). 54 [] -INDUCTIVE(x)|subclass(omega,x). 55 [] equal(D(restrict(E,V,x)),U(x)). 56 [] -member(x,V)|member(U(x),V). 57 [] equal(complement(image(E,complement(x))),P(x)). 58 [] -member(x,V)|member(P(x),V). 59 [] -FUNCTION(x)|subclass(x,cart(V,V)). 60 [] -FUNCTION(x)|subclass(composite(x,inverse(x)),Id). 61 [] -subclass(composite(x,inverse(x)),Id)| -subclass(x,cart(V,V))|FUNCTION(x). 62 [] -FUNCTION(x)| -member(y,V)|member(image(x,y),V). end_of_list. ------- end included file U:\AX-C\AXC.USE------- include("U:\AX-DE\AX-REG.USE"). ------- start included file U:\AX-DE\AX-REG.USE------- list(usable). 63 [] -AxReg|equal(x,0)|member(regular(x),x). 64 [] -AxReg|equal(x,0)|equal(intersection(regular(x),x),0). 65 [] AxReg| -equal(IRREG,0). 66 [] AxReg| -member(x,IRREG)| -equal(intersection(IRREG,x),0). end_of_list. ------- end included file U:\AX-DE\AX-REG.USE------- include("U:\AX-DE\AX-CH-JB.USE"). ------- start included file U:\AX-DE\AX-CH-JB.USE------- list(usable). 67 [] -AxCh|FUNCTION(CHOICE). 68 [] -AxCh|subclass(CHOICE,inverse(E)). 69 [] -AxCh|equal(D(CHOICE),complement(singleton(0))). 70 [] -FUNCTION(z)| -subclass(z,inverse(E))| -equal(D(z),complement(singleton(0)))|AxCh. end_of_list. ------- end included file U:\AX-DE\AX-CH-JB.USE------- include("U:\DF-ID\DF-OO-1.USE"). ------- start included file U:\DF-ID\DF-OO-1.USE------- list(usable). 71 [] -ONEONE(x)|FUNCTION(x). 72 [] -ONEONE(x)|FUNCTION(inverse(x)). 73 [] -FUNCTION(x)| -FUNCTION(inverse(x))|ONEONE(x). end_of_list. ------- end included file U:\DF-ID\DF-OO-1.USE------- include("U:\PO\PO-1.USE"). ------- start included file U:\PO\PO-1.USE------- list(usable). 74 [] subclass(x,x). 75 [] -subclass(x,y)| -subclass(y,z)|subclass(x,z). end_of_list. ------- end included file U:\PO\PO-1.USE------- include("U:\EQ\EQ-2.USE"). ------- start included file U:\EQ\EQ-2.USE------- list(usable). 76 [] equal(x,x). 77 [] equal(x,y)|member(notsub(x,y),x)|member(notsub(y,x),y). 78 [] -member(notsub(x,y),y)|equal(x,y)|member(notsub(y,x),y). 79 [] -member(notsub(y,x),x)|equal(x,y)|member(notsub(x,y),x). 80 [] -member(notsub(x,y),y)| -member(notsub(y,x),x)|equal(x,y). end_of_list. ------- end included file U:\EQ\EQ-2.USE------- include("U:\SP\SP1.USE"). ------- start included file U:\SP\SP1.USE------- list(usable). 81 [] -member(x,intersection(y,complement(y))). 82 [] -member(x,0). 83 [] subclass(0,x). 84 [] -subclass(x,0)|equal(x,0). 85 [] -subclass(V,x)|equal(x,V). 86 [] equal(x,0)|member(notsub(x,0),x). 87 [] equal(x,V)|member(notsub(V,x),complement(x)). 88 [] member(0,V). 89 [] -equal(V,0). 90 [] -subclass(V,0). end_of_list. ------- end included file U:\SP\SP1.USE------- include("U:\LA\LA1.USE"). ------- start included file U:\LA\LA1.USE------- list(usable). 91 [] subclass(intersection(x,y),x). 92 [] subclass(intersection(x,y),y). 93 [] -subclass(x,y)| -subclass(x,z)|subclass(x,intersection(y,z)). 94 [] -subclass(x,y)|subclass(intersection(x,z),intersection(y,z)). 95 [] -subclass(x,intersection(y,z))|subclass(x,y). 96 [] -subclass(x,intersection(y,z))|subclass(x,z). end_of_list. ------- end included file U:\LA\LA1.USE------- include("U:\I\I1.USE"). ------- start included file U:\I\I1.USE------- list(usable). 97 [] equal(intersection(intersection(x,y),z),intersection(x,intersection(y,z))). 98 [] subclass(intersection(x,y),intersection(y,x)). 99 [] equal(intersection(x,y),intersection(y,x)). 100 [] equal(intersection(x,intersection(y,z)),intersection(y,intersection(x,z))). 101 [] equal(intersection(0,x),0). 102 [] equal(intersection(x,0),0). 103 [] equal(intersection(V,x),x). 104 [] equal(intersection(x,V),x). 105 [] equal(intersection(x,x),x). 106 [] equal(intersection(x,intersection(y,x)),intersection(x,y)). 107 [] equal(intersection(x,intersection(x,y)),intersection(x,y)). end_of_list. ------- end included file U:\I\I1.USE------- include("U:\C\C1.USE"). ------- start included file U:\C\C1.USE------- list(usable). 108 [] member(notsub(x,y),complement(y))|subclass(x,y). 109 [] -member(notsub(x,y),complement(x))|subclass(x,y). 110 [] equal(complement(complement(x)),x). 111 [] -equal(complement(x),complement(y))|equal(x,y). 112 [] equal(complement(0),V). 113 [] equal(complement(V),0). 114 [] equal(intersection(x,complement(x)),0). 115 [] equal(intersection(x,intersection(complement(x),y)),0). 116 [] equal(intersection(complement(x),intersection(x,y)),0). 117 [] equal(union(x,complement(x)),V). 118 [] equal(complement(union(x,y)),intersection(complement(x),complement(y))). 119 [] equal(complement(intersection(x,y)),union(complement(x),complement(y))). 120 [] -equal(union(x,y),V)| -equal(intersection(x,y),0)|equal(x,complement(y)). 121 [] -equal(union(intersection(x,complement(y)),intersection(complement(x),y)),0)|equal(x,y). end_of_list. ------- end included file U:\C\C1.USE------- include("U:\U\U1.USE"). ------- start included file U:\U\U1.USE------- list(usable). 122 [] -member(x,union(y,z))|member(x,y)|member(x,z). 123 [] -member(x,y)|member(x,union(y,z)). 124 [] -member(x,y)|member(x,union(z,y)). 125 [] equal(union(union(x,y),z),union(x,union(y,z))). 126 [] equal(union(x,y),union(y,x)). 127 [] equal(union(x,union(y,z)),union(y,union(x,z))). 128 [] equal(union(0,x),x). 129 [] equal(union(x,0),x). 130 [] equal(union(V,x),V). 131 [] equal(union(x,V),V). 132 [] equal(union(x,x),x). 133 [] equal(union(x,union(y,x)),union(x,y)). 134 [] equal(union(x,union(x,y)),union(x,y)). 135 [] -equal(union(x,y),0)|equal(x,0). 136 [] -equal(union(x,y),0)|equal(y,0). end_of_list. ------- end included file U:\U\U1.USE------- include("U:\SU\SU1-A.USE"). ------- start included file U:\SU\SU1-A.USE------- list(usable). 137 [] -subclass(x,y)|subclass(complement(y),complement(x)). 138 [] -subclass(complement(x),complement(y))|subclass(y,x). 139 [] -subclass(x,y)|equal(intersection(x,y),x). 140 [] -equal(intersection(x,y),x)|subclass(x,y). 141 [] -subclass(x,y)|equal(intersection(x,intersection(y,z)),intersection(x,z)). 142 [] -subclass(x,y)|equal(union(x,y),y). 143 [] -equal(union(x,y),y)|subclass(x,y). end_of_list. ------- end included file U:\SU\SU1-A.USE------- include("U:\LA\LA2.USE"). ------- start included file U:\LA\LA2.USE------- list(usable). 144 [] subclass(x,union(x,y)). 145 [] subclass(x,union(y,x)). 146 [] -subclass(x,y)| -subclass(z,y)|subclass(union(x,z),y). 147 [] -subclass(x,y)|subclass(union(x,z),union(y,z)). end_of_list. ------- end included file U:\LA\LA2.USE------- include("U:\SU\SU2.USE"). ------- start included file U:\SU\SU2.USE------- list(usable). 148 [] -subclass(x,y)|equal(intersection(complement(y),x),0). 149 [] -subclass(x,complement(y))|equal(intersection(x,y),0). 150 [] -equal(intersection(complement(x),y),0)|subclass(y,x). 151 [] -equal(intersection(x,y),0)|subclass(x,complement(y)). 152 [] -subclass(x,y)|equal(union(complement(x),y),V). 153 [] -equal(union(complement(x),y),V)|subclass(x,y). 154 [] -equal(union(x,y),V)|subclass(complement(x),y). 155 [] -equal(union(x,y),V)|subclass(complement(y),x). 156 [] -subclass(x,union(y,z))|subclass(intersection(complement(y),x),z). 157 [] -subclass(x,union(complement(y),z))|subclass(intersection(x,y),z). 158 [] -subclass(intersection(complement(x),y),z)|subclass(y,union(x,z)). 159 [] -subclass(x,y)| -subclass(intersection(complement(x),z),y)|subclass(z,y). 160 [] -subclass(intersection(complement(x),y),z)|subclass(intersection(complement(z),y),x). 161 [] -subclass(intersection(x,y),z)|subclass(intersection(complement(z),y),complement(x)). 162 [] -subclass(intersection(complement(x),y),complement(z))|subclass(intersection(y,z),x). end_of_list. ------- end included file U:\SU\SU2.USE------- include("U:\D\D.USE"). ------- start included file U:\D\D.USE------- list(usable). 163 [] equal(intersection(x,union(y,z)),union(intersection(x,y),intersection(x,z))). 164 [] equal(intersection(union(x,y),z),union(intersection(x,z),intersection(y,z))). 165 [] equal(union(intersection(x,y),intersection(x,intersection(y,z))),intersection(x,y)). 166 [] equal(union(x,union(intersection(y,z),union(intersection(x,z),intersection(x,y)))),union(intersection(y,z),x)). 167 [] equal(union(x,intersection(x,y)),x). 168 [] equal(union(x,union(y,intersection(x,z))),union(x,y)). 169 [] equal(union(x,union(intersection(x,y),z)),union(x,z)). 170 [] -equal(union(intersection(x,complement(y)),intersection(y,complement(x))),0)|equal(x,y). 171 [] equal(union(x,intersection(complement(x),y)),union(x,y)). 172 [] -equal(union(intersection(x,y),intersection(complement(x),complement(y))),V)|equal(x,y). 173 [] equal(union(x,union(y,intersection(complement(x),z))),union(x,union(y,z))). 174 [] equal(union(intersection(x,y),intersection(complement(x),intersection(z,y))),union(intersection(x,y),intersection(z,y))). 175 [] equal(union(complement(x),intersection(x,y)),union(complement(x),y)). 176 [] equal(union(complement(x),union(y,intersection(x,z))),union(complement(x),union(y,z))). 177 [] equal(union(intersection(x,y),intersection(complement(x),y)),y). 178 [] subclass(union(x,intersection(y,z)),union(x,z)). 179 [] subclass(union(intersection(x,y),z),union(x,z)). 180 [] -equal(intersection(x,y),0)|equal(intersection(y,complement(x)),y). 181 [] -equal(intersection(x,y),0)| -subclass(x,union(z,y))|subclass(x,z). end_of_list. ------- end included file U:\D\D.USE------- include("U:\DJ\DJ.USE"). ------- start included file U:\DJ\DJ.USE------- list(usable). 182 [] -equal(intersection(x,y),0)|disjoint(x,y). 183 [] -disjoint(x,y)|equal(intersection(x,y),0). 184 [] -disjoint(intersection(x,y),z)|disjoint(x,intersection(y,z)). 185 [] -member(x,y)| -member(x,z)| -disjoint(y,z). 186 [] disjoint(x,0). 187 [] disjoint(0,x). 188 [] disjoint(x,complement(x)). 189 [] disjoint(complement(x),x). 190 [] -disjoint(x,x)|equal(x,0). 191 [] -equal(x,0)|disjoint(x,x). 192 [] -disjoint(x,y)|disjoint(y,x). 193 [] -subclass(x,y)|disjoint(x,complement(y)). 194 [] -disjoint(x,complement(y))|subclass(x,y). 195 [] -disjoint(x,y)|subclass(x,complement(y)). 196 [] -member(x,y)| -disjoint(singleton(x),y). 197 [] member(x,y)|disjoint(singleton(x),y). 198 [] -disjoint(x,y)| -disjoint(z,y)|disjoint(union(x,z),y). 199 [] -subclass(x,y)| -disjoint(y,z)|disjoint(x,z). 200 [] -disjoint(x,cart(y,z))|equal(restrict(x,y,z),0). 201 [] -equal(restrict(x,y,z),0)|disjoint(x,cart(y,z)). 202 [] -member(x,D(y))| -disjoint(y,cart(singleton(x),V)). 203 [] member(x,D(y))|disjoint(y,cart(singleton(x),V)). 204 [] member(notsub(x,complement(y)),x)|disjoint(x,y). 205 [] member(notsub(x,complement(y)),y)|disjoint(x,y). 206 [] -disjoint(x,y)| -subclass(complement(x),y)|equal(complement(x),y). end_of_list. ------- end included file U:\DJ\DJ.USE------- include("U:\UP\UP1.USE"). ------- start included file U:\UP\UP1.USE------- list(usable). 207 [] subclass(pairset(x,y),pairset(y,x)). 208 [] equal(pairset(x,y),pairset(y,x)). 209 [] equal(pairset(x,y),0)|member(x,V)|member(y,V). 210 [] subclass(singleton(x),pairset(x,y)). 211 [] equal(pairset(x,y),singleton(x))|member(y,V). 212 [] -equal(pairset(x,y),pairset(x,z))| -member(pair(y,z),cart(V,V))|equal(y,z). 213 [] -equal(pairset(x,y),pairset(z,y))| -member(pair(x,z),cart(V,V))|equal(x,z). 214 [] -equal(pairset(x,y),0)| -member(x,V). 215 [] -equal(pairset(x,y),0)| -member(y,V). 216 [] -member(x,y)| -member(z,y)|subclass(pairset(x,z),y). end_of_list. ------- end included file U:\UP\UP1.USE------- include("U:\UP\UP2.USE"). ------- start included file U:\UP\UP2.USE------- list(usable). 217 [] equal(union(singleton(x),singleton(y)),pairset(x,y)). 218 [] -equal(singleton(x),singleton(y))|equal(pairset(x,z),pairset(y,z)). 219 [] -equal(singleton(x),singleton(y))| -equal(singleton(z),singleton(u))|equal(pairset(x,singleton(z)),pairset(y,singleton(u))). end_of_list. ------- end included file U:\UP\UP2.USE------- include("U:\SS\SS1.USE"). ------- start included file U:\SS\SS1.USE------- list(usable). 220 [] member(singleton(x),V). 221 [] -member(x,V)|member(x,singleton(x)). 222 [] -member(x,complement(singleton(x))). 223 [] -equal(singleton(x),0)| -member(x,V). 224 [] -equal(singleton(0),0). 225 [] member(0,singleton(0)). 226 [] member(singleton(x),singleton(singleton(x))). 227 [] member(0,union(x,singleton(0))). 228 [] -member(x,singleton(y))|equal(x,y). 229 [] -equal(singleton(0),V). 230 [] equal(singleton(x),0)|member(x,V). 231 [] -subclass(x,union(y,singleton(z)))|member(z,x)|subclass(x,y). 232 [] -equal(singleton(x),singleton(y))| -member(x,V)|equal(x,y). 233 [] -equal(singleton(x),singleton(y))| -member(y,V)|equal(x,y). end_of_list. ------- end included file U:\SS\SS1.USE------- include("U:\SS\SS2.USE"). ------- start included file U:\SS\SS2.USE------- list(usable). 234 [] equal(memb(x),x)|member(memb(x),V). 235 [] equal(singleton(memb(x)),x)|equal(memb(x),x). 236 [] -member(x,V)|equal(memb(singleton(x)),x). 237 [] -member(x,V)|member(memb(x),V). 238 [] -equal(singleton(memb(x)),x)|member(x,V). 239 [] -equal(singleton(memb(x)),x)| -member(y,x)|equal(memb(x),y). end_of_list. ------- end included file U:\SS\SS2.USE------- include("U:\SS\SS3.USE"). ------- start included file U:\SS\SS3.USE------- list(usable). 240 [] -member(x,y)|subclass(singleton(x),y). 241 [] -subclass(x,singleton(y))|equal(x,0)|equal(singleton(y),x). 242 [] -member(x,y)| -subclass(y,singleton(x))|equal(singleton(x),y). 243 [] -subclass(x,singleton(y))|member(x,V). 244 [] -subclass(x,singleton(y))|equal(x,0)|member(y,x). 245 [] equal(x,0)|equal(singleton(notsub(x,0)),x)|member(notsub(x,singleton(notsub(x,0))),x). 246 [] equal(x,0)|equal(singleton(notsub(x,0)),x)|member(notsub(intersection(x,complement(singleton(notsub(x,0)))),0),x). 247 [] -equal(notsub(intersection(x,complement(singleton(notsub(x,0)))),0),notsub(x,0))|equal(x,0)|equal(singleton(notsub(x,0)),x). 248 [] equal(x,0)|equal(singleton(notsub(x,0)),x)|member(notsub(intersection(x,complement(singleton(notsub(x,0)))),0),intersection(x,complement(singleton(notsub(x,0))))). end_of_list. ------- end included file U:\SS\SS3.USE------- include("U:\SS\SS4.USE"). ------- start included file U:\SS\SS4.USE------- list(usable). 249 [] -equal(x,0)| -member(x,complement(singleton(0))). 250 [] -member(x,V)| -subclass(singleton(x),y)|member(x,y). 251 [] subclass(singleton(x),pairset(y,x)). 252 [] equal(x,y)|equal(intersection(singleton(x),singleton(y)),0). end_of_list. ------- end included file U:\SS\SS4.USE------- include("U:\OP\OP1.USE"). ------- start included file U:\OP\OP1.USE------- list(usable). 253 [] member(pair(x,y),V). 254 [] member(pair(pair(x,y),pair(z,u)),cart(V,V)). 255 [] member(singleton(x),pair(x,y)). 256 [] member(pairset(x,singleton(y)),pair(x,y)). 257 [] -equal(pair(x,y),0). 258 [] equal(pairset(singleton(x),pairset(x,0)),pair(x,y))|member(y,V). 259 [] equal(pairset(0,singleton(singleton(x))),pair(y,x))|member(y,V). 260 [] equal(pairset(0,singleton(0)),pair(x,y))|member(x,V)|member(y,V). 261 [] -equal(pair(x,y),pair(z,u))| -member(z,V)|equal(x,z). 262 [] -equal(pair(x,y),pair(z,u))| -member(y,V)| -member(u,V)|equal(y,u). 263 [] -equal(pair(x,y),pair(z,u))| -member(y,V)|equal(y,u)|member(x,V)|member(z,V). 264 [] -equal(pair(x,y),pair(z,u))| -member(x,V)| -member(u,V)|equal(y,u)|member(z,V). 265 [] -equal(pair(x,y),pair(z,u))| -member(x,V)| -member(y,V)|equal(y,u). 266 [] -member(x,V)| -member(y,pair(x,z))|member(x,y). end_of_list. ------- end included file U:\OP\OP1.USE------- include("U:\OP\OP2.USE"). ------- start included file U:\OP\OP2.USE------- list(usable). 267 [] equal(pair(first(x),second(x)),x)|equal(first(x),x). 268 [] equal(pair(first(x),second(x)),x)|equal(second(x),x). 269 [] equal(first(x),x)|member(x,cart(V,V)). 270 [] equal(second(x),x)|member(x,cart(V,V)). 271 [] equal(first(x),x)|member(pair(first(x),second(x)),cart(V,V)). 272 [] equal(second(x),x)|member(pair(first(x),second(x)),cart(V,V)). 273 [] -member(pair(x,y),cart(V,V))|equal(first(pair(x,y)),x). 274 [] -member(pair(x,y),cart(V,V))|equal(second(pair(x,y)),y). end_of_list. ------- end included file U:\OP\OP2.USE------- include("U:\OP\OP3.USE"). ------- start included file U:\OP\OP3.USE------- list(usable). 275 [] -equal(pair(first(x),second(x)),x)|member(x,V). 276 [] -equal(pair(first(x),second(x)),x)|member(x,cart(V,V)). 277 [] -equal(pair(x,y),pair(z,u))| -member(x,V)|equal(x,z). 278 [] equal(first(pair(x,y)),pair(x,y))|member(x,V). 279 [] equal(second(pair(x,y)),pair(x,y))|member(x,V). 280 [] -equal(pair(x,y),pair(z,u))| -member(y,V)|equal(y,u). 281 [] equal(first(pair(x,y)),pair(x,y))|member(y,V). 282 [] equal(second(pair(x,y)),pair(x,y))|member(y,V). 283 [] equal(first(x),x)|member(first(x),V). 284 [] equal(second(x),x)|member(second(x),V). 285 [] -member(x,V)|member(first(x),V). 286 [] -member(x,V)|member(second(x),V). 287 [] equal(first(x),x)|member(x,V). 288 [] equal(second(x),x)|member(x,V). 289 [] -member(x,cart(cart(V,V),V))|equal(pair(pair(first(first(x)),second(first(x))),second(x)),x). 290 [] -member(x,rotate(y))|member(pair(pair(second(first(x)),second(x)),first(first(x))),y). end_of_list. ------- end included file U:\OP\OP3.USE------- include("U:\OP\OP4.USE"). ------- start included file U:\OP\OP4.USE------- list(usable). 291 [] -equal(pair(x,y),pair(z,u))|equal(singleton(x),singleton(z)). 292 [] -equal(pair(x,y),pair(z,u))|equal(singleton(y),singleton(u)). 293 [] equal(pairset(singleton(x),union(singleton(x),singleton(singleton(y)))),pair(x,y)). 294 [] -equal(singleton(x),singleton(y))|equal(pair(z,x),pair(z,y)). 295 [] -equal(singleton(x),singleton(y))|equal(pair(x,z),pair(y,z)). end_of_list. ------- end included file U:\OP\OP4.USE------- include("U:\CP\CP1.USE"). ------- start included file U:\CP\CP1.USE------- list(usable). 296 [] subclass(cart(x,y),cart(V,V)). 297 [] -member(u,x)| -member(v,y)|member(pair(u,v),cart(V,V)). 298 [] -member(pair(u,v),cart(x,y))|member(pair(v,u),cart(y,x)). 299 [] -member(pair(pair(u,v),w),cart(cart(x,y),z))|member(pair(pair(v,u),w),cart(cart(y,x),z)). 300 [] -member(pair(pair(u,v),w),cart(cart(x,y),z))|member(pair(pair(w,u),v),cart(cart(z,x),y)). 301 [] -member(pair(pair(u,v),w),cart(cart(x,y),z))|member(pair(pair(v,w),u),cart(cart(y,z),x)). 302 [] equal(cart(x,0),0). 303 [] equal(cart(0,x),0). 304 [] -equal(cart(x,y),0)|equal(x,0)|equal(y,0). 305 [] -equal(cart(V,V),0). 306 [] -member(x,cart(y,z))|member(first(x),y). 307 [] -member(x,cart(y,z))|member(second(x),z). end_of_list. ------- end included file U:\CP\CP1.USE------- include("U:\CP\CP2.USE"). ------- start included file U:\CP\CP2.USE------- list(usable). 308 [] -subclass(x,y)|subclass(cart(x,z),cart(y,z)). 309 [] -subclass(x,y)|subclass(cart(z,x),cart(z,y)). 310 [] subclass(cart(intersection(x,y),z),cart(x,z)). 311 [] subclass(cart(intersection(x,y),z),cart(y,z)). 312 [] subclass(cart(x,intersection(y,z)),cart(x,y)). 313 [] subclass(cart(x,intersection(y,z)),cart(x,z)). 314 [] subclass(cart(cart(x,y),z),cart(cart(V,V),V)). 315 [] equal(cart(union(x,y),z),union(cart(x,z),cart(y,z))). 316 [] equal(cart(x,union(y,z)),union(cart(x,y),cart(x,z))). 317 [] equal(intersection(cart(x,z),cart(y,z)),cart(intersection(x,y),z)). 318 [] equal(intersection(cart(x,y),cart(x,z)),cart(x,intersection(y,z))). 319 [] -subclass(x,y)| -subclass(z,u)|subclass(cart(x,z),cart(y,u)). end_of_list. ------- end included file U:\CP\CP2.USE------- include("U:\CP\CP3.USE"). ------- start included file U:\CP\CP3.USE------- list(usable). 320 [] subclass(cart(intersection(w,x),intersection(y,z)),cart(w,z)). 321 [] equal(intersection(cart(x,y),cart(z,w)),cart(intersection(x,z),intersection(y,w))). 322 [] equal(intersection(cart(x,V),cart(V,y)),cart(x,y)). 323 [] -equal(cart(x,x),cart(y,y))|equal(x,y). 324 [] -subclass(cart(x,x),cart(y,y))|subclass(x,y). 325 [] -subclass(cart(u,v),cart(x,y))|equal(u,0)|subclass(v,y). 326 [] -subclass(cart(u,v),cart(x,y))|equal(v,0)|subclass(u,x). end_of_list. ------- end included file U:\CP\CP3.USE------- include("U:\CP\CP-SS.USE"). ------- start included file U:\CP\CP-SS.USE------- list(usable). 327 [] -member(x,cart(singleton(y),singleton(z)))|equal(x,pair(y,z)). 328 [] equal(cart(singleton(x),singleton(y)),0)|member(pair(x,y),cart(V,V)). 329 [] -equal(cart(singleton(x),singleton(y)),singleton(pair(x,y)))|member(pair(x,y),cart(V,V)). 330 [] subclass(cart(singleton(x),singleton(y)),singleton(pair(x,y))). 331 [] -member(pair(x,y),cart(V,V))|equal(cart(singleton(x),singleton(y)),singleton(pair(x,y))). 332 [] -member(pair(x,y),cart(V,V))|subclass(cart(singleton(z),pairset(x,y)),pairset(pair(z,x),pair(z,y))). 333 [] -member(x,cart(V,V))|equal(cart(singleton(first(x)),singleton(second(x))),singleton(x)). 334 [] -member(pair(x,y),cart(V,V))|member(pair(x,y),cart(singleton(x),singleton(y))). 335 [] -equal(cart(singleton(x),singleton(y)),0)| -member(pair(x,y),cart(V,V)). end_of_list. ------- end included file U:\CP\CP-SS.USE------- include("U:\CP\CP-C.USE"). ------- start included file U:\CP\CP-C.USE------- list(usable). 336 [] equal(union(cart(x,y),cart(complement(x),y)),cart(V,y)). 337 [] equal(union(cart(x,y),cart(x,complement(y))),cart(x,V)). 338 [] subclass(cart(complement(x),y),complement(cart(x,y))). 339 [] subclass(cart(x,complement(y)),complement(cart(x,y))). 340 [] equal(intersection(cart(x,y),complement(cart(z,y))),cart(intersection(x,complement(z)),y)). 341 [] equal(intersection(cart(x,y),complement(cart(x,z))),cart(x,intersection(y,complement(z)))). 342 [] equal(complement(cart(x,y)),union(complement(cart(x,V)),complement(cart(V,y)))). 343 [] equal(intersection(cart(V,V),complement(cart(x,y))),union(cart(complement(x),V),cart(V,complement(y)))). end_of_list. ------- end included file U:\CP\CP-C.USE------- include("U:\RS\RS.USE"). ------- start included file U:\RS\RS.USE------- list(usable). 344 [] equal(intersection(x,cart(y,z)),restrict(x,y,z)). 345 [] -member(pair(x,y),restrict(z,u,v))|member(pair(x,y),z). 346 [] -member(pair(x,y),restrict(z,u,v))|member(x,u). 347 [] -member(pair(x,y),restrict(z,u,v))|member(y,v). 348 [] -member(pair(x,y),z)| -member(pair(x,y),cart(u,v))|member(pair(x,y),restrict(z,u,v)). 349 [] equal(restrict(restrict(x,y,z),u,v),restrict(x,intersection(y,u),intersection(z,v))). 350 [] equal(restrict(V,x,y),cart(x,y)). 351 [] equal(restrict(0,x,y),0). 352 [] equal(restrict(x,0,y),0). 353 [] equal(restrict(x,y,0),0). 354 [] equal(restrict(union(x,y),z,u),union(restrict(x,z,u),restrict(y,z,u))). 355 [] equal(restrict(x,union(y,z),u),union(restrict(x,y,u),restrict(x,z,u))). 356 [] equal(restrict(x,y,union(z,u)),union(restrict(x,y,z),restrict(x,y,u))). 357 [] -member(x,D(restrict(E,y,singleton(z))))|member(x,intersection(y,z)). 358 [] -member(x,V)| -member(y,intersection(z,x))|member(y,D(restrict(E,z,singleton(x)))). 359 [] -member(x,V)|equal(D(restrict(E,y,singleton(x))),intersection(y,x)). 360 [] subclass(restrict(x,y,z),x). 361 [] subclass(restrict(x,y,z),cart(y,z)). 362 [] -subclass(x,y)|subclass(restrict(x,z,u),restrict(y,z,u)). 363 [] -subclass(x,y)|subclass(restrict(z,x,u),restrict(z,y,u)). 364 [] -subclass(x,y)|subclass(restrict(z,u,x),restrict(z,u,y)). 365 [] equal(restrict(cart(x,y),x,y),cart(x,y)). 366 [] equal(restrict(cart(x,y),z,u),cart(intersection(x,z),intersection(y,u))). 367 [] equal(intersection(x,restrict(y,z,u)),restrict(intersection(x,y),z,u)). 368 [] equal(intersection(restrict(x,y,z),u),restrict(intersection(x,u),y,z)). 369 [] -subclass(x,cart(y,z))|equal(restrict(intersection(x,u),y,z),intersection(x,u)). 370 [] equal(complement(restrict(x,y,z)),union(complement(x),complement(cart(y,z)))). 371 [] equal(image(restrict(x,V,V),y),image(x,y)). end_of_list. ------- end included file U:\RS\RS.USE------- include("U:\DO\DO1.USE"). ------- start included file U:\DO\DO1.USE------- list(usable). 372 [] equal(restrict(x,singleton(y),V),0)|member(y,D(x)). 373 [] -member(x,D(y))|member(notsub(restrict(y,singleton(x),V),0),y). 374 [] -member(x,D(y))|equal(first(notsub(restrict(y,singleton(x),V),0)),x). 375 [] -member(x,D(y))|equal(notsub(restrict(y,singleton(x),V),0),pair(x,ran(y,x,V))). 376 [] -member(x,D(y))|member(ran(y,x,V),V). 377 [] -member(x,D(y))|member(pair(x,ran(y,x,V)),cart(V,V)). 378 [] -member(x,D(y))|member(pair(x,ran(y,x,V)),y). 379 [] -member(pair(x,y),z)| -member(pair(x,y),cart(V,V))|member(x,D(z)). 380 [] -member(pair(x,y),z)| -subclass(z,cart(V,V))|member(x,D(z)). 381 [] equal(D(0),0). 382 [] equal(D(V),V). 383 [] -subclass(x,y)|subclass(D(x),D(y)). 384 [] subclass(D(intersection(x,y)),D(x)). 385 [] subclass(D(intersection(x,y)),D(y)). 386 [] equal(D(union(x,y)),union(D(x),D(y))). 387 [] subclass(D(intersection(x,y)),intersection(D(x),D(y))). end_of_list. ------- end included file U:\DO\DO1.USE------- include("U:\DO\DO2-A.USE"). ------- start included file U:\DO\DO2-A.USE------- list(usable). 388 [] -member(x,y)| -member(x,cart(complement(D(y)),V)). 389 [] equal(restrict(x,complement(D(x)),V),0). 390 [] disjoint(x,cart(complement(D(x)),V)). 391 [] -member(x,y)| -member(x,cart(V,V))|member(first(x),D(y)). 392 [] -member(x,y)| -member(x,cart(V,V))|member(x,cart(D(y),V)). 393 [] subclass(intersection(x,cart(V,y)),cart(D(x),y)). 394 [] subclass(restrict(x,V,V),cart(D(x),V)). 395 [] -equal(D(x),0)|equal(restrict(x,V,V),0). 396 [] -equal(D(x),0)|equal(intersection(x,cart(V,V)),0). 397 [] equal(D(intersection(x,cart(V,V))),D(x)). 398 [] subclass(D(cart(x,y)),x). 399 [] -subclass(x,cart(y,z))|subclass(D(x),y). 400 [] equal(x,0)|equal(D(cart(y,x)),y). 401 [] equal(D(cart(x,x)),x). 402 [] equal(D(cart(x,V)),x). 403 [] equal(D(complement(cart(x,V))),complement(x)). 404 [] equal(D(cart(x,singleton(singleton(y)))),x). 405 [] subclass(D(D(cart(x,y))),D(x)). 406 [] -member(x,restrict(y,z,u))|member(first(x),intersection(z,D(y))). 407 [] equal(restrict(x,intersection(y,D(x)),z),restrict(x,y,z)). 408 [] equal(restrict(x,D(x),y),restrict(x,V,y)). end_of_list. ------- end included file U:\DO\DO2-A.USE------- include("U:\DO\DO3.USE"). ------- start included file U:\DO\DO3.USE------- list(usable). 409 [] subclass(D(restrict(x,y,z)),intersection(D(x),y)). 410 [] equal(D(restrict(x,y,V)),intersection(D(x),y)). 411 [] subclass(D(restrict(x,y,z)),y). 412 [] subclass(complement(D(x)),D(complement(x))). 413 [] subclass(intersection(D(x),complement(D(y))),D(intersection(x,complement(y)))). 414 [] equal(D(restrict(x,y,z)),intersection(D(restrict(x,V,z)),y)). 415 [] -member(x,cart(V,V))|equal(D(singleton(x)),singleton(first(x))). 416 [] equal(D(singleton(x)),0)|member(x,cart(V,V)). end_of_list. ------- end included file U:\DO\DO3.USE------- include("U:\IN\IN1.USE"). ------- start included file U:\IN\IN1.USE------- list(usable). 417 [] equal(D(flip(cart(x,V))),inverse(x)). 418 [] subclass(D(flip(x)),cart(V,V)). 419 [] subclass(inverse(x),cart(V,V)). 420 [] equal(intersection(complement(cart(V,V)),inverse(x)),0). 421 [] -member(pair(x,y),inverse(z))|member(pair(y,x),z). 422 [] -member(pair(x,y),z)| -member(pair(x,y),cart(V,V))|member(pair(y,x),inverse(z)). 423 [] -member(pair(x,y),z)| -subclass(z,cart(V,V))|member(pair(y,x),inverse(z)). 424 [] equal(inverse(0),0). 425 [] equal(inverse(V),cart(V,V)). 426 [] -subclass(x,y)|subclass(inverse(x),inverse(y)). 427 [] equal(inverse(union(x,y)),union(inverse(x),inverse(y))). 428 [] equal(inverse(intersection(x,y)),intersection(inverse(x),inverse(y))). 429 [] -disjoint(x,y)|disjoint(inverse(x),inverse(y)). 430 [] -subclass(inverse(x),inverse(y))|subclass(restrict(x,V,V),y). 431 [] -subclass(x,cart(V,V))| -subclass(inverse(x),inverse(y))|subclass(x,y). 432 [] -subclass(x,inverse(y))|subclass(inverse(x),y). end_of_list. ------- end included file U:\IN\IN1.USE------- include("U:\IN\IN2.USE"). ------- start included file U:\IN\IN2.USE------- list(usable). 433 [] equal(restrict(complement(inverse(x)),V,V),inverse(complement(x))). 434 [] equal(D(complement(inverse(x))),R(complement(x))). 435 [] equal(image(complement(inverse(x)),y),image(inverse(complement(x)),y)). 436 [] equal(inverse(cart(x,y)),cart(y,x)). 437 [] -subclass(x,cart(y,z))|subclass(inverse(x),cart(z,y)). 438 [] -subclass(x,cart(y,z))|subclass(R(x),z). 439 [] equal(inverse(inverse(x)),restrict(x,V,V)). 440 [] equal(R(complement(inverse(x))),D(complement(x))). 441 [] equal(R(inverse(x)),D(x)). 442 [] equal(inverse(restrict(x,y,z)),restrict(inverse(x),z,y)). 443 [] -member(pair(x,y),cart(V,V))|equal(inverse(singleton(pair(x,y))),singleton(pair(y,x))). 444 [] equal(inverse(singleton(x)),0)|member(x,cart(V,V)). 445 [] -subclass(inverse(x),complement(y))|subclass(inverse(y),complement(x)). 446 [] -disjoint(x,inverse(y))|disjoint(y,inverse(x)). end_of_list. ------- end included file U:\IN\IN2.USE------- include("U:\RA\RA1.USE"). ------- start included file U:\RA\RA1.USE------- list(usable). 447 [] -equal(restrict(x,V,singleton(y)),0)| -member(y,R(x)). 448 [] equal(restrict(x,V,singleton(y)),0)|member(y,R(x)). 449 [] -member(x,R(y))|member(notsub(restrict(y,V,singleton(x)),0),y). 450 [] -member(x,R(y))|equal(second(notsub(restrict(y,V,singleton(x)),0)),x). 451 [] -member(x,R(y))|equal(pair(dom(y,V,x),x),notsub(restrict(y,V,singleton(x)),0)). 452 [] -member(x,R(y))|member(pair(dom(y,V,x),x),cart(V,V)). 453 [] -member(x,R(y))|member(dom(y,V,x),V). 454 [] -member(x,R(y))|member(pair(dom(y,V,x),x),y). 455 [] -member(pair(x,y),z)| -member(pair(x,y),cart(V,V))|member(y,R(z)). 456 [] equal(R(0),0). 457 [] equal(R(V),V). 458 [] -member(x,union(R(y),R(z)))|member(x,R(y))|member(x,R(z)). 459 [] -subclass(x,y)|subclass(R(x),R(y)). 460 [] subclass(R(intersection(x,y)),R(x)). 461 [] subclass(R(intersection(x,y)),R(y)). 462 [] equal(R(union(x,y)),union(R(x),R(y))). end_of_list. ------- end included file U:\RA\RA1.USE------- include("U:\RA\RA2.USE"). ------- start included file U:\RA\RA2.USE------- list(usable). 463 [] subclass(restrict(x,V,V),cart(V,R(x))). 464 [] subclass(restrict(x,V,V),cart(D(x),R(x))). 465 [] subclass(intersection(x,cart(V,V)),cart(D(x),R(x))). 466 [] -member(x,y)| -member(x,cart(V,V))|member(second(x),R(y)). 467 [] -member(x,y)| -member(x,cart(V,V))|member(x,cart(V,R(y))). 468 [] equal(R(intersection(x,cart(V,V))),R(x)). 469 [] equal(x,0)|equal(R(cart(x,y)),y). 470 [] equal(R(cart(x,x)),x). 471 [] equal(R(cart(V,x)),x). 472 [] subclass(R(cart(x,y)),y). 473 [] subclass(R(D(cart(x,y))),R(x)). 474 [] -member(x,cart(V,V))|equal(R(singleton(x)),singleton(second(x))). 475 [] equal(R(singleton(x)),0)|member(x,cart(V,V)). end_of_list. ------- end included file U:\RA\RA2.USE------- include("U:\RA\RA3.USE"). ------- start included file U:\RA\RA3.USE------- list(usable). 476 [] equal(restrict(x,y,intersection(R(x),z)),restrict(x,y,z)). 477 [] equal(restrict(x,y,R(x)),restrict(x,y,V)). 478 [] equal(R(restrict(x,V,y)),intersection(R(x),y)). 479 [] subclass(R(restrict(x,y,z)),intersection(R(x),z)). 480 [] subclass(cart(R(restrict(x,y,z)),u),cart(intersection(R(x),z),u)). 481 [] subclass(cart(x,R(restrict(y,z,u))),cart(x,intersection(R(y),u))). 482 [] subclass(cart(R(restrict(x,y,z)),R(restrict(u,v,w))),cart(z,w)). 483 [] -member(x,R(y))|member(dom(y,V,x),D(y)). 484 [] -member(x,D(y))|member(ran(y,x,V),R(y)). 485 [] -equal(D(x),0)|equal(R(x),0). 486 [] -equal(R(x),0)|equal(D(x),0). end_of_list. ------- end included file U:\RA\RA3.USE------- include("U:\IM\IM1.USE"). ------- start included file U:\IM\IM1.USE------- list(usable). 487 [] equal(D(restrict(x,y,z)),intersection(y,image(inverse(x),z))). 488 [] equal(R(restrict(x,y,z)),intersection(z,image(x,y))). 489 [] equal(image(restrict(x,y,z),u),intersection(z,image(x,intersection(y,u)))). 490 [] equal(image(x,0),0). 491 [] equal(image(0,x),0). 492 [] subclass(image(x,y),R(x)). 493 [] subclass(image(inverse(x),y),D(x)). 494 [] equal(image(complement(cart(V,V)),x),0). 495 [] -member(x,image(y,z))| -equal(restrict(y,z,singleton(x)),0). 496 [] -member(x,image(inverse(y),z))| -equal(restrict(y,singleton(x),z),0). 497 [] member(x,image(y,z))|equal(restrict(y,z,singleton(x)),0). 498 [] member(x,image(inverse(y),z))|equal(restrict(y,singleton(x),z),0). 499 [] -member(x,image(y,z))|member(notsub(restrict(y,z,singleton(x)),0),y). 500 [] -member(x,image(inverse(y),z))|member(notsub(restrict(y,singleton(x),z),0),y). 501 [] -member(x,image(y,z))|equal(second(notsub(restrict(y,z,singleton(x)),0)),x). 502 [] -member(x,image(inverse(y),z))|equal(first(notsub(restrict(y,singleton(x),z),0)),x). 503 [] -member(x,image(y,z))|equal(notsub(restrict(y,z,singleton(x)),0),pair(dom(y,z,x),x)). 504 [] -member(x,image(inverse(y),z))|equal(notsub(restrict(y,singleton(x),z),0),pair(x,ran(y,x,z))). 505 [] -member(x,image(y,z))|member(dom(y,z,x),z). 506 [] -member(x,image(y,singleton(z)))|member(pair(z,x),y). 507 [] -member(x,image(inverse(y),z))|member(ran(y,x,z),z). 508 [] subclass(cart(singleton(x),image(y,singleton(x))),y). 509 [] -member(x,y)| -member(pair(x,z),u)| -member(pair(x,z),cart(V,V))|member(z,image(u,y)). 510 [] -subclass(cart(x,y),z)|equal(x,0)|subclass(y,image(z,x)). 511 [] -member(pair(x,y),z)| -member(pair(x,y),cart(V,V))|member(y,image(z,singleton(x))). 512 [] -member(x,y)| -member(pair(x,z),u)| -subclass(u,cart(V,V))|member(z,image(u,y)). 513 [] -subclass(x,complement(image(y,z)))|subclass(cart(z,x),complement(y)). 514 [] -disjoint(x,image(y,z))|disjoint(cart(z,x),y). 515 [] -disjoint(x,image(inverse(y),z))|disjoint(cart(x,z),y). end_of_list. ------- end included file U:\IM\IM1.USE------- include("U:\IM\IM2.USE"). ------- start included file U:\IM\IM2.USE------- list(usable). 516 [] -member(x,image(y,z))|member(pair(dom(y,z,x),x),cart(V,V)). 517 [] -member(x,image(inverse(y),z))|member(pair(x,ran(y,x,z)),cart(V,V)). 518 [] -member(x,image(y,z))|member(pair(dom(y,z,x),x),y). 519 [] -member(x,image(inverse(y),z))|member(pair(x,ran(y,x,z)),y). 520 [] -subclass(cart(x,y),z)|subclass(y,complement(image(complement(z),x))). 521 [] -disjoint(cart(x,y),z)|disjoint(y,image(z,x)). 522 [] -disjoint(cart(x,y),z)|disjoint(x,image(inverse(z),y)). 523 [] -disjoint(x,image(y,z))|disjoint(z,image(inverse(y),x)). 524 [] -subclass(image(x,y),z)|subclass(image(inverse(x),complement(z)),complement(y)). 525 [] -subclass(image(inverse(x),complement(y)),complement(z))|subclass(image(x,z),y). 526 [] -equal(image(complement(x),y),V)| -subclass(cart(y,y),x). 527 [] equal(image(x,D(x)),R(x)). 528 [] equal(image(x,V),R(x)). 529 [] -subclass(D(x),y)|equal(image(x,y),R(x)). 530 [] -subclass(x,cart(y,V))|equal(image(x,y),R(x)). 531 [] equal(image(inverse(x),R(x)),D(x)). 532 [] -subclass(x,y)|subclass(image(z,x),image(z,y)). 533 [] -subclass(x,y)|subclass(image(x,z),image(y,z)). 534 [] equal(image(x,union(y,z)),union(image(x,y),image(x,z))). 535 [] equal(union(image(x,y),image(x,complement(y))),R(x)). 536 [] equal(union(image(x,y),image(x,intersection(z,complement(y)))),union(image(x,y),image(x,z))). 537 [] equal(image(union(x,y),z),union(image(x,z),image(y,z))). 538 [] subclass(image(intersection(x,y),z),intersection(image(x,z),image(y,z))). 539 [] equal(image(intersection(x,y),singleton(z)),intersection(image(x,singleton(z)),image(y,singleton(z)))). 540 [] -member(x,image(y,z))|member(dom(y,z,x),D(y)). 541 [] -equal(intersection(x,D(y)),0)|equal(image(y,x),0). 542 [] -equal(image(x,y),0)|equal(intersection(y,D(x)),0). 543 [] -equal(image(x,y),0)|disjoint(y,D(x)). 544 [] -disjoint(D(x),y)|equal(image(x,y),0). 545 [] equal(image(x,singleton(y)),0)|member(y,D(x)). 546 [] -equal(image(x,singleton(y)),0)| -member(y,D(x)). 547 [] -member(x,complement(image(E,complement(y))))|subclass(x,y). 548 [] -member(x,V)| -subclass(x,y)|member(x,complement(image(E,complement(y)))). 549 [] equal(x,0)|equal(image(V,x),V). 550 [] equal(0,x)|subclass(complement(image(V,x)),y). 551 [] equal(image(V,singleton(0)),V). 552 [] equal(cart(V,intersection(complement(image(V,x)),y)),cart(complement(image(V,x)),y)). 553 [] equal(cart(D(x),image(V,x)),cart(D(x),V)). 554 [] equal(cart(image(x,y),image(V,y)),cart(image(x,y),V)). 555 [] equal(cart(image(x,y),intersection(z,image(V,y))),cart(image(x,y),z)). 556 [] equal(cart(V,intersection(x,image(V,y))),cart(image(V,y),x)). 557 [] equal(cart(x,intersection(y,image(V,x))),cart(x,y)). 558 [] equal(cart(intersection(x,image(V,y)),z),cart(x,intersection(image(V,y),z))). 559 [] equal(cart(R(x),image(V,x)),cart(R(x),V)). 560 [] equal(intersection(singleton(x),image(V,intersection(singleton(x),y))),intersection(singleton(x),y)). 561 [] equal(cart(x,complement(image(V,x))),0). 562 [] equal(image(V,cart(x,y)),intersection(image(V,x),image(V,y))). 563 [] equal(image(V,inverse(x)),image(V,D(x))). 564 [] equal(image(V,R(x)),image(V,D(x))). 565 [] -member(x,V)|equal(image(V,singleton(x)),V). 566 [] -member(pair(x,y),cart(V,V))|member(x,image(V,singleton(y))). 567 [] -member(x,image(V,singleton(y)))|member(pair(x,y),cart(V,V)). 568 [] equal(image(V,singleton(x)),0)|member(x,V). 569 [] -subclass(image(V,x),y)|equal(x,0)|equal(y,V). 570 [] equal(union(image(V,x),image(V,singleton(x))),V). 571 [] equal(image(V,intersection(singleton(x),complement(singleton(0)))),intersection(image(V,x),image(V,singleton(x)))). 572 [] equal(image(x,image(V,y)),intersection(R(x),image(V,y))). 573 [] equal(image(x,complement(image(V,y))),intersection(R(x),complement(image(V,y)))). 574 [] equal(image(image(V,x),y),intersection(image(V,x),image(V,y))). 575 [] equal(D(image(V,x)),image(V,x)). 576 [] equal(R(image(V,x)),image(V,x)). 577 [] subclass(x,image(V,x)). 578 [] -disjoint(image(V,x),image(V,y))|equal(x,0)|equal(y,0). 579 [] equal(image(V,image(x,y)),image(V,intersection(D(x),y))). 580 [] subclass(image(x,y),image(V,x)). 581 [] equal(cart(x,image(V,x)),cart(x,V)). end_of_list. ------- end included file U:\IM\IM2.USE------- include("U:\IM\IM3.USE"). ------- start included file U:\IM\IM3.USE------- list(usable). 582 [] equal(image(complement(x),singleton(y)),intersection(image(V,singleton(y)),complement(image(x,singleton(y))))). 583 [] equal(D(cart(x,y)),intersection(x,image(V,y))). 584 [] equal(D(singleton(pair(x,y))),intersection(singleton(x),image(V,singleton(y)))). 585 [] equal(R(cart(x,y)),intersection(y,image(V,x))). 586 [] equal(R(singleton(pair(x,y))),intersection(singleton(y),image(V,singleton(x)))). 587 [] equal(image(cart(x,y),z),intersection(y,image(V,intersection(x,z)))). 588 [] -member(x,image(y,singleton(z)))|member(pair(x,z),cart(V,V)). 589 [] -member(x,image(y,singleton(z)))| -member(z,image(u,singleton(v)))|member(x,image(y,image(u,singleton(v)))). 590 [] subclass(image(x,intersection(y,z)),intersection(image(x,y),image(x,z))). 591 [] -member(x,y)| -member(z,complement(image(u,y)))| -member(pair(x,z),u). 592 [] -member(x,y)| -member(z,complement(image(u,y)))|member(pair(x,z),complement(u)). 593 [] subclass(cart(x,complement(image(y,x))),complement(y)). 594 [] -subclass(x,image(y,z))|subclass(x,image(y,intersection(z,image(inverse(y),x)))). end_of_list. ------- end included file U:\IM\IM3.USE------- include("U:\SC\SC1.USE"). ------- start included file U:\SC\SC1.USE------- list(usable). 595 [] equal(D(restrict(E,V,x)),U(x)). 596 [] equal(image(inverse(E),x),U(x)). 597 [] -member(x,U(y))|member(x,ran(E,x,y)). 598 [] -member(x,U(y))|member(ran(E,x,y),y). 599 [] -member(x,y)| -member(y,z)|member(x,U(z)). 600 [] -subclass(x,y)|subclass(U(x),U(y)). 601 [] -member(x,y)|subclass(x,U(y)). 602 [] subclass(x,P(U(x))). 603 [] equal(U(0),0). 604 [] equal(U(V),V). 605 [] equal(U(image(V,x)),image(V,x)). 606 [] equal(U(complement(image(V,x))),complement(image(V,x))). 607 [] equal(U(singleton(0)),0). 608 [] -member(x,V)|subclass(x,U(singleton(x))). 609 [] -member(x,V)|equal(U(singleton(x)),x). 610 [] equal(U(singleton(singleton(x))),singleton(x)). 611 [] equal(intersection(x,image(V,singleton(x))),U(singleton(x))). 612 [] subclass(U(singleton(x)),x). 613 [] -subclass(x,singleton(y))|equal(x,0)|equal(singleton(U(x)),x). 614 [] equal(image(V,complement(singleton(x))),V). 615 [] -member(x,cart(V,V))|equal(U(D(singleton(x))),first(x)). 616 [] -member(x,cart(V,V))|equal(U(R(singleton(x))),second(x)). end_of_list. ------- end included file U:\SC\SC1.USE------- include("U:\SC\SC2.USE"). ------- start included file U:\SC\SC2.USE------- list(usable). 617 [] subclass(U(pairset(x,y)),union(x,y)). 618 [] -member(pair(x,y),cart(V,V))|equal(U(pairset(x,y)),union(x,y)). 619 [] -member(pair(x,y),cart(V,V))|member(union(x,y),V). 620 [] -member(x,V)|member(union(x,singleton(y)),V). 621 [] equal(U(pair(x,y)),pairset(x,singleton(y))). 622 [] equal(U(union(x,y)),union(U(x),U(y))). 623 [] subclass(complement(U(x)),U(complement(x))). 624 [] subclass(U(intersection(x,y)),intersection(U(x),U(y))). 625 [] subclass(D(x),U(U(x))). 626 [] subclass(R(x),U(U(U(x)))). end_of_list. ------- end included file U:\SC\SC2.USE------- include("U:\A\A1.USE"). ------- start included file U:\A\A1.USE------- list(usable). 627 [] equal(complement(D(restrict(complement(E),V,x))),A(x)). 628 [] equal(complement(image(inverse(complement(E)),x)),A(x)). 629 [] equal(image(inverse(complement(E)),x),complement(A(x))). 630 [] equal(image(complement(inverse(E)),x),complement(A(x))). 631 [] -member(x,A(y))| -member(z,y)|member(x,z). 632 [] -member(x,y)|subclass(A(y),x). 633 [] -member(0,x)|equal(A(x),0). 634 [] equal(x,0)|subclass(A(x),U(x)). 635 [] subclass(A(x),U(y))|disjoint(x,y). 636 [] -member(x,ran(complement(E),x,y))|member(x,A(y)). 637 [] -member(x,V)|member(x,A(y))|member(ran(complement(E),x,y),y). 638 [] equal(A(0),V). 639 [] equal(A(V),0). 640 [] equal(A(image(V,x)),complement(image(V,x))). 641 [] equal(A(complement(image(V,x))),image(V,x)). 642 [] equal(A(intersection(x,image(V,y))),union(A(x),complement(image(V,y)))). 643 [] equal(A(intersection(x,complement(image(V,y)))),union(A(x),image(V,y))). 644 [] -member(x,V)|equal(A(singleton(x)),x). 645 [] equal(A(singleton(x)),union(x,complement(image(V,singleton(x))))). 646 [] -subclass(x,y)|subclass(A(y),A(x)). 647 [] equal(A(union(x,y)),intersection(A(x),A(y))). end_of_list. ------- end included file U:\A\A1.USE------- include("U:\A\A2.USE"). ------- start included file U:\A\A2.USE------- list(usable). 648 [] -member(pair(x,y),cart(V,V))|equal(A(pairset(x,y)),intersection(x,y)). 649 [] -member(x,V)| -subclass(x,y)|equal(A(pairset(x,y)),x). 650 [] equal(A(pair(x,y)),singleton(x)). 651 [] -member(x,cart(V,V))|equal(A(x),singleton(first(x))). 652 [] -member(x,cart(V,V))|equal(A(A(x)),first(x)). 653 [] subclass(singleton(x),A(image(E,singleton(x)))). 654 [] -member(x,V)|equal(A(image(E,singleton(x))),singleton(x)). 655 [] equal(A(image(E,singleton(x))),union(singleton(x),complement(image(V,singleton(x))))). end_of_list. ------- end included file U:\A\A2.USE------- include("U:\PC\PC0-A.USE"). ------- start included file U:\PC\PC0-A.USE------- list(usable). 656 [] equal(image(E,complement(x)),complement(P(x))). 657 [] equal(complement(image(E,x)),P(complement(x))). 658 [] equal(image(E,x),complement(P(complement(x)))). 659 [] subclass(intersection(image(E,x),P(y)),image(E,intersection(x,y))). end_of_list. ------- end included file U:\PC\PC0-A.USE------- include("U:\PC\PC1.USE"). ------- start included file U:\PC\PC1.USE------- list(usable). 660 [] -member(x,P(y))|subclass(x,y). 661 [] -member(x,V)| -subclass(x,y)|member(x,P(y)). 662 [] -member(x,V)|member(x,P(x)). 663 [] equal(intersection(image(V,singleton(x)),complement(image(V,intersection(x,complement(y))))),image(V,intersection(P(y),singleton(x)))). 664 [] subclass(singleton(x),P(x)). 665 [] member(singleton(x),P(P(x))). 666 [] equal(P(singleton(x)),pairset(0,singleton(x))). 667 [] -subclass(x,y)|subclass(P(x),P(y)). 668 [] member(0,P(x)). 669 [] -equal(P(x),0). 670 [] equal(P(V),V). 671 [] equal(intersection(singleton(0),P(x)),singleton(0)). 672 [] equal(A(P(x)),0). 673 [] -member(x,y)|member(singleton(x),P(y)). 674 [] -member(x,y)| -member(z,y)|member(pairset(x,z),P(y)). 675 [] -member(x,y)| -member(singleton(z),y)|member(pair(x,z),P(P(y))). 676 [] -member(x,cart(y,z))|member(x,P(P(union(y,P(z))))). 677 [] subclass(cart(x,y),P(P(union(x,P(y))))). 678 [] equal(U(P(x)),x). 679 [] -subclass(x,P(y))|equal(0,x)|subclass(A(x),y). 680 [] -equal(singleton(x),0)|equal(singleton(P(x)),0). 681 [] equal(intersection(P(x),P(y)),P(intersection(x,y))). end_of_list. ------- end included file U:\PC\PC1.USE------- include("U:\PC\PC2.USE"). ------- start included file U:\PC\PC2.USE------- list(usable). 682 [] equal(P(0),singleton(0)). 683 [] -subclass(P(x),singleton(y))|equal(x,0). 684 [] -subclass(P(x),singleton(y))|equal(y,0). 685 [] -equal(U(x),0)|equal(x,0)|equal(x,singleton(0)). 686 [] equal(P(image(V,x)),union(singleton(0),image(V,x))). 687 [] equal(P(complement(image(V,x))),union(singleton(0),complement(image(V,x)))). 688 [] subclass(P(x),union(singleton(0),image(E,x))). 689 [] -member(x,P(y))| -member(z,P(y))|member(union(x,z),P(y)). 690 [] subclass(union(P(x),P(y)),P(union(x,y))). 691 [] -subclass(x,P(y))|subclass(U(x),y). 692 [] -subclass(U(x),y)|subclass(x,P(y)). 693 [] equal(image(V,intersection(x,complement(P(y)))),image(V,intersection(complement(y),U(x)))). 694 [] -member(x,P(P(y)))|member(U(x),P(y)). 695 [] -subclass(P(x),y)|subclass(x,U(y)). 696 [] -member(x,y)|member(U(x),P(U(U(y)))). 697 [] -member(x,y)|member(P(x),P(P(U(y)))). end_of_list. ------- end included file U:\PC\PC2.USE------- include("U:\RL\RL.USE"). ------- start included file U:\RL\RL.USE------- list(usable). 698 [] subclass(restrict(x,y,z),cart(V,V)). 699 [] -subclass(x,cart(V,V))|subclass(x,cart(D(x),R(x))). 700 [] -subclass(x,cart(V,V))|subclass(x,cart(D(x),image(x,D(x)))). 701 [] -subclass(x,cart(V,V))|equal(restrict(x,D(x),R(x)),x). 702 [] -subclass(x,cart(cart(V,V),V))|subclass(x,cart(cart(D(D(x)),R(D(x))),R(x))). 703 [] -subclass(x,cart(V,V))|equal(inverse(inverse(x)),x). 704 [] -equal(inverse(x),inverse(y))| -subclass(x,cart(V,V))| -subclass(y,cart(V,V))|equal(x,y). 705 [] -equal(inverse(x),inverse(y))| -subclass(union(x,y),cart(V,V))|equal(x,y). 706 [] equal(inverse(inverse(inverse(x))),inverse(x)). 707 [] equal(inverse(inverse(E)),E). 708 [] -subclass(x,cart(V,V))|equal(restrict(x,V,V),x). 709 [] -subclass(x,inverse(x))|equal(inverse(x),x). 710 [] -subclass(x,inverse(x))|equal(R(x),D(x)). 711 [] -subclass(x,inverse(x))|subclass(x,cart(D(x),D(x))). end_of_list. ------- end included file U:\RL\RL.USE------- include("U:\CR\CR.USE"). ------- start included file U:\CR\CR.USE------- list(usable). 712 [] equal(restrict(complement(x),V,V),compreln(x)). 713 [] -member(x,cart(V,V))|member(x,y)|member(x,composite(Id,complement(y))). 714 [] subclass(compreln(x),cart(V,V)). 715 [] disjoint(compreln(x),x). 716 [] subclass(compreln(x),complement(x)). 717 [] equal(compreln(restrict(x,V,V)),compreln(x)). 718 [] equal(compreln(compreln(x)),restrict(x,V,V)). 719 [] equal(compreln(union(x,y)),intersection(compreln(x),compreln(y))). 720 [] equal(compreln(intersection(x,y)),union(compreln(x),compreln(y))). end_of_list. ------- end included file U:\CR\CR.USE------- include("U:\FL\FL1.USE"). ------- start included file U:\FL\FL1.USE------- list(usable). 721 [] -subclass(x,y)|subclass(flip(x),flip(y)). 722 [] equal(flip(intersection(x,y)),intersection(flip(x),flip(y))). 723 [] equal(flip(union(x,y)),union(flip(x),flip(y))). 724 [] subclass(flip(flip(x)),x). 725 [] -subclass(x,flip(x))|equal(flip(x),x). 726 [] -subclass(x,cart(cart(V,V),V))|equal(flip(flip(x)),x). 727 [] equal(flip(flip(flip(x))),flip(x)). end_of_list. ------- end included file U:\FL\FL1.USE------- include("U:\FL\FL2.USE"). ------- start included file U:\FL\FL2.USE------- list(usable). 728 [] subclass(cart(inverse(x),y),cart(cart(V,V),V)). 729 [] equal(flip(cart(x,y)),cart(inverse(x),y)). 730 [] equal(flip(intersection(x,cart(cart(V,V),V))),flip(x)). 731 [] equal(flip(flip(x)),intersection(x,cart(cart(V,V),V))). 732 [] equal(flip(V),cart(cart(V,V),V)). 733 [] equal(flip(0),0). 734 [] equal(D(flip(x)),inverse(D(x))). 735 [] equal(R(flip(x)),image(x,cart(V,V))). 736 [] subclass(flip(x),cart(inverse(D(x)),R(x))). end_of_list. ------- end included file U:\FL\FL2.USE------- include("U:\RO\RO1.USE"). ------- start included file U:\RO\RO1.USE------- list(usable). 737 [] equal(intersection(cart(cart(V,V),V),rotate(x)),rotate(x)). 738 [] equal(rotate(cart(cart(x,y),z)),cart(cart(z,x),y)). 739 [] -subclass(x,y)|subclass(rotate(x),rotate(y)). 740 [] equal(rotate(intersection(x,y)),intersection(rotate(x),rotate(y))). 741 [] equal(rotate(union(x,y)),union(rotate(x),rotate(y))). end_of_list. ------- end included file U:\RO\RO1.USE------- include("U:\RO\RO2.USE"). ------- start included file U:\RO\RO2.USE------- list(usable). 742 [] equal(rotate(flip(rotate(x))),flip(x)). 743 [] equal(rotate(rotate(x)),flip(rotate(flip(x)))). 744 [] -subclass(x,rotate(x))|equal(rotate(x),x). end_of_list. ------- end included file U:\RO\RO2.USE------- include("U:\RO\RO3.USE"). ------- start included file U:\RO\RO3.USE------- list(usable). 745 [] subclass(rotate(x),cart(cart(R(x),D(D(x))),R(D(x)))). 746 [] equal(R(rotate(x)),R(D(x))). 747 [] subclass(D(rotate(x)),cart(R(x),D(D(x)))). 748 [] subclass(D(D(rotate(x))),R(x)). 749 [] subclass(R(D(rotate(x))),D(D(x))). 750 [] equal(rotate(0),0). 751 [] equal(rotate(V),cart(cart(V,V),V)). 752 [] subclass(rotate(cart(x,y)),cart(cart(y,D(x)),R(x))). 753 [] equal(D(rotate(cart(x,y))),cart(y,D(x))). end_of_list. ------- end included file U:\RO\RO3.USE------- include("U:\CO\CO1-B.USE"). ------- start included file U:\CO\CO1-B.USE------- list(usable). 754 [] equal(composite(0,x),0). 755 [] equal(composite(x,0),0). 756 [] subclass(composite(x,y),cart(V,V)). 757 [] equal(intersection(complement(cart(V,V)),composite(x,y)),0). 758 [] equal(intersection(cart(V,V),composite(x,y)),composite(x,y)). 759 [] equal(composite(cart(x,y),cart(z,u)),cart(z,y))|equal(intersection(x,u),0). 760 [] equal(composite(cart(V,x),cart(y,V)),cart(y,x)). 761 [] equal(composite(union(x,y),z),union(composite(x,z),composite(y,z))). 762 [] equal(composite(x,union(y,z)),union(composite(x,y),composite(x,z))). 763 [] equal(composite(intersection(x,cart(V,V)),y),composite(x,y)). 764 [] equal(composite(x,intersection(y,cart(V,V))),composite(x,y)). 765 [] equal(composite(complement(cart(V,V)),x),0). 766 [] equal(composite(x,complement(cart(V,V))),0). 767 [] equal(inverse(composite(x,y)),composite(inverse(y),inverse(x))). 768 [] -subclass(composite(inverse(x),inverse(y)),inverse(z))|subclass(composite(y,x),z). end_of_list. ------- end included file U:\CO\CO1-B.USE------- include("U:\CO\CO2-A.USE"). ------- start included file U:\CO\CO2-A.USE------- list(usable). 769 [] -subclass(x,y)|subclass(composite(x,z),composite(y,z)). 770 [] -subclass(x,y)|subclass(composite(z,x),composite(z,y)). 771 [] -subclass(x,y)| -subclass(z,u)|subclass(composite(x,z),composite(y,u)). 772 [] subclass(composite(intersection(x,y),z),composite(x,z)). 773 [] subclass(composite(intersection(x,y),z),composite(y,z)). 774 [] subclass(composite(x,intersection(y,z)),composite(x,y)). 775 [] subclass(composite(x,intersection(y,z)),composite(x,z)). 776 [] subclass(composite(intersection(x,y),z),intersection(composite(x,z),composite(y,z))). 777 [] subclass(composite(x,intersection(y,z)),intersection(composite(x,y),composite(x,z))). 778 [] -member(pair(x,y),z)| -member(pair(x,y),cart(V,V))| -member(pair(y,u),v)| -member(pair(y,u),cart(V,V))|member(pair(x,u),composite(v,z)). 779 [] -member(pair(x,y),z)| -member(pair(y,u),v)| -member(pair(pair(x,u),y),cart(cart(V,V),V))|member(pair(x,u),composite(v,z)). 780 [] equal(composite(cart(V,x),y),cart(D(y),x)). 781 [] subclass(composite(x,y),cart(D(y),V)). 782 [] subclass(D(composite(x,y)),D(y)). 783 [] equal(composite(V,x),cart(D(x),V)). 784 [] equal(composite(image(V,x),y),cart(D(y),image(V,x))). 785 [] equal(composite(x,cart(y,V)),cart(y,R(x))). 786 [] subclass(composite(x,y),cart(V,R(x))). 787 [] subclass(R(composite(x,y)),R(x)). 788 [] equal(composite(x,V),cart(V,R(x))). 789 [] equal(composite(x,image(V,y)),cart(image(V,y),R(x))). 790 [] subclass(composite(x,y),cart(D(y),R(x))). end_of_list. ------- end included file U:\CO\CO2-A.USE------- include("U:\CO\CO3-C.USE"). ------- start included file U:\CO\CO3-C.USE------- list(usable). 791 [] equal(composite(x,cart(y,z)),cart(y,image(x,z))). 792 [] equal(composite(cart(x,y),z),cart(image(inverse(z),x),y)). 793 [] -member(x,image(y,image(z,singleton(u))))|member(pair(u,x),cart(V,V)). 794 [] -member(x,image(y,image(z,singleton(u))))|member(pair(u,x),composite(y,z)). 795 [] member(pair(x,y),composite(z,u))|disjoint(image(u,singleton(x)),image(inverse(z),singleton(y))). 796 [] -member(pair(x,y),composite(z,u))|member(y,image(z,image(u,singleton(x)))). 797 [] -subclass(image(x,image(y,singleton(first(notsub(composite(x,y),z))))),image(z,singleton(first(notsub(composite(x,y),z)))))|subclass(composite(x,y),z). 798 [] -equal(intersection(image(inverse(x),singleton(y)),image(z,singleton(u))),0)| -member(pair(u,y),composite(x,z)). 799 [] equal(image(composite(x,y),z),image(x,image(y,z))). 800 [] equal(composite(composite(x,y),z),composite(x,composite(y,z))). 801 [] -member(x,D(y))| -subclass(R(y),D(z))|member(x,image(inverse(y),D(z))). 802 [] -subclass(R(x),D(y))|equal(D(composite(y,x)),D(x)). 803 [] equal(R(composite(x,y)),image(x,R(y))). 804 [] equal(D(composite(x,y)),image(inverse(y),D(x))). 805 [] -subclass(composite(x,y),composite(y,x))|subclass(image(inverse(y),D(x)),D(x)). 806 [] equal(D(composite(x,inverse(y))),image(y,D(x))). 807 [] equal(D(composite(x,E)),U(D(x))). 808 [] subclass(composite(x,y),cart(image(inverse(y),D(x)),image(x,R(y)))). 809 [] -disjoint(D(x),R(y))|equal(composite(x,y),0). 810 [] -disjoint(D(x),D(y))|equal(composite(x,inverse(y)),0). 811 [] -disjoint(cart(V,D(x)),y)|equal(composite(x,y),0). 812 [] -disjoint(x,cart(R(y),V))|equal(composite(x,y),0). end_of_list. ------- end included file U:\CO\CO3-C.USE------- include("U:\CO\CO4-B.USE"). ------- start included file U:\CO\CO4-B.USE------- list(usable). 813 [] -member(pair(x,y),cart(cart(V,V),V))| -member(pair(y,second(x)),z)| -member(pair(first(x),y),u)|member(x,composite(z,u)). 814 [] equal(dom(x,image(y,singleton(z)),u),com(x,y,z,u)). 815 [] -member(pair(x,y),composite(z,u))|member(com(z,u,x,y),V). 816 [] -member(pair(x,y),composite(z,u))|member(pair(x,com(z,u,x,y)),u). 817 [] -member(pair(x,y),composite(z,u))|member(pair(x,com(z,u,x,y)),cart(V,V)). 818 [] -member(pair(x,y),composite(z,u))|member(pair(com(z,u,x,y),y),z). 819 [] -member(pair(x,y),composite(z,u))|member(pair(com(z,u,x,y),y),cart(V,V)). 820 [] -member(x,image(y,z))| -member(z,V)|member(pair(z,x),composite(y,inverse(E))). 821 [] subclass(cart(singleton(x),image(y,x)),composite(y,inverse(E))). 822 [] -member(pair(x,y),composite(z,inverse(E)))|member(y,image(z,x)). 823 [] -member(pair(x,y),composite(complement(E),composite(z,inverse(E))))| -subclass(image(z,x),y). 824 [] -member(pair(x,y),composite(E,complement(composite(z,inverse(E)))))| -subclass(y,image(z,x)). 825 [] -member(pair(x,image(y,x)),composite(complement(E),composite(y,inverse(E)))). 826 [] -member(pair(x,image(y,x)),composite(E,complement(composite(y,inverse(E))))). 827 [] subclass(intersection(complement(composite(x,y)),composite(z,y)),composite(intersection(complement(x),z),y)). 828 [] subclass(intersection(complement(composite(x,y)),composite(x,z)),composite(x,intersection(complement(y),z))). 829 [] equal(flip(composite(x,y)),composite(x,flip(y))). end_of_list. ------- end included file U:\CO\CO4-B.USE------- include("U:\CO\CO5.USE"). ------- start included file U:\CO\CO5.USE------- list(usable). 830 [] -subclass(composite(complement(x),inverse(y)),complement(z))|subclass(composite(z,y),x). 831 [] -subclass(composite(x,y),z)|subclass(composite(complement(z),inverse(y)),complement(x)). 832 [] -disjoint(composite(x,y),z)|disjoint(composite(z,inverse(y)),x). 833 [] -disjoint(composite(x,y),inverse(z))|disjoint(composite(y,z),inverse(x)). 834 [] subclass(composite(complement(composite(x,y)),inverse(y)),complement(x)). 835 [] equal(union(complement(x),composite(complement(composite(x,y)),inverse(y))),complement(x)). end_of_list. ------- end included file U:\CO\CO5.USE------- include("U:\E\E1-A.USE"). ------- start included file U:\E\E1-A.USE------- list(usable). 836 [] -member(x,E)|member(first(x),second(x)). 837 [] -member(x,cart(V,V))| -member(first(x),second(x))|member(x,E). 838 [] equal(intersection(cart(V,V),E),E). 839 [] -member(pair(x,y),E)|member(pair(x,y),cart(V,V)). 840 [] -member(x,y)| -member(y,V)|member(pair(x,y),E). 841 [] equal(D(E),V). 842 [] equal(D(restrict(E,x,y)),intersection(x,U(y))). 843 [] -member(0,R(E)). 844 [] -member(x,V)|equal(x,0)|member(x,R(E)). 845 [] equal(R(E),complement(singleton(0))). 846 [] -subclass(cart(V,V),E). 847 [] -member(x,V)|member(pair(x,singleton(x)),E). 848 [] subclass(cart(x,singleton(x)),E). 849 [] -member(singleton(x),image(E,y))|member(x,y). 850 [] -member(x,image(inverse(y),singleton(z)))|member(pair(x,singleton(z)),complement(composite(E,complement(y)))). 851 [] equal(image(inverse(x),singleton(y)),0)|member(singleton(y),R(complement(composite(E,complement(x))))). 852 [] member(singleton(x),R(complement(composite(E,complement(y)))))|disjoint(y,cart(V,singleton(x))). 853 [] -member(x,R(y))|member(singleton(x),R(complement(composite(E,complement(y))))). 854 [] equal(U(R(complement(composite(E,x)))),R(complement(x))). 855 [] -member(x,V)|subclass(P(image(y,singleton(x))),R(complement(composite(E,complement(y))))). 856 [] -member(x,y)| -member(pair(y,x),inverse(complement(E))). 857 [] -member(pair(x,y),cart(V,V))|member(y,x)|member(pair(x,y),inverse(complement(E))). 858 [] -member(pair(x,y),cart(V,V))|equal(x,y)|member(pair(x,y),composite(inverse(complement(E)),E)). end_of_list. ------- end included file U:\E\E1-A.USE------- include("U:\E\E2-A.USE"). ------- start included file U:\E\E2-A.USE------- list(usable). 859 [] -member(pair(x,y),composite(E,complement(E)))|member(x,complement(A(y))). 860 [] -member(x,complement(A(y)))| -member(y,V)|member(pair(x,y),composite(E,complement(E))). 861 [] equal(composite(inverse(E),E),cart(V,V)). 862 [] -member(pair(x,y),cart(V,V))|equal(intersection(x,y),0)|member(pair(x,y),composite(E,inverse(E))). 863 [] -equal(intersection(x,y),0)| -member(pair(x,y),composite(E,inverse(E))). 864 [] -member(pair(x,y),composite(E,E))|member(x,U(y)). 865 [] -member(x,U(y))| -member(y,V)|member(pair(x,y),composite(E,E)). 866 [] -member(pair(x,y),restrict(z,V,V))| -subclass(composite(E,z),composite(E,u))|member(pair(x,y),u). 867 [] -subclass(composite(E,x),composite(E,y))|subclass(restrict(x,V,V),y). 868 [] -equal(composite(E,x),composite(E,y))|equal(restrict(x,V,V),restrict(y,V,V)). 869 [] -subclass(composite(E,x),composite(E,y))|subclass(composite(z,x),composite(z,y)). 870 [] -equal(composite(E,x),composite(E,y))|equal(composite(z,x),composite(z,y)). 871 [] -member(x,image(E,y))| -disjoint(x,y). 872 [] -member(x,V)|member(x,image(E,y))|disjoint(x,y). 873 [] -member(0,image(E,x)). 874 [] equal(composite(complement(inverse(E)),complement(E)),cart(V,V)). 875 [] equal(composite(complement(inverse(E)),complement(S)),cart(complement(singleton(0)),V)). 876 [] -member(x,image(E,singleton(y)))|member(y,x). 877 [] member(x,U(complement(y)))|subclass(image(E,singleton(x)),y). 878 [] -member(pair(x,y),cart(V,V))|member(pair(x,pairset(x,y)),E). 879 [] -member(pair(x,y),cart(V,V))|member(pair(y,pairset(x,y)),E). 880 [] equal(U(image(E,x)),image(V,x)). 881 [] -disjoint(image(E,x),image(E,y))|equal(x,0)|equal(y,0). 882 [] -subclass(image(E,x),P(y))|equal(x,0)|equal(y,V). 883 [] -equal(union(P(x),P(y)),V)|equal(x,V)|equal(y,V). 884 [] equal(U(complement(P(x))),image(V,complement(x))). end_of_list. ------- end included file U:\E\E2-A.USE------- include("U:\SR\SR1.USE"). ------- start included file U:\SR\SR1.USE------- list(usable). 885 [] subclass(S,cart(V,V)). 886 [] equal(restrict(S,V,V),S). 887 [] equal(inverse(inverse(S)),S). 888 [] -member(pair(x,y),S)|subclass(x,y). 889 [] -member(x,S)|subclass(first(x),second(x)). 890 [] -member(x,image(inverse(S),y))|subclass(x,dom(inverse(S),y,x)). 891 [] -member(x,image(S,singleton(y)))|member(y,P(x)). 892 [] -member(x,image(S,singleton(y)))|subclass(y,x). 893 [] -member(pair(x,y),cart(V,V))| -subclass(x,y)|member(pair(x,y),S). 894 [] equal(D(S),V). 895 [] equal(R(S),V). 896 [] -member(0,x)|equal(image(S,x),V). 897 [] -equal(image(S,x),V)|member(0,x). 898 [] equal(A(complement(image(S,singleton(x)))),complement(image(V,x))). 899 [] equal(union(image(V,x),image(S,singleton(x))),V). 900 [] equal(image(V,complement(image(S,x))),complement(image(V,intersection(singleton(0),x)))). 901 [] equal(image(S,P(x)),V). 902 [] -member(x,V)|equal(image(inverse(S),singleton(x)),P(x)). 903 [] equal(image(inverse(S),singleton(x)),intersection(P(x),image(V,singleton(x)))). 904 [] equal(image(complement(inverse(S)),x),complement(P(A(x)))). end_of_list. ------- end included file U:\SR\SR1.USE------- include("U:\SR\SR2.USE"). ------- start included file U:\SR\SR2.USE------- list(usable). 905 [] -subclass(x,cart(V,V))|subclass(x,composite(S,x)). 906 [] subclass(intersection(x,cart(V,V)),composite(S,x)). 907 [] -subclass(x,cart(V,V))|subclass(x,composite(x,S)). 908 [] subclass(intersection(x,cart(V,V)),composite(x,S)). 909 [] equal(composite(S,E),E). 910 [] equal(composite(S,S),S). 911 [] equal(composite(complement(S),inverse(S)),restrict(complement(S),V,V)). 912 [] equal(composite(S,inverse(S)),cart(V,V)). 913 [] equal(composite(inverse(S),S),cart(V,V)). 914 [] equal(composite(inverse(S),E),cart(V,V)). 915 [] equal(image(inverse(S),complement(P(x))),image(V,complement(x))). 916 [] equal(composite(S,complement(E)),cart(V,V)). 917 [] equal(composite(S,complement(S)),cart(complement(singleton(0)),V)). 918 [] equal(composite(inverse(E),S),cart(V,V)). 919 [] -member(pair(x,y),composite(E,complement(S)))| -subclass(x,A(y)). 920 [] -member(pair(x,y),cart(V,V))|member(pair(x,y),composite(E,complement(S)))|subclass(x,A(y)). end_of_list. ------- end included file U:\SR\SR2.USE------- include("U:\SR\SR3.USE"). ------- start included file U:\SR\SR3.USE------- list(usable). 921 [] equal(x,0)|member(0,image(inverse(S),x)). 922 [] subclass(x,image(S,x)). 923 [] -equal(image(inverse(S),x),x)|equal(image(S,complement(x)),complement(x)). 924 [] equal(image(S,complement(P(x))),complement(P(x))). 925 [] equal(image(S,complement(singleton(0))),complement(singleton(0))). 926 [] equal(intersection(P(x),image(S,singleton(x))),singleton(x)). 927 [] subclass(x,image(inverse(S),x)). 928 [] -equal(image(S,complement(x)),complement(x))|equal(image(inverse(S),x),x). 929 [] equal(A(image(S,x)),A(x)). 930 [] equal(A(image(inverse(S),x)),complement(image(V,x))). 931 [] equal(U(image(S,x)),image(V,x)). 932 [] equal(U(image(inverse(S),x)),U(x)). 933 [] subclass(image(inverse(S),x),P(U(x))). 934 [] -equal(image(inverse(S),x),V)|equal(U(x),V). 935 [] equal(image(S,image(S,x)),image(S,x)). 936 [] equal(image(inverse(S),image(inverse(S),x)),image(inverse(S),x)). 937 [] equal(image(inverse(S),P(x)),P(x)). 938 [] -member(0,image(S,x))|member(0,x). 939 [] -member(0,x)|member(0,image(S,x)). end_of_list. ------- end included file U:\SR\SR3.USE------- include("U:\ID\ID1-A.USE"). ------- start included file U:\ID\ID1-A.USE------- list(usable). 940 [] subclass(Id,S). 941 [] subclass(Id,cart(V,V)). 942 [] -FUNCTION(S). 943 [] equal(restrict(Id,V,V),Id). 944 [] equal(intersection(Id,cart(V,V)),Id). 945 [] -member(pair(x,y),Id)|equal(x,y). 946 [] -member(x,Id)|equal(second(x),first(x)). 947 [] -member(x,Id)|equal(pair(first(x),first(x)),x). 948 [] -member(x,V)|member(pair(x,x),Id). 949 [] -equal(second(x),first(x))| -member(x,cart(V,V))|member(x,Id). 950 [] equal(inverse(Id),Id). 951 [] -subclass(x,Id)|equal(inverse(x),x). end_of_list. ------- end included file U:\ID\ID1-A.USE------- include("U:\ID\ID-CO.USE"). ------- start included file U:\ID\ID-CO.USE------- list(usable). 952 [] subclass(composite(Id,x),x). 953 [] subclass(composite(complement(x),inverse(x)),complement(Id)). 954 [] subclass(composite(inverse(x),complement(x)),complement(Id)). 955 [] subclass(composite(x,Id),x). 956 [] -subclass(image(x,singleton(first(notsub(composite(Id,x),y)))),image(y,singleton(first(notsub(composite(Id,x),y)))))|subclass(composite(Id,x),y). 957 [] -member(pair(x,y),z)| -member(pair(x,y),cart(V,V))|member(pair(x,y),composite(Id,z)). 958 [] -subclass(x,cart(V,V))|equal(composite(Id,x),x). 959 [] -FUNCTION(x)|equal(composite(Id,x),x). 960 [] equal(composite(Id,cart(x,y)),cart(x,y)). 961 [] equal(composite(Id,E),E). 962 [] equal(composite(Id,S),S). 963 [] -equal(cart(V,V),Id). 964 [] equal(restrict(x,V,V),composite(Id,x)). 965 [] equal(intersection(x,composite(Id,y)),composite(Id,intersection(x,y))). 966 [] equal(intersection(composite(Id,x),y),composite(Id,intersection(x,y))). 967 [] -subclass(V,image(x,singleton(first(notsub(cart(V,V),x)))))|subclass(cart(V,V),x). 968 [] equal(inverse(complement(x)),composite(Id,complement(inverse(x)))). 969 [] equal(inverse(inverse(x)),composite(Id,x)). 970 [] -FUNCTION(inverse(E)). 971 [] -FUNCTION(inverse(S)). 972 [] -subclass(x,cart(V,V))|equal(composite(x,Id),x). 973 [] equal(composite(cart(x,y),Id),cart(x,y)). 974 [] equal(composite(E,Id),E). 975 [] equal(composite(S,Id),S). 976 [] equal(composite(Id,Id),Id). 977 [] -subclass(x,Id)| -subclass(y,Id)|subclass(composite(x,y),Id). 978 [] equal(composite(x,Id),composite(Id,x)). 979 [] equal(complement(composite(Id,x)),union(complement(x),complement(cart(V,V)))). 980 [] equal(composite(Id,complement(cart(x,y))),union(cart(complement(x),V),cart(V,complement(y)))). 981 [] -subclass(x,cart(V,V))|equal(union(complement(cart(V,V)),composite(Id,complement(x))),complement(x)). 982 [] equal(composite(x,complement(cart(y,z))),union(cart(V,image(x,complement(z))),cart(complement(y),R(x)))). 983 [] equal(composite(complement(cart(x,y)),z),union(cart(D(z),complement(y)),cart(image(inverse(z),complement(x)),V))). 984 [] -subclass(composite(Id,x),y)|subclass(composite(Id,complement(y)),complement(x)). 985 [] equal(composite(Id,composite(x,y)),composite(x,y)). 986 [] equal(composite(x,composite(Id,y)),composite(x,y)). 987 [] equal(composite(x,composite(y,Id)),composite(x,y)). 988 [] -subclass(x,composite(y,x))| -subclass(composite(y,y),Id)|equal(composite(y,x),x). 989 [] -subclass(x,composite(x,y))| -subclass(composite(y,y),Id)|equal(composite(x,y),x). 990 [] equal(composite(complement(inverse(S)),complement(E)),cart(V,complement(singleton(0)))). 991 [] equal(composite(complement(inverse(S)),complement(S)),cart(complement(singleton(0)),complement(singleton(0)))). 992 [] equal(composite(Id,inverse(x)),inverse(x)). 993 [] equal(composite(inverse(x),Id),inverse(x)). 994 [] equal(composite(inverse(complement(E)),E),composite(Id,complement(Id))). 995 [] equal(composite(complement(inverse(E)),E),composite(Id,complement(Id))). 996 [] -subclass(Id,composite(x,y))| -subclass(composite(z,x),composite(u,v))| -subclass(composite(w,u),Id)|subclass(composite(w,z),composite(v,y)). end_of_list. ------- end included file U:\ID\ID-CO.USE------- include("U:\ID\ID2.USE"). ------- start included file U:\ID\ID2.USE------- list(usable). 997 [] -member(pair(x,y),z)| -member(pair(x,y),cart(V,V))|member(pair(x,x),composite(inverse(z),z)). 998 [] subclass(restrict(Id,D(x),V),composite(inverse(x),x)). 999 [] -member(x,D(y))| -subclass(y,Id)|member(pair(x,x),y). 1000 [] FUNCTION(Id). 1001 [] -subclass(x,Id)|FUNCTION(x). 1002 [] equal(D(Id),V). 1003 [] equal(D(composite(Id,x)),D(x)). 1004 [] equal(R(Id),V). 1005 [] -subclass(x,Id)|equal(R(x),D(x)). 1006 [] -subclass(E,Id). 1007 [] -subclass(x,Id)|subclass(x,restrict(Id,D(x),D(x))). 1008 [] -subclass(x,Id)|equal(restrict(Id,D(x),D(x)),x). 1009 [] -subclass(x,Id)| -subclass(y,Id)|equal(D(intersection(x,y)),intersection(D(x),D(y))). 1010 [] -subclass(x,Id)| -subclass(y,Id)| -subclass(D(x),D(y))|subclass(x,y). end_of_list. ------- end included file U:\ID\ID2.USE------- include("U:\FP\FP1-B.USE"). ------- start included file U:\FP\FP1-B.USE------- list(usable). 1011 [] equal(D(intersection(Id,x)),fix(x)). 1012 [] equal(R(intersection(Id,x)),fix(x)). 1013 [] -member(x,V)| -member(pair(x,x),y)|member(x,fix(y)). 1014 [] -member(x,fix(y))|member(pair(x,x),y). 1015 [] -member(x,x)| -member(x,complement(fix(E))). 1016 [] -member(x,V)|member(x,x)|member(x,complement(fix(E))). 1017 [] -member(complement(fix(E)),V). end_of_list. ------- end included file U:\FP\FP1-B.USE------- include("U:\ID\ID3-A.USE"). ------- start included file U:\ID\ID3-A.USE------- list(usable). 1018 [] -equal(D(x),D(y))| -subclass(x,Id)| -subclass(y,Id)|equal(x,y). 1019 [] equal(intersection(restrict(Id,x,V),restrict(Id,V,y)),restrict(Id,x,y)). 1020 [] equal(restrict(Id,x,V),restrict(Id,x,x)). 1021 [] equal(intersection(restrict(Id,x,x),restrict(Id,y,y)),restrict(Id,x,y)). 1022 [] equal(D(restrict(Id,x,y)),intersection(x,y)). 1023 [] equal(restrict(Id,intersection(x,y),intersection(x,y)),restrict(Id,x,y)). 1024 [] equal(R(restrict(Id,x,y)),intersection(x,y)). 1025 [] equal(image(Id,x),x). 1026 [] -member(pair(x,y),composite(Id,z))| -subclass(composite(u,z),v)|subclass(image(u,singleton(y)),image(v,singleton(x))). 1027 [] equal(D(complement(cart(x,y))),union(complement(x),image(V,complement(y)))). 1028 [] equal(R(complement(cart(x,y))),union(complement(y),image(V,complement(x)))). 1029 [] equal(A(complement(P(x))),complement(image(complement(Id),complement(x)))). 1030 [] equal(union(x,image(complement(Id),x)),image(V,x)). 1031 [] equal(x,0)|subclass(complement(x),image(complement(Id),x)). 1032 [] equal(x,0)|equal(singleton(U(x)),x)|equal(image(complement(Id),x),V). 1033 [] equal(R(complement(Id)),V). 1034 [] equal(D(complement(Id)),V). 1035 [] equal(inverse(image(V,x)),composite(Id,image(V,x))). 1036 [] equal(image(restrict(Id,x,x),y),intersection(x,y)). 1037 [] -subclass(x,Id)| -subclass(y,Id)|equal(D(composite(x,y)),intersection(D(x),D(y))). 1038 [] -subclass(x,Id)| -subclass(y,Id)|equal(composite(x,y),intersection(x,y)). 1039 [] ONEONE(Id). end_of_list. ------- end included file U:\ID\ID3-A.USE------- include("U:\ID\ID4.USE"). ------- start included file U:\ID\ID4.USE------- list(usable). 1040 [] -subclass(cart(x,y),Id)|equal(x,y)|equal(x,0)|equal(y,0). 1041 [] subclass(cart(singleton(x),singleton(x)),Id). 1042 [] -member(x,y)| -member(z,y)| -subclass(cart(y,y),Id)|equal(x,z). 1043 [] -subclass(cart(x,x),Id)|subclass(x,singleton(notsub(x,0))). 1044 [] -subclass(cart(x,x),Id)|equal(x,0)|equal(singleton(notsub(x,0)),x). 1045 [] -subclass(cart(x,x),Id)|equal(x,0)|equal(singleton(U(x)),x). 1046 [] -subclass(cart(x,x),Id)|equal(x,0)|equal(singleton(memb(x)),x). 1047 [] -subclass(cart(x,x),Id)|member(x,V). 1048 [] -subclass(cart(x,y),Id)|member(x,V)|member(y,V). 1049 [] -subclass(x,singleton(y))|subclass(cart(x,x),Id). 1050 [] -member(x,y)|subclass(cart(y,y),Id)|member(notsub(intersection(y,complement(singleton(x))),0),y). 1051 [] -equal(notsub(intersection(x,complement(singleton(y))),0),y)| -member(y,x)|subclass(cart(x,x),Id). 1052 [] subclass(intersection(x,Id),intersection(x,inverse(x))). 1053 [] subclass(cart(complement(U(x)),A(complement(x))),Id). end_of_list. ------- end included file U:\ID\ID4.USE------- include("U:\UB\UB1.USE"). ------- start included file U:\UB\UB1.USE------- list(usable). 1054 [] equal(composite(Id,complement(composite(complement(x),inverse(E)))),UB(x)). 1055 [] equal(UB(cart(x,y)),union(cart(singleton(0),V),cart(P(x),y))). 1056 [] -subclass(composite(x,E),y)|subclass(composite(Id,x),UB(y)). 1057 [] equal(UB(composite(Id,x)),UB(x)). 1058 [] subclass(UB(x),cart(V,V)). 1059 [] subclass(composite(x,UB(y)),UB(composite(x,y))). 1060 [] equal(UB(0),cart(singleton(0),V)). 1061 [] equal(UB(E),S). 1062 [] -member(pair(x,y),UB(z))|subclass(cart(x,singleton(y)),z). 1063 [] -member(pair(x,y),cart(V,V))| -subclass(cart(x,singleton(y)),z)|member(pair(x,y),UB(z)). 1064 [] subclass(cart(singleton(0),V),UB(x)). 1065 [] -member(pair(x,y),UB(z))| -member(pair(u,y),UB(z))|member(pair(union(x,u),y),UB(z)). 1066 [] -member(pair(x,y),composite(Id,z))|member(pair(singleton(x),y),UB(z)). 1067 [] equal(UB(intersection(x,y)),intersection(UB(x),UB(y))). 1068 [] equal(UB(restrict(x,y,V)),restrict(UB(x),P(y),V)). 1069 [] subclass(D(UB(x)),P(D(x))). 1070 [] equal(composite(UB(x),S),UB(x)). 1071 [] equal(composite(UB(x),E),composite(Id,x)). end_of_list. ------- end included file U:\UB\UB1.USE------- include("U:\LB\LB1.USE"). ------- start included file U:\LB\LB1.USE------- list(usable). 1072 [] equal(UB(inverse(x)),LB(x)). 1073 [] equal(LB(inverse(x)),UB(x)). 1074 [] disjoint(composite(complement(x),LB(x)),inverse(E)). 1075 [] equal(LB(composite(Id,x)),LB(x)). 1076 [] subclass(LB(x),cart(V,V)). 1077 [] equal(LB(0),cart(singleton(0),V)). 1078 [] subclass(composite(inverse(x),LB(y)),LB(composite(y,x))). 1079 [] -member(pair(x,y),LB(z))|subclass(cart(singleton(y),x),z). 1080 [] -member(pair(x,y),cart(V,V))| -subclass(cart(singleton(y),x),z)|member(pair(x,y),LB(z)). 1081 [] subclass(cart(singleton(0),V),LB(x)). 1082 [] -member(pair(x,y),inverse(z))|member(pair(singleton(x),y),LB(z)). 1083 [] subclass(D(LB(x)),P(R(x))). 1084 [] equal(LB(intersection(x,y)),intersection(LB(x),LB(y))). 1085 [] equal(composite(LB(x),S),LB(x)). 1086 [] equal(composite(LB(x),E),inverse(x)). end_of_list. ------- end included file U:\LB\LB1.USE------- include("U:\DI\DI.USE"). ------- start included file U:\DI\DI.USE------- list(usable). 1087 [] equal(intersection(cart(V,V),complement(Id)),Di). 1088 [] equal(composite(Id,complement(Id)),Di). 1089 [] subclass(Di,cart(V,V)). 1090 [] equal(composite(Id,Di),Di). 1091 [] equal(inverse(Di),Di). 1092 [] equal(complement(Di),union(Id,complement(cart(V,V)))). 1093 [] equal(union(composite(Id,complement(S)),composite(Id,complement(inverse(S)))),Di). 1094 [] equal(union(Di,complement(cart(V,V))),complement(Id)). 1095 [] -FUNCTION(x)|subclass(composite(inverse(x),composite(Di,x)),Di). 1096 [] subclass(cart(x,complement(image(Di,x))),Id). 1097 [] subclass(cart(x,complement(x)),Di). 1098 [] equal(intersection(Id,Di),0). 1099 [] -member(x,V)| -member(pair(x,x),Di). 1100 [] equal(union(Id,Di),cart(V,V)). 1101 [] -member(pair(x,y),cart(V,V))|equal(x,y)|member(pair(x,y),Di). 1102 [] -disjoint(x,y)|subclass(composite(x,inverse(y)),Di). 1103 [] -subclass(composite(x,y),Di)|disjoint(x,inverse(y)). 1104 [] subclass(PS,Di). 1105 [] equal(intersection(Di,S),PS). 1106 [] equal(intersection(Di,PS),PS). 1107 [] equal(intersection(E,complement(composite(E,Di))),SINGLETON). 1108 [] subclass(composite(complement(x),inverse(x)),Di). 1109 [] subclass(composite(inverse(x),complement(x)),Di). 1110 [] equal(composite(complement(inverse(E)),E),Di). 1111 [] equal(composite(inverse(E),complement(E)),Di). 1112 [] equal(A(complement(P(x))),complement(image(Di,complement(x)))). 1113 [] equal(union(x,image(Di,x)),image(V,x)). 1114 [] equal(x,0)|equal(singleton(U(x)),x)|equal(image(Di,x),V). 1115 [] equal(union(image(V,singleton(x)),image(Di,x)),V). 1116 [] equal(image(Di,x),V)|member(x,V). 1117 [] -member(x,V)|equal(image(Di,singleton(x)),complement(singleton(x))). 1118 [] subclass(x,image(Di,x))|disjoint(x,image(Di,x)). 1119 [] equal(image(Di,P(x)),union(complement(singleton(0)),image(V,x))). 1120 [] equal(composite(Di,complement(E)),cart(V,V)). 1121 [] equal(x,0)|subclass(complement(x),image(Di,x)). 1122 [] equal(R(Di),V). 1123 [] equal(D(Di),V). 1124 [] equal(image(V,Di),V). end_of_list. ------- end included file U:\DI\DI.USE------- include("U:\FP\FP2-B.USE"). ------- start included file U:\FP\FP2-B.USE------- list(usable). 1125 [] equal(fix(0),0). 1126 [] equal(fix(V),V). 1127 [] equal(fix(Id),V). 1128 [] equal(fix(Di),0). end_of_list. ------- end included file U:\FP\FP2-B.USE------- include("U:\FP\FP3.USE"). ------- start included file U:\FP\FP3.USE------- list(usable). 1129 [] subclass(fix(x),D(x)). 1130 [] subclass(fix(x),R(x)). 1131 [] equal(fix(union(x,y)),union(fix(x),fix(y))). 1132 [] -subclass(x,y)|subclass(fix(x),fix(y)). 1133 [] equal(fix(complement(x)),complement(fix(x))). 1134 [] equal(fix(intersection(x,y)),intersection(fix(x),fix(y))). end_of_list. ------- end included file U:\FP\FP3.USE------- include("U:\FP\FP4.USE"). ------- start included file U:\FP\FP4.USE------- list(usable). 1135 [] equal(fix(inverse(x)),fix(x)). 1136 [] equal(fix(composite(Id,x)),fix(x)). 1137 [] equal(fix(cart(x,y)),intersection(x,y)). 1138 [] equal(fix(restrict(x,y,z)),intersection(fix(x),intersection(y,z))). end_of_list. ------- end included file U:\FP\FP4.USE------- include("U:\DJT\DJT-D.USE"). ------- start included file U:\DJT\DJT-D.USE------- list(usable). 1139 [] equal(composite(E,inverse(E)),composite(Id,complement(DISJOINT))). 1140 [] subclass(DISJOINT,cart(V,V)). 1141 [] equal(composite(Id,DISJOINT),DISJOINT). 1142 [] equal(union(complement(cart(V,V)),composite(Id,complement(DISJOINT))),complement(DISJOINT)). 1143 [] equal(inverse(DISJOINT),DISJOINT). 1144 [] -member(pair(x,y),DISJOINT)|disjoint(x,y). 1145 [] -member(x,DISJOINT)|disjoint(first(x),second(x)). 1146 [] -member(pair(x,y),cart(V,V))| -disjoint(x,y)|member(pair(x,y),DISJOINT). 1147 [] equal(intersection(S,DISJOINT),cart(singleton(0),V)). 1148 [] equal(composite(DISJOINT,S),DISJOINT). 1149 [] equal(composite(inverse(S),DISJOINT),DISJOINT). 1150 [] equal(composite(DISJOINT,E),composite(Id,complement(E))). 1151 [] equal(composite(inverse(E),DISJOINT),composite(Id,complement(inverse(E)))). 1152 [] equal(U(image(DISJOINT,x)),complement(A(x))). 1153 [] equal(D(DISJOINT),V). 1154 [] equal(R(DISJOINT),V). 1155 [] equal(image(DISJOINT,singleton(x)),intersection(image(V,singleton(x)),P(complement(x)))). 1156 [] -member(0,x)|equal(image(DISJOINT,x),V). 1157 [] equal(image(DISJOINT,P(x)),V). 1158 [] equal(A(image(DISJOINT,x)),complement(image(V,x))). 1159 [] equal(composite(S,DISJOINT),cart(V,V)). 1160 [] equal(composite(DISJOINT,complement(E)),cart(V,V)). 1161 [] equal(composite(DISJOINT,complement(S)),cart(complement(singleton(0)),V)). 1162 [] equal(composite(DISJOINT,DISJOINT),cart(V,V)). 1163 [] subclass(cart(singleton(0),V),DISJOINT). end_of_list. ------- end included file U:\DJT\DJT-D.USE------- include("U:\SV\SV-REF.USE"). ------- start included file U:\SV\SV-REF.USE------- list(usable). 1164 [] -subclass(composite(x,inverse(x)),Id)|disjoint(x,composite(Di,x)). 1165 [] -disjoint(x,composite(Di,x))|subclass(composite(x,inverse(x)),Id). 1166 [] -subclass(cart(V,V),Id). 1167 [] -member(pair(x,y),z)| -member(pair(x,y),cart(V,V))| -member(pair(x,u),z)| -member(pair(x,u),cart(V,V))| -subclass(composite(z,inverse(z)),Id)|equal(y,u). 1168 [] equal(first(notsub(composite(x,inverse(x)),Id)),sv1(x)). 1169 [] equal(second(notsub(composite(x,inverse(x)),Id)),sv2(x)). 1170 [] equal(dom(x,image(inverse(x),singleton(sv1(x))),sv2(x)),sv3(x)). 1171 [] member(sv1(x),V)|subclass(composite(x,inverse(x)),Id). 1172 [] member(sv2(x),V)|subclass(composite(x,inverse(x)),Id). 1173 [] equal(notsub(composite(x,inverse(x)),Id),pair(sv1(x),sv2(x)))|subclass(composite(x,inverse(x)),Id). 1174 [] -equal(sv2(x),sv1(x))|subclass(composite(x,inverse(x)),Id). 1175 [] member(pair(sv3(x),sv1(x)),x)|subclass(composite(x,inverse(x)),Id). 1176 [] member(pair(sv3(x),sv2(x)),x)|subclass(composite(x,inverse(x)),Id). 1177 [] member(sv3(x),V)|subclass(composite(x,inverse(x)),Id). 1178 [] member(pair(sv3(composite(x,y)),sv1(composite(x,y))),composite(x,y))|FUNCTION(composite(x,y)). 1179 [] member(pair(sv3(composite(x,y)),sv2(composite(x,y))),composite(x,y))|FUNCTION(composite(x,y)). 1180 [] -equal(sv2(composite(x,y)),sv1(composite(x,y)))|FUNCTION(composite(x,y)). 1181 [] -subclass(x,y)| -subclass(composite(y,inverse(y)),Id)|subclass(composite(x,inverse(x)),Id). 1182 [] -subclass(composite(x,inverse(x)),Id)|subclass(composite(intersection(x,y),inverse(intersection(x,y))),Id). 1183 [] -member(pair(x,y),z)| -member(pair(x,y),cart(V,V))| -subclass(composite(z,inverse(z)),Id)|equal(image(z,singleton(x)),singleton(y)). 1184 [] -subclass(composite(x,inverse(x)),Id)|subclass(composite(composite(y,x),inverse(x)),y). 1185 [] -subclass(composite(x,inverse(x)),Id)| -subclass(composite(y,inverse(y)),Id)|subclass(composite(x,composite(y,composite(inverse(y),inverse(x)))),Id). 1186 [] -subclass(composite(x,inverse(x)),Id)|subclass(composite(complement(y),x),complement(composite(y,x))). 1187 [] -subclass(x,composite(y,z))| -subclass(composite(z,inverse(z)),Id)|subclass(composite(x,inverse(z)),y). end_of_list. ------- end included file U:\SV\SV-REF.USE------- include("U:\FU\FU1-REF.USE"). ------- start included file U:\FU\FU1-REF.USE------- list(usable). 1188 [] -FUNCTION(x)|disjoint(x,composite(Di,x)). 1189 [] -subclass(x,cart(V,V))| -disjoint(x,composite(Di,x))|FUNCTION(x). 1190 [] -FUNCTION(x)| -member(y,x)|member(y,cart(V,V)). 1191 [] -FUNCTION(x)| -subclass(y,composite(z,x))|subclass(composite(y,inverse(x)),z). 1192 [] -FUNCTION(x)|equal(composite(x,intersection(composite(inverse(x),y),z)),intersection(y,composite(x,z))). 1193 [] -FUNCTION(composite(Id,x))|subclass(composite(x,inverse(x)),Id). 1194 [] -subclass(composite(x,inverse(x)),Id)|FUNCTION(composite(Id,x)). 1195 [] -FUNCTION(x)| -member(pair(y,z),x)| -member(pair(y,u),x)|equal(z,u). 1196 [] -FUNCTION(x)|FUNCTION(composite(Id,intersection(y,complement(composite(Di,intersection(y,complement(x))))))). 1197 [] -FUNCTION(x)| -equal(first(y),first(z))| -member(pair(y,z),cart(x,x))|equal(second(y),second(z)). 1198 [] -FUNCTION(x)| -equal(first(y),first(z))| -member(pair(y,z),cart(x,x))|equal(y,z). 1199 [] -FUNCTION(x)| -subclass(y,x)|FUNCTION(y). 1200 [] -FUNCTION(x)|FUNCTION(restrict(x,y,z)). 1201 [] -FUNCTION(x)|FUNCTION(intersection(x,y)). 1202 [] -FUNCTION(x)| -FUNCTION(y)|FUNCTION(composite(x,y)). 1203 [] -FUNCTION(x)|equal(restrict(x,V,V),x). 1204 [] -subclass(composite(inverse(x),x),Id)|FUNCTION(inverse(x)). 1205 [] -FUNCTION(x)| -equal(D(y),V)| -subclass(composite(y,z),composite(u,x))|subclass(composite(x,inverse(z)),composite(inverse(u),y)). 1206 [] -FUNCTION(x)|subclass(x,composite(Id,complement(composite(Di,x)))). 1207 [] -subclass(x,composite(Id,complement(composite(Di,x))))|FUNCTION(x). 1208 [] equal(intersection(composite(Id,x),complement(composite(Di,x))),funpart(x)). 1209 [] subclass(funpart(x),x). 1210 [] subclass(composite(funpart(x),inverse(x)),Id). 1211 [] equal(inverse(funpart(inverse(E))),SINGLETON). 1212 [] -equal(funpart(x),x)|FUNCTION(x). 1213 [] -FUNCTION(x)|equal(funpart(x),x). 1214 [] subclass(funpart(x),cart(V,V)). 1215 [] equal(composite(Id,funpart(x)),funpart(x)). 1216 [] -member(pair(x,y),funpart(z))| -member(pair(x,u),composite(Id,z))|equal(y,u). 1217 [] FUNCTION(funpart(x)). 1218 [] equal(funpart(funpart(x)),funpart(x)). end_of_list. ------- end included file U:\FU\FU1-REF.USE------- include("U:\FU\FU2-A.USE"). ------- start included file U:\FU\FU2-A.USE------- list(usable). 1219 [] FUNCTION(0). 1220 [] FUNCTION(cart(x,singleton(y))). 1221 [] -member(x,cart(V,V))|FUNCTION(singleton(x)). 1222 [] -FUNCTION(pairset(x,y))| -member(x,V)|member(x,cart(V,V)). 1223 [] -FUNCTION(pairset(x,y))| -member(y,V)|member(y,cart(V,V)). 1224 [] -FUNCTION(pairset(pair(x,y),pair(x,z)))|equal(y,z). 1225 [] equal(pairset(pair(x,y),pair(y,x)),transposition(x,y)). 1226 [] -member(pair(x,y),cart(V,V))|subclass(transposition(x,y),cart(V,V)). 1227 [] equal(transposition(x,y),transposition(y,x)). 1228 [] -FUNCTION(x)| -subclass(D(x),D(intersection(x,y)))|subclass(x,y). 1229 [] -FUNCTION(x)| -subclass(y,x)| -subclass(D(x),D(y))|equal(x,y). 1230 [] -FUNCTION(x)| -subclass(y,x)|equal(intersection(x,cart(D(y),V)),y). 1231 [] -FUNCTION(x)| -FUNCTION(y)| -equal(intersection(D(x),D(y)),0)|FUNCTION(union(x,y)). 1232 [] -FUNCTION(x)| -member(y,cart(V,V))|FUNCTION(union(x,singleton(y)))|member(first(y),D(x)). 1233 [] -member(pair(x,y),cart(V,V))| -member(pair(z,u),cart(V,V))|FUNCTION(pairset(pair(x,y),pair(z,u)))|equal(x,z). 1234 [] -member(pair(x,y),cart(V,V))|FUNCTION(transposition(x,y)). 1235 [] -member(pair(x,y),cart(V,V))|equal(inverse(transposition(x,y)),transposition(x,y)). end_of_list. ------- end included file U:\FU\FU2-A.USE------- include("U:\OO\OO.USE"). ------- start included file U:\OO\OO.USE------- list(usable). 1236 [] member(sv1(inverse(x)),V)|subclass(composite(inverse(x),x),Id). 1237 [] member(sv2(inverse(x)),V)|subclass(composite(inverse(x),x),Id). 1238 [] member(sv3(inverse(x)),V)|subclass(composite(inverse(x),x),Id). 1239 [] member(pair(sv1(inverse(x)),sv3(inverse(x))),x)|subclass(composite(inverse(x),x),Id). 1240 [] member(pair(sv2(inverse(x)),sv3(inverse(x))),x)|subclass(composite(inverse(x),x),Id). 1241 [] -equal(sv2(inverse(x)),sv1(inverse(x)))|subclass(composite(inverse(x),x),Id). 1242 [] ONEONE(0). 1243 [] -ONEONE(x)|ONEONE(inverse(x)). 1244 [] -ONEONE(x)| -subclass(y,x)|ONEONE(y). 1245 [] -ONEONE(x)| -ONEONE(y)|ONEONE(composite(x,y)). 1246 [] -ONEONE(x)| -ONEONE(y)| -disjoint(D(x),D(y))| -disjoint(R(x),R(y))|ONEONE(union(x,y)). end_of_list. ------- end included file U:\OO\OO.USE------- include("U:\IDX\IDX1.USE"). ------- start included file U:\IDX\IDX1.USE------- list(usable). 1247 [] equal(restrict(Id,x,x),id(x)). 1248 [] equal(intersection(Id,cart(x,x)),id(x)). 1249 [] subclass(id(x),cart(V,V)). 1250 [] subclass(id(x),cart(x,x)). 1251 [] equal(composite(Id,id(x)),id(x)). 1252 [] -member(pair(x,y),id(z))|member(x,z). 1253 [] -member(pair(x,y),id(z))|member(y,z). 1254 [] subclass(id(x),Id). 1255 [] subclass(composite(x,id(y)),x). 1256 [] subclass(composite(id(x),y),y). 1257 [] equal(intersection(Di,id(x)),0). 1258 [] -member(pair(x,y),id(z))|equal(x,y). 1259 [] equal(id(V),Id). 1260 [] equal(id(0),0). 1261 [] equal(inverse(id(x)),id(x)). 1262 [] -member(x,y)|member(pair(x,x),id(y)). 1263 [] -member(x,V)|equal(singleton(pair(x,x)),id(singleton(x))). 1264 [] equal(singleton(pair(0,0)),id(singleton(0))). 1265 [] -member(x,id(y))|equal(second(x),first(x)). 1266 [] -member(x,id(y))|member(first(x),y). 1267 [] FUNCTION(id(x)). 1268 [] ONEONE(id(x)). end_of_list. ------- end included file U:\IDX\IDX1.USE------- include("U:\IDX\IDX2-A.USE"). ------- start included file U:\IDX\IDX2-A.USE------- list(usable). 1269 [] equal(intersection(id(x),id(y)),id(intersection(x,y))). 1270 [] equal(composite(id(x),id(y)),id(intersection(x,y))). 1271 [] -subclass(x,Id)|equal(id(D(x)),x). 1272 [] -subclass(x,y)|subclass(id(x),id(y)). 1273 [] equal(intersection(Id,x),id(fix(x))). 1274 [] equal(intersection(Id,cart(x,y)),id(intersection(x,y))). 1275 [] -subclass(intersection(x,inverse(x)),Id)|equal(intersection(x,inverse(x)),id(fix(x))). 1276 [] -subclass(x,Id)|equal(D(x),fix(x)). 1277 [] equal(fix(id(x)),x). 1278 [] -subclass(id(x),y)|subclass(x,fix(y)). 1279 [] -subclass(x,fix(y))|subclass(id(x),y). 1280 [] equal(D(id(x)),x). 1281 [] equal(R(id(x)),x). 1282 [] -member(pair(x,y),composite(z,id(u)))|member(x,u). 1283 [] -member(pair(x,y),composite(id(z),u))|member(y,z). 1284 [] equal(cart(singleton(x),singleton(x)),id(singleton(x))). 1285 [] equal(composite(x,id(singleton(y))),cart(singleton(y),image(x,singleton(y)))). 1286 [] equal(composite(id(singleton(x)),y),cart(image(inverse(y),singleton(x)),singleton(x))). 1287 [] equal(image(id(x),y),intersection(x,y)). 1288 [] -subclass(composite(x,id(y)),composite(id(z),x))|subclass(image(x,y),z). 1289 [] -subclass(image(x,y),z)|subclass(composite(x,id(y)),composite(id(z),x)). 1290 [] -subclass(U(x),x)|subclass(composite(inverse(E),id(x)),composite(id(x),inverse(E))). 1291 [] -subclass(composite(id(x),y),composite(y,id(z)))|subclass(image(inverse(y),x),z). 1292 [] -subclass(image(inverse(x),y),z)|subclass(composite(id(y),x),composite(x,id(z))). 1293 [] equal(restrict(Id,x,y),id(intersection(x,y))). 1294 [] equal(composite(x,id(y)),restrict(x,y,V)). 1295 [] equal(D(composite(x,id(y))),intersection(D(x),y)). 1296 [] equal(composite(id(x),y),restrict(y,V,x)). 1297 [] equal(intersection(x,composite(y,id(z))),composite(intersection(x,y),id(z))). 1298 [] equal(intersection(x,composite(id(y),z)),composite(id(y),intersection(x,z))). 1299 [] equal(composite(x,id(complement(D(x)))),0). 1300 [] equal(composite(id(complement(R(x))),x),0). 1301 [] -FUNCTION(x)| -subclass(y,x)|equal(composite(x,id(D(y))),y). 1302 [] -FUNCTION(x)|equal(composite(id(y),x),composite(x,id(image(inverse(x),y)))). 1303 [] equal(union(id(x),id(y)),id(union(x,y))). end_of_list. ------- end included file U:\IDX\IDX2-A.USE------- include("U:\FP\FP5.USE"). ------- start included file U:\FP\FP5.USE------- list(usable). 1304 [] equal(fix(composite(inverse(x),y)),D(intersection(x,y))). 1305 [] equal(fix(composite(x,y)),D(intersection(inverse(x),y))). 1306 [] equal(fix(composite(intersection(x,inverse(y)),z)),fix(composite(x,intersection(y,z)))). 1307 [] equal(fix(composite(x,intersection(inverse(y),z))),fix(composite(intersection(x,y),z))). 1308 [] equal(fix(composite(x,inverse(y))),R(intersection(x,y))). 1309 [] equal(fix(composite(x,y)),R(intersection(x,inverse(y)))). 1310 [] equal(fix(composite(x,composite(y,id(z)))),intersection(z,fix(composite(x,y)))). end_of_list. ------- end included file U:\FP\FP5.USE------- include("U:\FP\FP6.USE"). ------- start included file U:\FP\FP6.USE------- list(usable). 1311 [] subclass(intersection(fix(x),fix(y)),fix(composite(x,y))). 1312 [] subclass(fix(x),fix(composite(x,x))). 1313 [] subclass(fix(composite(x,y)),intersection(R(x),D(y))). 1314 [] -equal(fix(composite(x,y)),0)|equal(fix(composite(y,x)),0). end_of_list. ------- end included file U:\FP\FP6.USE------- include("U:\FP\FP-SR.USE"). ------- start included file U:\FP\FP-SR.USE------- list(usable). 1315 [] equal(fix(S),V). 1316 [] subclass(fix(x),fix(composite(S,x))). 1317 [] subclass(fix(x),fix(composite(x,S))). 1318 [] subclass(fix(x),D(intersection(S,x))). 1319 [] subclass(fix(x),R(intersection(S,x))). end_of_list. ------- end included file U:\FP\FP-SR.USE------- include("U:\FP\FP-DJ.USE"). ------- start included file U:\FP\FP-DJ.USE------- list(usable). 1320 [] equal(fix(DISJOINT),singleton(0)). 1321 [] -subclass(inverse(x),complement(y))|equal(fix(composite(x,y)),0). 1322 [] -equal(fix(composite(x,y)),0)|subclass(inverse(x),complement(y)). 1323 [] -equal(fix(composite(x,y)),0)|disjoint(x,inverse(y)). 1324 [] -disjoint(x,inverse(y))|equal(fix(composite(x,y)),0). end_of_list. ------- end included file U:\FP\FP-DJ.USE------- include("U:\FP\FP-IM.USE"). ------- start included file U:\FP\FP-IM.USE------- list(usable). 1325 [] equal(fix(image(V,x)),image(V,x)). 1326 [] equal(intersection(Id,image(V,x)),id(image(V,x))). 1327 [] -member(x,fix(composite(complement(composite(E,inverse(y))),composite(z,inverse(E)))))| -subclass(image(z,x),image(y,x)). 1328 [] -member(x,fix(complement(composite(complement(composite(E,y)),composite(z,inverse(E))))))|subclass(image(z,x),image(inverse(y),x)). 1329 [] subclass(image(x,U(fix(complement(composite(complement(composite(E,y)),composite(x,inverse(E))))))),image(inverse(y),U(fix(complement(composite(complement(composite(E,y)),composite(x,inverse(E)))))))). 1330 [] -member(x,fix(composite(complement(composite(E,y)),composite(z,inverse(E)))))| -subclass(image(z,x),image(inverse(y),x)). end_of_list. ------- end included file U:\FP\FP-IM.USE------- include("U:\FP\FP-UB.USE"). ------- start included file U:\FP\FP-UB.USE------- list(usable). 1331 [] -member(x,V)|member(x,fix(composite(E,composite(inverse(y),UB(complement(z))))))|subclass(image(y,x),image(z,x)). 1332 [] -member(x,V)|member(x,fix(composite(E,composite(y,UB(z)))))|subclass(image(inverse(y),x),image(complement(z),x)). 1333 [] -member(x,fix(composite(E,composite(y,UB(z)))))| -subclass(image(inverse(y),x),image(complement(z),x)). 1334 [] -member(x,fix(composite(E,composite(inverse(y),UB(complement(z))))))| -subclass(image(y,x),image(z,x)). end_of_list. ------- end included file U:\FP\FP-UB.USE------- include("U:\IDX\IDX3-A.USE"). ------- start included file U:\IDX\IDX3-A.USE------- list(usable). 1335 [] subclass(id(D(x)),composite(inverse(x),x)). 1336 [] -subclass(x,inverse(y))|subclass(id(D(x)),composite(y,x)). 1337 [] subclass(intersection(D(x),y),image(inverse(x),image(x,y))). 1338 [] subclass(id(R(x)),composite(x,inverse(x))). 1339 [] subclass(intersection(R(x),y),image(x,image(inverse(x),y))). 1340 [] equal(composite(id(R(x)),x),composite(Id,x)). 1341 [] -subclass(R(x),y)|equal(composite(id(y),x),composite(Id,x)). 1342 [] equal(composite(x,id(D(x))),composite(x,Id)). 1343 [] -subclass(D(x),y)|equal(composite(x,id(y)),composite(Id,x)). 1344 [] -equal(D(x),R(y))| -subclass(composite(x,y),Id)|equal(composite(Id,x),inverse(y)). end_of_list. ------- end included file U:\IDX\IDX3-A.USE------- include("U:\ST\ST1.USE"). ------- start included file U:\ST\ST1.USE------- list(usable). 1345 [] -subcommute(x,y)|subclass(composite(x,y),composite(y,x)). 1346 [] -subclass(composite(x,y),composite(y,x))|subcommute(x,y). 1347 [] subcommute(x,0). 1348 [] subcommute(0,x). 1349 [] subcommute(x,Id). 1350 [] subcommute(Id,x). 1351 [] -subcommute(composite(Id,x),y)|subcommute(x,y). 1352 [] -subcommute(x,composite(Id,y))|subcommute(x,y). 1353 [] -subcommute(x,y)|subcommute(inverse(y),inverse(x)). 1354 [] -subcommute(x,y)| -subcommute(x,z)|subcommute(x,composite(y,z)). 1355 [] -subcommute(x,y)| -subcommute(z,y)|subcommute(composite(x,z),y). 1356 [] -subcommute(x,y)| -subcommute(x,z)|subcommute(x,union(y,z)). 1357 [] -subcommute(x,y)| -subcommute(z,y)|subcommute(union(x,z),y). 1358 [] -subcommute(x,y)|subclass(image(x,R(y)),R(y)). 1359 [] -subcommute(x,y)|subclass(image(inverse(y),D(x)),D(x)). 1360 [] -subcommute(x,id(y))|subclass(image(x,y),y). 1361 [] -subclass(image(x,y),y)|subcommute(x,id(y)). 1362 [] -subcommute(id(x),y)|subclass(image(inverse(y),x),x). 1363 [] -subclass(image(inverse(x),y),y)|subcommute(id(y),x). 1364 [] subcommute(S,E). 1365 [] -FUNCTION(x)| -subcommute(x,y)| -equal(D(x),V)|subcommute(x,inverse(y)). end_of_list. ------- end included file U:\ST\ST1.USE------- include("U:\FU\FU3-REF.USE"). ------- start included file U:\FU\FU3-REF.USE------- list(usable). 1366 [] -subclass(R(x),D(y))| -subclass(composite(y,x),Id)|FUNCTION(inverse(x)). 1367 [] -FUNCTION(x)| -subclass(y,inverse(x))|equal(composite(x,y),id(D(y))). 1368 [] equal(composite(x,id(D(funpart(x)))),funpart(x)). 1369 [] -equal(D(funpart(x)),D(x))|FUNCTION(composite(Id,x)). 1370 [] -FUNCTION(inverse(x))|equal(image(x,intersection(y,z)),intersection(image(x,y),image(x,z))). 1371 [] -FUNCTION(x)|disjoint(image(inverse(x),complement(y)),image(inverse(x),y)). 1372 [] -FUNCTION(inverse(x))|equal(image(x,complement(y)),intersection(R(x),complement(image(x,y)))). 1373 [] -FUNCTION(composite(Id,x))|equal(composite(x,inverse(x)),id(R(x))). 1374 [] -FUNCTION(x)|equal(composite(x,inverse(x)),id(R(x))). 1375 [] -ONEONE(x)|equal(composite(inverse(x),x),id(D(x))). 1376 [] -FUNCTION(x)| -equal(composite(x,x),x)|equal(composite(x,id(R(x))),id(R(x))). 1377 [] -FUNCTION(composite(Id,x))|equal(image(x,image(inverse(x),y)),intersection(R(x),y)). 1378 [] -FUNCTION(composite(Id,x))| -subclass(y,image(x,z))|equal(image(x,intersection(z,image(inverse(x),y))),y). 1379 [] -FUNCTION(x)| -subclass(y,image(inverse(x),z))|subclass(image(x,y),z). 1380 [] -FUNCTION(x)| -subclass(y,R(x))| -subclass(image(inverse(x),y),image(inverse(x),z))|subclass(y,z). 1381 [] -FUNCTION(x)|equal(image(x,image(inverse(x),y)),intersection(R(x),y)). 1382 [] -FUNCTION(x)| -equal(image(inverse(x),y),image(inverse(x),z))| -subclass(union(y,z),R(x))|equal(y,z). end_of_list. ------- end included file U:\FU\FU3-REF.USE------- include("U:\SG\SG1-A.USE"). ------- start included file U:\SG\SG1-A.USE------- list(usable). 1383 [] equal(intersection(E,complement(composite(E,complement(Id)))),SINGLETON). 1384 [] subclass(SINGLETON,E). 1385 [] subclass(SINGLETON,cart(V,V)). 1386 [] equal(restrict(SINGLETON,V,V),SINGLETON). 1387 [] equal(union(complement(cart(V,V)),composite(Id,complement(SINGLETON))),complement(SINGLETON)). 1388 [] -member(pair(x,y),SINGLETON)|member(x,y). 1389 [] -member(pair(x,y),cart(V,V))|subclass(y,singleton(x))|member(pair(x,y),composite(E,complement(Id))). 1390 [] -member(pair(x,y),composite(E,complement(Id)))| -subclass(y,singleton(x)). 1391 [] -member(pair(x,y),SINGLETON)|equal(singleton(x),y). 1392 [] FUNCTION(SINGLETON). 1393 [] equal(composite(SINGLETON,inverse(SINGLETON)),id(R(SINGLETON))). 1394 [] ONEONE(SINGLETON). 1395 [] -member(x,V)|member(pair(x,singleton(x)),SINGLETON). 1396 [] -member(x,y)|member(singleton(x),image(SINGLETON,y)). 1397 [] equal(composite(S,SINGLETON),E). 1398 [] equal(composite(Id,complement(E)),composite(DISJOINT,SINGLETON)). 1399 [] subclass(composite(SINGLETON,Di),composite(Di,SINGLETON)). 1400 [] equal(composite(inverse(E),SINGLETON),Id). 1401 [] equal(U(image(SINGLETON,x)),x). 1402 [] -equal(image(SINGLETON,x),singleton(x))|member(x,R(SINGLETON)). 1403 [] equal(composite(inverse(SINGLETON),E),Id). 1404 [] subclass(composite(x,inverse(SINGLETON)),UB(x)). 1405 [] -subclass(composite(x,inverse(E)),composite(y,inverse(E)))|subclass(composite(Id,x),composite(Id,y)). 1406 [] -equal(composite(x,inverse(E)),composite(y,inverse(E)))|equal(composite(Id,x),composite(Id,y)). 1407 [] -subclass(composite(E,x),composite(E,y))|subclass(composite(Id,x),composite(Id,y)). 1408 [] -equal(composite(E,x),composite(E,y))|equal(composite(Id,x),composite(Id,y)). end_of_list. ------- end included file U:\SG\SG1-A.USE------- include("U:\SG\SG2-REF.USE"). ------- start included file U:\SG\SG2-REF.USE------- list(usable). 1409 [] equal(D(SINGLETON),V). 1410 [] -subclass(R(SINGLETON),x)|equal(U(intersection(x,R(SINGLETON))),V). 1411 [] -equal(U(intersection(x,R(SINGLETON))),V)|subclass(R(SINGLETON),x). 1412 [] equal(composite(inverse(SINGLETON),SINGLETON),Id). 1413 [] -member(image(SINGLETON,x),V)|member(x,V). 1414 [] -member(intersection(P(x),R(SINGLETON)),V)|member(x,V). 1415 [] -member(0,R(SINGLETON)). 1416 [] -member(x,V)|member(singleton(x),R(SINGLETON)). 1417 [] -FUNCTION(composite(Id,x))| -member(y,D(x))|member(image(x,singleton(y)),R(SINGLETON)). 1418 [] -member(x,D(funpart(y)))|member(image(y,singleton(x)),R(SINGLETON)). 1419 [] -member(x,R(SINGLETON))|equal(singleton(U(x)),x). 1420 [] -member(x,R(SINGLETON))|member(U(x),x). 1421 [] -member(x,y)| -member(y,R(SINGLETON))|equal(singleton(x),y). 1422 [] -member(x,R(SINGLETON))|subclass(x,y)|disjoint(x,y). 1423 [] -member(pair(x,y),funpart(z))|equal(image(z,singleton(x)),singleton(y)). 1424 [] -equal(singleton(U(x)),x)|member(x,R(SINGLETON)). 1425 [] -member(x,V)|member(x,image(Di,y))|subclass(y,singleton(x)). 1426 [] subclass(R(SINGLETON),union(P(x),P(complement(x)))). 1427 [] -member(x,U(intersection(y,R(SINGLETON))))|member(singleton(x),y). 1428 [] -member(x,V)| -member(singleton(x),y)|member(x,U(intersection(y,R(SINGLETON)))). 1429 [] equal(image(inverse(SINGLETON),x),U(intersection(x,R(SINGLETON)))). 1430 [] equal(composite(id(x),SINGLETON),composite(SINGLETON,id(U(intersection(x,R(SINGLETON)))))). 1431 [] -member(x,image(SINGLETON,y))|equal(singleton(U(x)),x). 1432 [] -member(x,image(SINGLETON,y))|member(U(x),y). 1433 [] -member(x,intersection(P(y),R(SINGLETON)))|member(U(x),y). 1434 [] -equal(singleton(U(x)),x)| -member(U(x),y)|member(x,image(SINGLETON,y)). 1435 [] -equal(singleton(U(x)),x)| -member(U(x),y)|member(x,intersection(P(y),R(SINGLETON))). 1436 [] subclass(image(SINGLETON,x),P(x)). 1437 [] equal(intersection(P(x),R(SINGLETON)),image(SINGLETON,x)). 1438 [] equal(intersection(image(SINGLETON,x),P(y)),image(SINGLETON,intersection(x,y))). 1439 [] equal(intersection(image(SINGLETON,x),image(SINGLETON,y)),image(SINGLETON,intersection(x,y))). 1440 [] equal(U(intersection(x,image(SINGLETON,y))),intersection(y,U(intersection(x,R(SINGLETON))))). 1441 [] equal(U(intersection(x,intersection(P(y),R(SINGLETON)))),intersection(y,U(intersection(x,R(SINGLETON))))). 1442 [] subclass(image(SINGLETON,x),complement(P(complement(x)))). 1443 [] equal(intersection(R(SINGLETON),complement(P(complement(x)))),image(SINGLETON,x)). 1444 [] equal(intersection(complement(P(x)),R(SINGLETON)),image(SINGLETON,complement(x))). 1445 [] equal(intersection(image(SINGLETON,x),complement(P(y))),image(SINGLETON,intersection(x,complement(y)))). 1446 [] equal(intersection(image(SINGLETON,x),complement(image(SINGLETON,y))),image(SINGLETON,intersection(x,complement(y)))). 1447 [] equal(x,0)|equal(image(complement(Id),x),V)|member(x,R(SINGLETON)). 1448 [] equal(image(inverse(S),R(SINGLETON)),union(singleton(0),R(SINGLETON))). 1449 [] -member(x,R(SINGLETON))|equal(memb(x),U(x)). 1450 [] equal(U(R(SINGLETON)),V). 1451 [] -subclass(R(SINGLETON),P(x))|equal(x,V). 1452 [] -member(x,R(SINGLETON))|equal(image(complement(Id),x),complement(x)). 1453 [] -member(x,V)|equal(image(complement(Id),singleton(x)),complement(singleton(x))). 1454 [] equal(A(R(SINGLETON)),0). end_of_list. ------- end included file U:\SG\SG2-REF.USE------- include("U:\FP\FP-FU.USE"). ------- start included file U:\FP\FP-FU.USE------- list(usable). 1455 [] equal(fix(composite(complement(composite(inverse(x),Di)),x)),D(funpart(x))). 1456 [] -FUNCTION(x)|equal(composite(x,id(D(intersection(x,y)))),intersection(x,y)). 1457 [] equal(composite(SINGLETON,id(D(intersection(SINGLETON,x)))),intersection(SINGLETON,x)). 1458 [] -FUNCTION(x)|equal(composite(x,id(fix(x))),id(fix(x))). 1459 [] -FUNCTION(x)|equal(image(x,fix(x)),fix(x)). 1460 [] -FUNCTION(x)| -subclass(y,fix(x))|equal(image(x,y),y). 1461 [] -FUNCTION(x)| -equal(D(intersection(x,complement(y))),0)|subclass(x,y). 1462 [] -FUNCTION(x)| -subclass(x,composite(y,x))|subclass(R(x),fix(y)). end_of_list. ------- end included file U:\FP\FP-FU.USE------- include("U:\RP\RP1.USE"). ------- start included file U:\RP\RP1.USE------- list(usable). 1463 [] -member(x,V)|member(intersection(y,x),V). 1464 [] -member(x,V)| -subclass(y,x)|member(y,V). 1465 [] -member(x,P(union(y,z)))|member(intersection(complement(z),x),P(y)). 1466 [] -member(x,P(union(y,z)))|member(intersection(complement(y),x),P(z)). 1467 [] -member(intersection(x,y),V)| -member(complement(x),V)|member(y,V). 1468 [] -member(intersection(complement(singleton(x)),y),V)|member(y,V). 1469 [] -member(x,V)|member(restrict(x,y,z),V). 1470 [] -member(image(inverse(S),x),V)|member(x,V). 1471 [] -member(x,V)| -subclass(y,x)|member(pair(y,x),S). 1472 [] -member(x,y)| -subclass(z,x)|member(z,image(inverse(S),y)). 1473 [] -member(x,V)| -subclass(y,x)|member(x,image(S,singleton(y))). 1474 [] -subclass(x,y)|subclass(image(S,singleton(y)),image(S,singleton(x))). 1475 [] equal(image(S,singleton(union(x,y))),intersection(image(S,singleton(x)),image(S,singleton(y)))). 1476 [] -member(x,V)| -subclass(y,x)|member(y,P(x)). 1477 [] -member(x,y)|member(A(y),P(x)). 1478 [] equal(x,0)|member(A(x),V). 1479 [] -subclass(x,image(S,singleton(y)))|subclass(y,A(x)). 1480 [] -subclass(x,A(y))|subclass(y,image(S,singleton(x))). 1481 [] equal(intersection(complement(image(S,singleton(A(x)))),x),0). 1482 [] -member(x,V)|equal(union(complement(image(V,singleton(x))),x),x). 1483 [] equal(A(image(S,singleton(x))),union(complement(image(V,singleton(x))),x)). 1484 [] -member(x,V)|member(D(x),V). 1485 [] -member(x,V)|member(R(x),V). 1486 [] -member(x,V)|member(image(x,y),V). 1487 [] -member(x,V)|member(fix(x),V). 1488 [] -member(pair(x,y),cart(V,V))|member(cart(x,y),V). 1489 [] -member(pair(x,y),cart(V,V))|member(restrict(z,x,y),V). 1490 [] -member(composite(x,y),V)|member(image(x,R(y)),V). 1491 [] -member(composite(x,y),V)|member(image(inverse(y),D(x)),V). 1492 [] -member(image(x,R(y)),V)| -member(image(inverse(y),D(x)),V)|member(composite(x,y),V). 1493 [] -member(composite(x,id(y)),V)|member(image(x,y),V). 1494 [] -member(x,V)| -member(image(y,x),V)|member(composite(y,id(x)),V). 1495 [] -member(composite(id(x),y),V)|member(image(inverse(y),x),V). 1496 [] -member(x,V)| -member(image(y,x),V)|member(composite(id(x),inverse(y)),V). 1497 [] equal(image(V,singleton(composite(x,y))),intersection(image(V,singleton(image(x,R(y)))),image(V,singleton(image(inverse(y),D(x)))))). 1498 [] subclass(composite(id(x),E),cart(U(x),x)). 1499 [] -member(x,V)|member(composite(id(x),E),V). 1500 [] -member(pair(D(x),R(x)),cart(V,V))| -subclass(x,cart(V,V))|member(x,V). 1501 [] -member(x,V)|member(inverse(x),V). 1502 [] -equal(singleton(inverse(x)),0)|equal(singleton(x),0). 1503 [] -FUNCTION(x)| -member(D(x),V)|member(x,V). 1504 [] -member(x,V)|member(flip(x),V). 1505 [] -member(x,V)|member(D(flip(x)),V). 1506 [] -member(x,V)|member(rotate(x),V). 1507 [] -member(pair(x,y),cart(V,V))|member(composite(x,y),V). end_of_list. ------- end included file U:\RP\RP1.USE------- include("U:\RP\RP2-REF.USE"). ------- start included file U:\RP\RP2-REF.USE------- list(usable). 1508 [] -FUNCTION(composite(Id,x))|FUNCTION(restrict(x,y,z)). 1509 [] -member(x,V)|member(D(restrict(y,x,z)),V). 1510 [] -FUNCTION(composite(Id,x))| -member(y,V)|member(restrict(x,y,z),V). 1511 [] -member(U(x),V)|member(x,V). 1512 [] -member(x,V)|member(image(inverse(S),x),V). 1513 [] equal(image(V,singleton(image(inverse(S),x))),image(V,singleton(x))). 1514 [] -member(P(x),V)|member(x,V). 1515 [] -member(union(x,y),V)|member(x,V). 1516 [] equal(image(V,singleton(union(x,y))),intersection(image(V,singleton(x)),image(V,singleton(y)))). 1517 [] -member(union(x,y),V)|member(pair(x,y),cart(V,V)). 1518 [] -member(cart(x,y),V)|equal(y,0)|member(x,V). 1519 [] -member(cart(x,y),V)|equal(x,0)|member(y,V). 1520 [] equal(image(V,singleton(cart(x,y))),union(complement(image(V,x)),union(complement(image(V,y)),intersection(image(V,singleton(x)),image(V,singleton(y)))))). 1521 [] -member(x,V)|member(id(x),V). 1522 [] -member(id(x),V)|member(x,V). end_of_list. ------- end included file U:\RP\RP2-REF.USE------- include("U:\GREATEST\GT.USE"). ------- start included file U:\GREATEST\GT.USE------- list(usable). 1523 [] equal(intersection(UB(x),inverse(E)),GREATEST(x)). 1524 [] equal(GREATEST(cart(x,y)),restrict(inverse(E),P(x),y)). 1525 [] equal(GREATEST(Id),inverse(SINGLETON)). 1526 [] subclass(GREATEST(x),cart(V,V)). 1527 [] equal(GREATEST(composite(Id,x)),GREATEST(x)). 1528 [] subclass(composite(GREATEST(x),inverse(GREATEST(x))),x). 1529 [] -subclass(intersection(x,inverse(x)),Id)|FUNCTION(GREATEST(x)). 1530 [] equal(GREATEST(0),0). 1531 [] subclass(D(GREATEST(x)),P(D(x))). 1532 [] equal(R(GREATEST(x)),fix(x)). 1533 [] equal(GREATEST(intersection(x,y)),intersection(GREATEST(x),GREATEST(y))). 1534 [] equal(GREATEST(restrict(x,y,z)),restrict(GREATEST(x),P(y),z)). 1535 [] equal(image(GREATEST(x),P(y)),intersection(y,fix(x))). 1536 [] equal(D(GREATEST(restrict(x,y,y))),intersection(D(GREATEST(x)),P(y))). 1537 [] equal(GREATEST(id(x)),composite(id(x),inverse(SINGLETON))). 1538 [] -member(pair(x,y),GREATEST(z))|subclass(cart(x,singleton(y)),z). 1539 [] -member(pair(x,y),GREATEST(z))|member(y,x). 1540 [] -member(x,V)| -member(y,x)| -subclass(cart(x,singleton(y)),z)|member(pair(x,y),GREATEST(z)). 1541 [] -member(pair(x,y),UB(z))| -member(pair(u,y),GREATEST(z))|member(pair(union(x,u),y),GREATEST(z)). 1542 [] -member(pair(x,y),cart(V,V))| -member(pairset(x,y),D(GREATEST(z)))|member(pair(x,y),union(z,inverse(z))). 1543 [] -member(x,fix(y))|member(pair(singleton(x),x),GREATEST(y)). 1544 [] equal(composite(GREATEST(x),S),composite(id(fix(x)),UB(x))). end_of_list. ------- end included file U:\GREATEST\GT.USE------- include("U:\LEAST\LT.USE"). ------- start included file U:\LEAST\LT.USE------- list(usable). 1545 [] equal(intersection(LB(x),inverse(E)),LEAST(x)). 1546 [] subclass(LEAST(x),cart(V,V)). 1547 [] equal(composite(Id,LEAST(x)),LEAST(x)). 1548 [] subclass(D(LEAST(x)),P(R(x))). 1549 [] equal(GREATEST(inverse(x)),LEAST(x)). 1550 [] equal(LEAST(inverse(x)),GREATEST(x)). 1551 [] equal(LEAST(0),0). 1552 [] equal(LEAST(cart(x,y)),restrict(inverse(E),P(y),x)). 1553 [] equal(LEAST(restrict(x,y,z)),restrict(LEAST(x),P(z),y)). 1554 [] equal(LEAST(id(x)),composite(id(x),inverse(SINGLETON))). 1555 [] equal(R(LEAST(x)),fix(x)). 1556 [] equal(image(LEAST(x),P(y)),intersection(y,fix(x))). 1557 [] equal(D(LEAST(restrict(x,y,y))),intersection(D(LEAST(x)),P(y))). 1558 [] equal(LEAST(intersection(x,y)),intersection(LEAST(x),LEAST(y))). 1559 [] -member(pair(x,y),LEAST(z))|subclass(cart(singleton(y),x),z). 1560 [] -member(pair(x,y),LEAST(z))|member(y,x). 1561 [] -member(x,y)| -member(y,V)| -subclass(cart(singleton(x),y),z)|member(pair(y,x),LEAST(z)). 1562 [] -member(x,y)| -member(pair(y,z),LEAST(u))|member(pair(z,x),u). 1563 [] -member(0,D(LEAST(x))). 1564 [] -member(pair(x,y),cart(V,V))| -member(pairset(x,y),D(LEAST(z)))|member(pair(x,y),union(z,inverse(z))). 1565 [] -member(x,fix(y))|member(pair(singleton(x),x),LEAST(y)). 1566 [] equal(LEAST(composite(Id,x)),LEAST(x)). 1567 [] -subclass(intersection(x,inverse(x)),Id)|FUNCTION(LEAST(x)). end_of_list. ------- end included file U:\LEAST\LT.USE------- include("U:\GLB\GLB.USE"). ------- start included file U:\GLB\GLB.USE------- list(usable). 1568 [] equal(intersection(LB(x),complement(composite(complement(x),LB(x)))),GLB(x)). 1569 [] equal(intersection(GLB(x),inverse(E)),LEAST(x)). 1570 [] subclass(LEAST(x),GLB(x)). 1571 [] equal(GLB(composite(Id,x)),GLB(x)). 1572 [] subclass(GLB(x),cart(V,V)). 1573 [] subclass(composite(GLB(x),inverse(GLB(x))),x). 1574 [] -subclass(intersection(x,inverse(x)),Id)|FUNCTION(GLB(x)). end_of_list. ------- end included file U:\GLB\GLB.USE------- include("U:\LUB\LUB.USE"). ------- start included file U:\LUB\LUB.USE------- list(usable). 1575 [] equal(GLB(inverse(x)),LUB(x)). 1576 [] -subclass(intersection(x,inverse(x)),Id)|FUNCTION(LUB(x)). 1577 [] equal(LUB(inverse(x)),GLB(x)). 1578 [] equal(LUB(composite(Id,x)),LUB(x)). 1579 [] subclass(LUB(x),cart(V,V)). end_of_list. ------- end included file U:\LUB\LUB.USE------- include("U:\RFX\RFX.USE"). ------- start included file U:\RFX\RFX.USE------- list(usable). 1580 [] -REFLEXIVE(x)|subclass(x,cart(fix(x),fix(x))). 1581 [] -subclass(x,cart(fix(x),fix(x)))|REFLEXIVE(x). 1582 [] -REFLEXIVE(x)| -member(pair(y,z),x)|member(pair(y,y),x). 1583 [] -REFLEXIVE(x)| -member(pair(y,z),x)|member(pair(z,z),x). 1584 [] -REFLEXIVE(x)| -member(pair(y,z),x)|member(pair(pairset(y,z),y),LEAST(x)). 1585 [] -REFLEXIVE(x)|subclass(intersection(x,inverse(x)),composite(LEAST(x),inverse(LEAST(x)))). 1586 [] -FUNCTION(LEAST(x))| -REFLEXIVE(x)|subclass(intersection(x,inverse(x)),Id). 1587 [] -REFLEXIVE(x)|equal(composite(Id,x),x). 1588 [] -REFLEXIVE(x)|REFLEXIVE(inverse(x)). 1589 [] -REFLEXIVE(x)|equal(D(x),fix(x)). 1590 [] -REFLEXIVE(x)|equal(R(x),fix(x)). 1591 [] -REFLEXIVE(x)|subclass(x,composite(x,x)). 1592 [] REFLEXIVE(0). 1593 [] REFLEXIVE(id(x)). 1594 [] REFLEXIVE(S). 1595 [] REFLEXIVE(cart(x,x)). 1596 [] -REFLEXIVE(cart(x,y))|equal(x,y)|equal(cart(x,y),0). 1597 [] -REFLEXIVE(x)| -REFLEXIVE(y)|REFLEXIVE(intersection(x,y)). 1598 [] -REFLEXIVE(x)|REFLEXIVE(restrict(x,y,y)). 1599 [] -REFLEXIVE(x)| -REFLEXIVE(y)|REFLEXIVE(union(x,y)). 1600 [] -REFLEXIVE(x)| -member(fix(x),V)|member(x,V). end_of_list. ------- end included file U:\RFX\RFX.USE------- include("U:\SYM\SYM.USE"). ------- start included file U:\SYM\SYM.USE------- list(usable). 1601 [] -SYMMETRIC(x)|subclass(x,inverse(x)). 1602 [] -subclass(x,inverse(x))|SYMMETRIC(x). 1603 [] -SYMMETRIC(x)| -member(pair(y,z),x)|member(pair(z,y),x). 1604 [] -SYMMETRIC(x)|subclass(x,cart(V,V)). 1605 [] -SYMMETRIC(x)|equal(inverse(x),x). 1606 [] -SYMMETRIC(x)|equal(composite(Id,x),x). 1607 [] -SYMMETRIC(x)|equal(R(x),D(x)). 1608 [] SYMMETRIC(0). 1609 [] SYMMETRIC(id(x)). 1610 [] SYMMETRIC(cart(x,x)). 1611 [] -SYMMETRIC(cart(x,y))|equal(x,y)|equal(cart(x,y),0). 1612 [] -SYMMETRIC(x)| -SYMMETRIC(y)|SYMMETRIC(intersection(x,y)). 1613 [] -SYMMETRIC(x)|SYMMETRIC(restrict(x,y,y)). 1614 [] -SYMMETRIC(x)| -SYMMETRIC(y)|SYMMETRIC(union(x,y)). 1615 [] -SYMMETRIC(x)| -member(D(x),V)|member(x,V). end_of_list. ------- end included file U:\SYM\SYM.USE------- include("U:\TRV\TRV.USE"). ------- start included file U:\TRV\TRV.USE------- list(usable). 1616 [] -TRANSITIVE(x)|subclass(x,composite(Id,complement(composite(complement(x),inverse(x))))). 1617 [] -subclass(x,composite(Id,complement(composite(complement(x),inverse(x)))))|TRANSITIVE(x). 1618 [] -TRANSITIVE(x)|subclass(x,cart(V,V)). 1619 [] -TRANSITIVE(x)|subclass(composite(x,x),x). 1620 [] -subclass(x,cart(V,V))| -subclass(composite(x,x),x)|TRANSITIVE(x). 1621 [] -TRANSITIVE(x)|equal(composite(Id,x),x). 1622 [] -TRANSITIVE(x)| -member(pair(y,z),x)| -member(pair(z,u),x)|member(pair(y,u),x). 1623 [] -TRANSITIVE(x)| -member(pair(y,z),x)|subclass(image(x,singleton(z)),image(x,singleton(y))). 1624 [] TRANSITIVE(0). 1625 [] TRANSITIVE(id(x)). 1626 [] TRANSITIVE(S). 1627 [] TRANSITIVE(cart(x,y)). 1628 [] -TRANSITIVE(x)|TRANSITIVE(inverse(x)). 1629 [] -TRANSITIVE(x)| -TRANSITIVE(y)|TRANSITIVE(intersection(x,y)). 1630 [] -TRANSITIVE(x)|TRANSITIVE(restrict(x,y,z)). 1631 [] -TRANSITIVE(x)| -subclass(y,Id)|TRANSITIVE(union(x,y)). 1632 [] -TRANSITIVE(intersection(x,Di))|TRANSITIVE(composite(Id,x)). 1633 [] -TRANSITIVE(intersection(x,Di))|subclass(intersection(x,inverse(x)),Id). 1634 [] -TRANSITIVE(x)| -subclass(intersection(x,inverse(x)),Id)|TRANSITIVE(intersection(x,Di)). end_of_list. ------- end included file U:\TRV\TRV.USE------- include("U:\POSET\POR.USE"). ------- start included file U:\POSET\POR.USE------- list(usable). 1635 [] -PARTIALORDER(x)|REFLEXIVE(x). 1636 [] -PARTIALORDER(x)|TRANSITIVE(intersection(x,Di)). 1637 [] -REFLEXIVE(x)| -TRANSITIVE(intersection(x,Di))|PARTIALORDER(x). 1638 [] -PARTIALORDER(x)|PARTIALORDER(union(x,id(y))). 1639 [] -TRANSITIVE(x)| -subclass(x,intersection(Di,cart(y,y)))|PARTIALORDER(union(x,id(y))). 1640 [] -PARTIALORDER(x)|subclass(intersection(x,inverse(x)),Id). 1641 [] -PARTIALORDER(x)|TRANSITIVE(x). 1642 [] -REFLEXIVE(x)| -subclass(intersection(x,inverse(x)),Id)| -TRANSITIVE(x)|PARTIALORDER(x). 1643 [] -PARTIALORDER(x)|equal(intersection(x,inverse(x)),id(fix(x))). 1644 [] -PARTIALORDER(x)|equal(composite(x,x),x). 1645 [] PARTIALORDER(0). 1646 [] PARTIALORDER(S). 1647 [] -PARTIALORDER(x)|PARTIALORDER(inverse(x)). 1648 [] PARTIALORDER(id(x)). 1649 [] -PARTIALORDER(x)| -REFLEXIVE(y)| -TRANSITIVE(y)|PARTIALORDER(intersection(x,y)). 1650 [] -PARTIALORDER(x)|PARTIALORDER(intersection(x,cart(y,y))). end_of_list. ------- end included file U:\POSET\POR.USE------- include("U:\TOTALORD\TO.USE"). ------- start included file U:\TOTALORD\TO.USE------- list(usable). 1651 [] -TOTALORDER(x)|PARTIALORDER(x). 1652 [] -TOTALORDER(x)|TRANSITIVE(intersection(Di,x)). 1653 [] -TOTALORDER(x)|equal(union(x,inverse(x)),cart(fix(x),fix(x))). 1654 [] -TRANSITIVE(intersection(Di,x))| -equal(union(x,inverse(x)),cart(fix(x),fix(x)))|TOTALORDER(x). 1655 [] -PARTIALORDER(x)| -equal(union(x,inverse(x)),cart(fix(x),fix(x)))|TOTALORDER(x). 1656 [] -TOTALORDER(x)| -member(pair(y,z),cart(fix(x),fix(x)))|member(pair(y,z),x)|member(pair(z,y),x). 1657 [] TOTALORDER(0). 1658 [] TOTALORDER(id(singleton(x))). 1659 [] -TOTALORDER(x)|TOTALORDER(inverse(x)). 1660 [] -TOTALORDER(x)|TOTALORDER(intersection(x,cart(y,y))). end_of_list. ------- end included file U:\TOTALORD\TO.USE------- include("U:\EQV\EQV1.USE"). ------- start included file U:\EQV\EQV1.USE------- list(usable). 1661 [] -EQUIVALENCE(x)|equal(composite(x,inverse(x)),x). 1662 [] -equal(composite(x,inverse(x)),x)|EQUIVALENCE(x). 1663 [] -EQUIVALENCE(x)|subclass(x,cart(V,V)). 1664 [] -EQUIVALENCE(x)|equal(composite(Id,x),x). 1665 [] -EQUIVALENCE(x)|equal(inverse(x),x). 1666 [] -EQUIVALENCE(x)|SYMMETRIC(x). 1667 [] -EQUIVALENCE(x)|equal(composite(x,x),x). 1668 [] -EQUIVALENCE(x)|TRANSITIVE(x). 1669 [] -EQUIVALENCE(x)| -member(pair(y,z),x)|member(pair(z,y),x). 1670 [] -EQUIVALENCE(x)| -member(pair(y,z),x)|member(pair(y,y),x). 1671 [] -EQUIVALENCE(x)| -member(pair(y,z),x)|member(pair(z,z),x). 1672 [] -EQUIVALENCE(x)| -member(pair(y,z),x)| -member(pair(z,u),x)|member(pair(y,u),x). 1673 [] -member(pair(x,y),z)| -subclass(z,inverse(z))| -subclass(composite(z,z),z)|member(pair(x,x),z). 1674 [] -member(pair(x,y),z)| -subclass(z,inverse(z))| -subclass(composite(z,z),z)|member(pair(y,y),z). 1675 [] -EQUIVALENCE(x)|equal(D(x),fix(x)). 1676 [] -EQUIVALENCE(x)|equal(R(x),fix(x)). 1677 [] -EQUIVALENCE(x)|subclass(x,cart(fix(x),fix(x))). 1678 [] -EQUIVALENCE(x)|REFLEXIVE(x). 1679 [] -subclass(x,inverse(x))| -subclass(composite(x,x),x)|equal(D(x),fix(x)). 1680 [] -subclass(x,inverse(x))| -subclass(composite(x,x),x)|equal(R(x),fix(x)). 1681 [] -subclass(x,inverse(x))| -subclass(composite(x,x),x)|subclass(x,cart(fix(x),fix(x))). 1682 [] -SYMMETRIC(x)| -TRANSITIVE(x)|REFLEXIVE(x). 1683 [] -SYMMETRIC(x)| -TRANSITIVE(x)|EQUIVALENCE(x). 1684 [] -subclass(x,inverse(x))| -subclass(composite(x,x),x)|EQUIVALENCE(x). end_of_list. ------- end included file U:\EQV\EQV1.USE------- include("U:\EQV\EQV2.USE"). ------- start included file U:\EQV\EQV2.USE------- list(usable). 1685 [] EQUIVALENCE(0). 1686 [] EQUIVALENCE(id(x)). 1687 [] -FUNCTION(x)|EQUIVALENCE(composite(inverse(x),x)). 1688 [] EQUIVALENCE(cart(x,x)). 1689 [] -EQUIVALENCE(cart(x,y))|equal(x,y)|equal(cart(x,y),0). 1690 [] -EQUIVALENCE(x)|equal(image(complement(x),y),V)|subclass(cart(y,y),x). 1691 [] -EQUIVALENCE(x)| -EQUIVALENCE(y)|EQUIVALENCE(intersection(x,y)). 1692 [] -EQUIVALENCE(x)|EQUIVALENCE(restrict(x,y,y)). 1693 [] -EQUIVALENCE(x)|subclass(composite(complement(x),x),complement(x)). 1694 [] -EQUIVALENCE(x)|subclass(composite(x,complement(x)),complement(x)). end_of_list. ------- end included file U:\EQV\EQV2.USE------- include("U:\EQV\EQV3.USE"). ------- start included file U:\EQV\EQV3.USE------- list(usable). 1695 [] -EQUIVALENCE(x)| -member(pair(y,z),x)|equal(image(x,singleton(y)),image(x,singleton(z))). 1696 [] -EQUIVALENCE(x)|member(pair(y,z),x)|disjoint(image(x,singleton(y)),image(x,singleton(z))). 1697 [] -EQUIVALENCE(x)|equal(image(x,singleton(y)),image(x,singleton(z)))|disjoint(image(x,singleton(y)),image(x,singleton(z))). end_of_list. ------- end included file U:\EQV\EQV3.USE------- include("U:\RUS\RUS1.USE"). ------- start included file U:\RUS\RUS1.USE------- list(usable). 1698 [] equal(fix(E),complement(RUSSELL)). 1699 [] -member(x,x)| -member(x,RUSSELL). 1700 [] -member(x,V)|member(x,x)|member(x,RUSSELL). 1701 [] -member(x,RUSSELL)|member(singleton(x),RUSSELL). 1702 [] -member(RUSSELL,x). 1703 [] -member(P(RUSSELL),x). 1704 [] equal(singleton(RUSSELL),0). 1705 [] subclass(P(RUSSELL),RUSSELL). 1706 [] -member(x,P(RUSSELL))|member(singleton(x),P(RUSSELL)). 1707 [] -member(x,P(RUSSELL))|member(succ(x),P(RUSSELL)). 1708 [] -member(intersection(RUSSELL,x),x). 1709 [] -member(x,V)|member(intersection(RUSSELL,x),P(RUSSELL)). end_of_list. ------- end included file U:\RUS\RUS1.USE------- include("U:\RUS\RUS2.USE"). ------- start included file U:\RUS\RUS2.USE------- list(usable). 1710 [] equal(A(RUSSELL),0). 1711 [] subclass(intersection(RUSSELL,A(x)),complement(x)). 1712 [] -member(x,x)|subclass(x,U(x)). 1713 [] subclass(x,union(RUSSELL,U(x))). 1714 [] -subclass(U(x),RUSSELL)|subclass(x,RUSSELL). 1715 [] subclass(image(SINGLETON,RUSSELL),RUSSELL). 1716 [] -member(U(x),P(RUSSELL))|member(x,P(RUSSELL)). 1717 [] subclass(P(x),union(RUSSELL,x)). 1718 [] -subclass(RUSSELL,x)|subclass(P(x),x). 1719 [] -member(x,P(RUSSELL))|member(P(x),P(RUSSELL)). 1720 [] -member(P(x),P(x)). 1721 [] -member(x,V)| -subclass(P(x),x). 1722 [] -member(x,V)|member(P(x),RUSSELL). 1723 [] equal(U(RUSSELL),V). 1724 [] equal(image(inverse(S),RUSSELL),V). 1725 [] equal(composite(complement(S),S),cart(V,V)). 1726 [] equal(composite(complement(S),E),cart(V,V)). end_of_list. ------- end included file U:\RUS\RUS2.USE------- include("U:\REG\REG1.USE"). ------- start included file U:\REG\REG1.USE------- list(usable). 1727 [] equal(complement(fix(composite(E,DISJOINT))),DESCENDING). 1728 [] -member(x,DESCENDING)|subclass(x,image(E,x)). 1729 [] -member(x,V)| -subclass(x,image(E,x))|member(x,DESCENDING). 1730 [] member(0,DESCENDING). 1731 [] equal(A(DESCENDING),0). 1732 [] -member(x,P(DESCENDING))|member(U(x),DESCENDING). 1733 [] -member(x,DESCENDING)|member(union(x,singleton(y)),DESCENDING)|disjoint(x,y). 1734 [] -member(x,y)| -member(x,U(DESCENDING))| -member(y,V)|member(y,U(DESCENDING)). 1735 [] subclass(image(E,U(DESCENDING)),U(DESCENDING)). 1736 [] -member(x,x)|member(singleton(x),DESCENDING). 1737 [] -member(x,complement(x))| -member(singleton(x),DESCENDING). 1738 [] -member(x,y)| -member(y,x)|member(pairset(x,y),DESCENDING). end_of_list. ------- end included file U:\REG\REG1.USE------- include("U:\REG\REG2.USE"). ------- start included file U:\REG\REG2.USE------- list(usable). 1739 [] equal(complement(U(DESCENDING)),REGULAR). 1740 [] equal(complement(REGULAR),U(DESCENDING)). 1741 [] equal(P(REGULAR),REGULAR). 1742 [] equal(image(E,U(DESCENDING)),U(DESCENDING)). 1743 [] -member(x,V)|member(intersection(REGULAR,x),REGULAR). 1744 [] -subclass(x,REGULAR)|subclass(U(x),REGULAR). 1745 [] -subclass(U(x),REGULAR)|subclass(x,REGULAR). 1746 [] -subclass(x,REGULAR)|subclass(P(x),REGULAR). 1747 [] equal(image(inverse(S),U(DESCENDING)),image(V,U(DESCENDING))). 1748 [] equal(U(U(DESCENDING)),image(V,U(DESCENDING))). 1749 [] -member(DESCENDING,V)|equal(REGULAR,V). 1750 [] equal(image(Di,U(DESCENDING)),image(V,U(DESCENDING))). 1751 [] equal(A(U(DESCENDING)),complement(image(V,U(DESCENDING)))). 1752 [] equal(image(V,REGULAR),V). 1753 [] equal(U(REGULAR),REGULAR). 1754 [] -subclass(P(x),REGULAR)|subclass(x,REGULAR). 1755 [] equal(image(inverse(S),REGULAR),REGULAR). 1756 [] -member(x,REGULAR)|subclass(x,REGULAR). 1757 [] -member(x,y)| -member(y,REGULAR)|member(x,REGULAR). 1758 [] -member(x,REGULAR)|member(P(x),REGULAR). 1759 [] -member(x,REGULAR)|member(U(x),REGULAR). 1760 [] -member(x,REGULAR)| -subclass(y,x)|member(y,REGULAR). 1761 [] member(0,REGULAR). 1762 [] equal(intersection(REGULAR,P(U(DESCENDING))),singleton(0)). 1763 [] equal(image(S,REGULAR),V). 1764 [] equal(image(DISJOINT,REGULAR),V). 1765 [] equal(A(REGULAR),0). 1766 [] -member(x,REGULAR)| -member(y,REGULAR)|member(union(x,y),REGULAR). 1767 [] -member(x,REGULAR)|member(intersection(x,y),REGULAR). 1768 [] -member(x,REGULAR)|member(singleton(x),REGULAR). 1769 [] -member(x,REGULAR)| -member(y,REGULAR)|member(pairset(x,y),REGULAR). 1770 [] -member(P(x),REGULAR)|member(x,REGULAR). 1771 [] -member(U(x),REGULAR)|member(x,REGULAR). 1772 [] -member(pair(x,y),cart(REGULAR,REGULAR))|member(cart(x,y),REGULAR). 1773 [] -member(x,DESCENDING)|disjoint(x,REGULAR). 1774 [] -member(x,DESCENDING)| -member(y,REGULAR)|disjoint(x,y). 1775 [] equal(intersection(DESCENDING,REGULAR),singleton(0)). 1776 [] -disjoint(DESCENDING,image(E,x))|subclass(x,REGULAR). 1777 [] -subclass(x,REGULAR)|disjoint(DESCENDING,image(E,x)). 1778 [] -member(x,REGULAR)|member(D(x),REGULAR). 1779 [] -member(x,REGULAR)|member(R(x),REGULAR). 1780 [] -member(x,REGULAR)|member(rotate(x),REGULAR). 1781 [] -subclass(x,REGULAR)|subclass(D(x),REGULAR). 1782 [] -subclass(x,REGULAR)|subclass(R(x),REGULAR). 1783 [] subclass(cart(REGULAR,REGULAR),REGULAR). 1784 [] -member(x,REGULAR)| -subclass(x,image(E,x))|equal(x,0). 1785 [] -member(REGULAR,x). 1786 [] equal(image(Di,REGULAR),V). 1787 [] equal(singleton(REGULAR),0). 1788 [] -member(cart(REGULAR,REGULAR),x). 1789 [] equal(D(REGULAR),REGULAR). 1790 [] equal(R(REGULAR),REGULAR). 1791 [] -member(x,REGULAR)|member(first(x),REGULAR). 1792 [] -member(x,REGULAR)|member(second(x),REGULAR). 1793 [] equal(intersection(REGULAR,cart(V,V)),cart(REGULAR,REGULAR)). 1794 [] equal(composite(x,REGULAR),cart(REGULAR,image(x,REGULAR))). 1795 [] equal(composite(REGU