1%-------------------------------------------------------------------------- 2% File : SET004-0 : TPTP v6.4.0. Bugfixed v2.1.0. 3% Domain : Set Theory 4% Axioms : Set theory axioms based on NBG set theory 5% Version : [Qua92] axioms. 6% English : 7 8% Refs : [Qua92] Quaife (1992), Automated Deduction in von Neumann-Bern 9% Source : [Qua92] 10% Names : 11 12% Status : Satisfiable 13% Syntax : Number of clauses : 91 ( 8 non-Horn; 29 unit; 62 RR) 14% Number of atoms : 181 ( 39 equality) 15% Maximal clause size : 5 ( 2 average) 16% Number of predicates : 10 ( 0 propositional; 1-3 arity) 17% Number of functors : 38 ( 8 constant; 0-3 arity) 18% Number of variables : 176 ( 25 singleton) 19% Maximal term depth : 6 ( 2 average) 20% SPC : 21 22% Comments : 23% Bugfixes : v2.1.0 - Clause compatible4 fixed 24%-------------------------------------------------------------------------- 25%----GROUP 1: AXIOMS AND BASIC DEFINITIONS. 26 27%----Axiom A-1: sets are classes (omitted because all objects are 28%----classes). 29 30%----Definition of < (subclass). 31%----a:x:a:y:((x < y) <=> a:u:((u e x) ==> (u e y))). 32cnf(subclass_members,axiom, 33 ( ~ subclass(X,Y) 34 | ~ member(U,X) 35 | member(U,Y) )). 36 37cnf(not_subclass_members1,axiom, 38 ( member(not_subclass_element(X,Y),X) 39 | subclass(X,Y) )). 40 41cnf(not_subclass_members2,axiom, 42 ( ~ member(not_subclass_element(X,Y),Y) 43 | subclass(X,Y) )). 44 45%----Axiom A-2: elements of classes are sets. 46%----a:x:(x < universal_class). 47%----Singleton variables OK. 48cnf(class_elements_are_sets,axiom, 49 ( subclass(X,universal_class) )). 50 51%----Axiom A-3: principle of extensionality. 52%----a:x:a:y:((x = y) <=> (x < y) & (y < x)). 53cnf(equal_implies_subclass1,axiom, 54 ( X != Y 55 | subclass(X,Y) )). 56 57cnf(equal_implies_subclass2,axiom, 58 ( X != Y 59 | subclass(Y,X) )). 60 61cnf(subclass_implies_equal,axiom, 62 ( ~ subclass(X,Y) 63 | ~ subclass(Y,X) 64 | X = Y )). 65 66%----Axiom A-4: existence of unordered pair. 67%----a:u:a:x:a:y:((u e {x, y}) <=> (u e universal_class) 68%----& (u = x | u = y)). 69%----a:x:a:y:({x, y} e universal_class). 70cnf(unordered_pair_member,axiom, 71 ( ~ member(U,unordered_pair(X,Y)) 72 | U = X 73 | U = Y )). 74 75%----(x e universal_class), (u = x) --> (u e {x, y}). 76%----Singleton variables OK. 77cnf(unordered_pair2,axiom, 78 ( ~ member(X,universal_class) 79 | member(X,unordered_pair(X,Y)) )). 80 81%----(y e universal_class), (u = y) --> (u e {x, y}). 82%----Singleton variables OK. 83cnf(unordered_pair3,axiom, 84 ( ~ member(Y,universal_class) 85 | member(Y,unordered_pair(X,Y)) )). 86 87%----Singleton variables OK. 88cnf(unordered_pairs_in_universal,axiom, 89 ( member(unordered_pair(X,Y),universal_class) )). 90 91%----Definition of singleton set. 92%----a:x:({x} = {x, x}). 93cnf(singleton_set,axiom, 94 ( unordered_pair(X,X) = singleton(X) )). 95 96%----See Theorem (SS6) for memb. 97 98%----Definition of ordered pair. 99%----a:x:a:y:([x,y] = {{x}, {x, {y}}}). 100cnf(ordered_pair,axiom, 101 ( unordered_pair(singleton(X),unordered_pair(X,singleton(Y))) = ordered_pair(X,Y) )). 102 103%----Axiom B-5'a: Cartesian product. 104%----a:u:a:v:a:y:(([u,v] e cross_product(x,y)) <=> (u e x) & (v e y)). 105%----Singleton variables OK. 106cnf(cartesian_product1,axiom, 107 ( ~ member(ordered_pair(U,V),cross_product(X,Y)) 108 | member(U,X) )). 109 110%----Singleton variables OK. 111cnf(cartesian_product2,axiom, 112 ( ~ member(ordered_pair(U,V),cross_product(X,Y)) 113 | member(V,Y) )). 114 115cnf(cartesian_product3,axiom, 116 ( ~ member(U,X) 117 | ~ member(V,Y) 118 | member(ordered_pair(U,V),cross_product(X,Y)) )). 119 120%----See Theorem (OP6) for 1st and 2nd. 121 122%----Axiom B-5'b: Cartesian product. 123%----a:z:(z e cross_product(x,y) --> ([first(z),second(z)] = z) 124%----Singleton variables OK. 125cnf(cartesian_product4,axiom, 126 ( ~ member(Z,cross_product(X,Y)) 127 | ordered_pair(first(Z),second(Z)) = Z )). 128 129%----Axiom B-1: E (element relation). 130%----(E < cross_product(universal_class,universal_class)). 131%----a:x:a:y:(([x,y] e E) <=> ([x,y] e cross_product(universal_class, 132%----universal_class)) (x e y)). 133cnf(element_relation1,axiom, 134 ( subclass(element_relation,cross_product(universal_class,universal_class)) )). 135 136cnf(element_relation2,axiom, 137 ( ~ member(ordered_pair(X,Y),element_relation) 138 | member(X,Y) )). 139 140cnf(element_relation3,axiom, 141 ( ~ member(ordered_pair(X,Y),cross_product(universal_class,universal_class)) 142 | ~ member(X,Y) 143 | member(ordered_pair(X,Y),element_relation) )). 144 145%----Axiom B-2: * (intersection). 146%----a:z:a:x:a:y:((z e (x * y)) <=> (z e x) & (z e y)). 147%----Singleton variables OK. 148cnf(intersection1,axiom, 149 ( ~ member(Z,intersection(X,Y)) 150 | member(Z,X) )). 151 152%----Singleton variables OK. 153cnf(intersection2,axiom, 154 ( ~ member(Z,intersection(X,Y)) 155 | member(Z,Y) )). 156 157cnf(intersection3,axiom, 158 ( ~ member(Z,X) 159 | ~ member(Z,Y) 160 | member(Z,intersection(X,Y)) )). 161 162%----Axiom B-3: complement. 163%----a:z:a:x:((z e ~(x)) <=> (z e universal_class) & -(z e x)). 164cnf(complement1,axiom, 165 ( ~ member(Z,complement(X)) 166 | ~ member(Z,X) )). 167 168cnf(complement2,axiom, 169 ( ~ member(Z,universal_class) 170 | member(Z,complement(X)) 171 | member(Z,X) )). 172 173%---- Theorem (SP2) introduces the null class O. 174 175%----Definition of + (union). 176%----a:x:a:y:((x + y) = ~((~(x) * ~(y)))). 177cnf(union,axiom, 178 ( complement(intersection(complement(X),complement(Y))) = union(X,Y) )). 179 180%----Definition of & (exclusive or). (= symmetric difference). 181%----a:x:a:y:((x y) = (~(x * y) * ~(~(x) * ~(y)))). 182cnf(symmetric_difference,axiom, 183 ( intersection(complement(intersection(X,Y)),complement(intersection(complement(X),complement(Y)))) = symmetric_difference(X,Y) )). 184 185%----Definition of restriction. 186%----a:x(restrict(xr,x,y) = (xr * cross_product(x,y))). 187%----This is extra to the paper 188cnf(restriction1,axiom, 189 ( intersection(Xr,cross_product(X,Y)) = restrict(Xr,X,Y) )). 190 191cnf(restriction2,axiom, 192 ( intersection(cross_product(X,Y),Xr) = restrict(Xr,X,Y) )). 193 194%----Axiom B-4: D (domain_of). 195%----a:y:a:z:((z e domain_of(x)) <=> (z e universal_class) & 196%---- -(restrict(x,{z},universal_class) = O)). 197%----next is subsumed by A-2. 198%------> (domain_of(x) < universal_class). 199cnf(domain1,axiom, 200 ( restrict(X,singleton(Z),universal_class) != null_class 201 | ~ member(Z,domain_of(X)) )). 202 203cnf(domain2,axiom, 204 ( ~ member(Z,universal_class) 205 | restrict(X,singleton(Z),universal_class) = null_class 206 | member(Z,domain_of(X)) )). 207 208%----Axiom B-7: rotate. 209%----a:x:(rotate(x) < cross_product(cross_product(universal_class, 210%----universal_class),universal_class)). 211%----a:x:a:u:a:v:a:w:(([[u,v],w] e rotate(x)) <=> ([[u,v],w]] 212%---- e cross_product(cross_product(universal_class,universal_class), 213%----universal_class)) & ([[v,w],u]] e x). 214%----Singleton variables OK. 215cnf(rotate1,axiom, 216 ( subclass(rotate(X),cross_product(cross_product(universal_class,universal_class),universal_class)) )). 217 218cnf(rotate2,axiom, 219 ( ~ member(ordered_pair(ordered_pair(U,V),W),rotate(X)) 220 | member(ordered_pair(ordered_pair(V,W),U),X) )). 221 222cnf(rotate3,axiom, 223 ( ~ member(ordered_pair(ordered_pair(V,W),U),X) 224 | ~ member(ordered_pair(ordered_pair(U,V),W),cross_product(cross_product(universal_class,universal_class),universal_class)) 225 | member(ordered_pair(ordered_pair(U,V),W),rotate(X)) )). 226 227%----Axiom B-8: flip. 228%----a:x:(flip(x) < cross_product(cross_product(universal_class, 229%----universal_class),universal_class)). 230%----a:z:a:u:a:v:a:w:(([[u,v],w] e flip(x)) <=> ([[u,v],w] 231%----e cross_product(cross_product(universal_class,universal_class), 232%----universal_class)) & ([[v,u],w] e x). 233%----Singleton variables OK. 234cnf(flip1,axiom, 235 ( subclass(flip(X),cross_product(cross_product(universal_class,universal_class),universal_class)) )). 236 237cnf(flip2,axiom, 238 ( ~ member(ordered_pair(ordered_pair(U,V),W),flip(X)) 239 | member(ordered_pair(ordered_pair(V,U),W),X) )). 240 241cnf(flip3,axiom, 242 ( ~ member(ordered_pair(ordered_pair(V,U),W),X) 243 | ~ member(ordered_pair(ordered_pair(U,V),W),cross_product(cross_product(universal_class,universal_class),universal_class)) 244 | member(ordered_pair(ordered_pair(U,V),W),flip(X)) )). 245 246%----Definition of inverse. 247%----a:y:(inverse(y) = domain_of(flip(cross_product(y,V)))). 248cnf(inverse,axiom, 249 ( domain_of(flip(cross_product(Y,universal_class))) = inverse(Y) )). 250 251%----Definition of R (range_of). 252%----a:z:(range_of(z) = domain_of(inverse(z))). 253cnf(range_of,axiom, 254 ( domain_of(inverse(Z)) = range_of(Z) )). 255 256%----Definition of domain. 257%----a:z:a:x:a:y:(domain(z,x,y) = first(notsub(restrict(z,x,{y}),O))). 258cnf(domain,axiom, 259 ( first(not_subclass_element(restrict(Z,X,singleton(Y)),null_class)) = domain(Z,X,Y) )). 260 261%----Definition of range. 262%----a:z:a:x:(range(z,x,y) = second(notsub(restrict(z,{x},y),O))). 263cnf(range,axiom, 264 ( second(not_subclass_element(restrict(Z,singleton(X),Y),null_class)) = range(Z,X,Y) )). 265 266%----Definition of image. 267%----a:x:a:xr:((xr image x) = range_of(restrict(xr,x,V))). 268cnf(image,axiom, 269 ( range_of(restrict(Xr,X,universal_class)) = image(Xr,X) )). 270 271%----Definition of successor. 272%----a:x:(successor(x) = (x + {x})). 273cnf(successor,axiom, 274 ( union(X,singleton(X)) = successor(X) )). 275 276%----Explicit definition of successor_relation. 277%------> ((cross_product(V,V) * ~(((E ^ ~(inverse((E + I)))) + 278%----(~(E) ^ inverse((E + I)))))) = successor_relation). 279%----Definition of successor_relation from the Class Existence Theorem. 280%----a:x:a:y:([x,y] e successor_relation <=> x e V & successor(x) = y). 281%----The above FOF does not agree with the book 282cnf(successor_relation1,axiom, 283 ( subclass(successor_relation,cross_product(universal_class,universal_class)) )). 284 285cnf(successor_relation2,axiom, 286 ( ~ member(ordered_pair(X,Y),successor_relation) 287 | successor(X) = Y )). 288 289%----This is what's in the book and paper. Does not change axiom. 290% input_clause(successor_relation3,axiom, 291% [--equal(successor(X),Y), 292% --member(X,universal_class), 293% ++member(ordered_pair(X,Y),successor_relation)]). 294 295%----This is what I got by email from Quaife 296cnf(successor_relation3,axiom, 297 ( successor(X) != Y 298 | ~ member(ordered_pair(X,Y),cross_product(universal_class,universal_class)) 299 | member(ordered_pair(X,Y),successor_relation) )). 300 301%----Definition of inductive a:x:(inductive(x) <=> null_class 302%----e x & (successor_relation image x) < x)). 303cnf(inductive1,axiom, 304 ( ~ inductive(X) 305 | member(null_class,X) )). 306 307cnf(inductive2,axiom, 308 ( ~ inductive(X) 309 | subclass(image(successor_relation,X),X) )). 310 311cnf(inductive3,axiom, 312 ( ~ member(null_class,X) 313 | ~ subclass(image(successor_relation,X),X) 314 | inductive(X) )). 315 316%----Axiom C-1: infinity. 317%----e:x:((x e V) & inductive(x) & a:y:(inductive(y) ==> (x < y))). 318%----e:x:((x e V) & (O e x) & ((successor_relation image x) < x) 319%---- & a:y:((O e y) & ((successor_relation image y) < y) ==> 320%----(x < y))). 321cnf(omega_is_inductive1,axiom, 322 ( inductive(omega) )). 323 324cnf(omega_is_inductive2,axiom, 325 ( ~ inductive(Y) 326 | subclass(omega,Y) )). 327 328cnf(omega_in_universal,axiom, 329 ( member(omega,universal_class) )). 330 331%----These were commented out in the set Quaife sent me, and are not 332%----in the paper true --> (null_class e omega). 333%----true --> ((successor_relation image omega) < omega). 334%----(null_class e y), ((successor_relation image y) < y) --> 335%----(omega < y). true --> (omega e universal_class). 336 337%----Definition of U (sum class). 338%----a:x:(sum_class(x) = domain_of(restrict(E,V,x))). 339cnf(sum_class_definition,axiom, 340 ( domain_of(restrict(element_relation,universal_class,X)) = sum_class(X) )). 341 342%----Axiom C-2: U (sum class). 343%----a:x:((x e V) ==> (sum_class(x) e V)). 344cnf(sum_class2,axiom, 345 ( ~ member(X,universal_class) 346 | member(sum_class(X),universal_class) )). 347 348%----Definition of P (power class). 349%----a:x:(power_class(x) = ~((E image ~(x)))). 350cnf(power_class_definition,axiom, 351 ( complement(image(element_relation,complement(X))) = power_class(X) )). 352 353%----Axiom C-3: P (power class). 354%----a:u:((u e V) ==> (power_class(u) e V)). 355cnf(power_class2,axiom, 356 ( ~ member(U,universal_class) 357 | member(power_class(U),universal_class) )). 358 359%----Definition of compose. 360%----a:xr:a:yr:((yr ^ xr) < cross_product(V,V)). 361%----a:u:a:v:a:xr:a:yr:(([u,v] e (yr ^ xr)) <=> ([u,v] 362%----e cross_product(V,V)) & (v e (yr image (xr image {u})))). 363%----Singleton variables OK. 364cnf(compose1,axiom, 365 ( subclass(compose(Yr,Xr),cross_product(universal_class,universal_class)) )). 366 367cnf(compose2,axiom, 368 ( ~ member(ordered_pair(Y,Z),compose(Yr,Xr)) 369 | member(Z,image(Yr,image(Xr,singleton(Y)))) )). 370 371cnf(compose3,axiom, 372 ( ~ member(Z,image(Yr,image(Xr,singleton(Y)))) 373 | ~ member(ordered_pair(Y,Z),cross_product(universal_class,universal_class)) 374 | member(ordered_pair(Y,Z),compose(Yr,Xr)) )). 375 376%----7/21/90 eliminate SINGVAL and just use FUNCTION. 377%----Not eliminated in TPTP - I'm following the paper 378cnf(single_valued_class1,axiom, 379 ( ~ single_valued_class(X) 380 | subclass(compose(X,inverse(X)),identity_relation) )). 381 382cnf(single_valued_class2,axiom, 383 ( ~ subclass(compose(X,inverse(X)),identity_relation) 384 | single_valued_class(X) )). 385 386%----Definition of function. 387%----a:xf:(function(xf) <=> (xf < cross_product(V,V)) & ((xf 388%----^ inverse(xf)) < identity_relation)). 389cnf(function1,axiom, 390 ( ~ function(Xf) 391 | subclass(Xf,cross_product(universal_class,universal_class)) )). 392 393cnf(function2,axiom, 394 ( ~ function(Xf) 395 | subclass(compose(Xf,inverse(Xf)),identity_relation) )). 396 397cnf(function3,axiom, 398 ( ~ subclass(Xf,cross_product(universal_class,universal_class)) 399 | ~ subclass(compose(Xf,inverse(Xf)),identity_relation) 400 | function(Xf) )). 401 402%----Axiom C-4: replacement. 403%----a:x:((x e V) & function(xf) ==> ((xf image x) e V)). 404cnf(replacement,axiom, 405 ( ~ function(Xf) 406 | ~ member(X,universal_class) 407 | member(image(Xf,X),universal_class) )). 408 409%----Axiom D: regularity. 410%----a:x:(-(x = O) ==> e:u:((u e V) & (u e x) & ((u * x) = O))). 411cnf(regularity1,axiom, 412 ( X = null_class 413 | member(regular(X),X) )). 414 415cnf(regularity2,axiom, 416 ( X = null_class 417 | intersection(X,regular(X)) = null_class )). 418 419%----Definition of apply (apply). 420%----a:xf:a:y:((xf apply y) = sum_class((xf image {y}))). 421cnf(apply,axiom, 422 ( sum_class(image(Xf,singleton(Y))) = apply(Xf,Y) )). 423 424%----Axiom E: universal choice. 425%----e:xf:(function(xf) & a:y:((y e V) ==> (y = null_class) | 426%----((xf apply y) e y))). 427cnf(choice1,axiom, 428 ( function(choice) )). 429 430cnf(choice2,axiom, 431 ( ~ member(Y,universal_class) 432 | Y = null_class 433 | member(apply(choice,Y),Y) )). 434 435%----GROUP 2: MORE SET THEORY DEFINITIONS. 436 437%----Definition of one_to_one (one-to-one function). 438%----a:xf:(one_to_one(xf) <=> function(xf) & function(inverse(xf))). 439cnf(one_to_one1,axiom, 440 ( ~ one_to_one(Xf) 441 | function(Xf) )). 442 443cnf(one_to_one2,axiom, 444 ( ~ one_to_one(Xf) 445 | function(inverse(Xf)) )). 446 447cnf(one_to_one3,axiom, 448 ( ~ function(inverse(Xf)) 449 | ~ function(Xf) 450 | one_to_one(Xf) )). 451 452%----Definition of S (subset relation). 453cnf(subset_relation,axiom, 454 ( intersection(cross_product(universal_class,universal_class),intersection(cross_product(universal_class,universal_class),complement(compose(complement(element_relation),inverse(element_relation))))) = subset_relation )). 455 456%----Definition of I (identity relation). 457cnf(identity_relation,axiom, 458 ( intersection(inverse(subset_relation),subset_relation) = identity_relation )). 459 460%----Definition of diagonalization. 461%----a:xr:(diagonalise(xr) = ~(domain_of((identity_relation * xr)))). 462cnf(diagonalisation,axiom, 463 ( complement(domain_of(intersection(Xr,identity_relation))) = diagonalise(Xr) )). 464 465%----Definition of Cantor class. 466cnf(cantor_class,axiom, 467 ( intersection(domain_of(X),diagonalise(compose(inverse(element_relation),X))) = cantor(X) )). 468 469%----Definition of operation. 470%----a:xf:(operation(xf) <=> function(xf) & (cross_product(domain_of( 471%----domain_of(xf)),domain_of(domain_of(xf))) = domain_of(xf)) 472%----& (range_of(xf) < domain_of(domain_of(xf))). 473cnf(operation1,axiom, 474 ( ~ operation(Xf) 475 | function(Xf) )). 476 477cnf(operation2,axiom, 478 ( ~ operation(Xf) 479 | cross_product(domain_of(domain_of(Xf)),domain_of(domain_of(Xf))) = domain_of(Xf) )). 480 481cnf(operation3,axiom, 482 ( ~ operation(Xf) 483 | subclass(range_of(Xf),domain_of(domain_of(Xf))) )). 484 485cnf(operation4,axiom, 486 ( ~ function(Xf) 487 | cross_product(domain_of(domain_of(Xf)),domain_of(domain_of(Xf))) != domain_of(Xf) 488 | ~ subclass(range_of(Xf),domain_of(domain_of(Xf))) 489 | operation(Xf) )). 490 491%----Definition of compatible. 492%----a:xh:a:xf1:a:af2: (compatible(xh,xf1,xf2) <=> function(xh) 493%----& (domain_of(domain_of(xf1)) = domain_of(xh)) & (range_of(xh) 494%----< domain_of(domain_of(xf2)))). 495%----Singleton variables OK. 496cnf(compatible1,axiom, 497 ( ~ compatible(Xh,Xf1,Xf2) 498 | function(Xh) )). 499 500%----Singleton variables OK. 501cnf(compatible2,axiom, 502 ( ~ compatible(Xh,Xf1,Xf2) 503 | domain_of(domain_of(Xf1)) = domain_of(Xh) )). 504 505%----Singleton variables OK. 506cnf(compatible3,axiom, 507 ( ~ compatible(Xh,Xf1,Xf2) 508 | subclass(range_of(Xh),domain_of(domain_of(Xf2))) )). 509 510cnf(compatible4,axiom, 511 ( ~ function(Xh) 512 | domain_of(domain_of(Xf1)) != domain_of(Xh) 513 | ~ subclass(range_of(Xh),domain_of(domain_of(Xf2))) 514 | compatible(Xh,Xf1,Xf2) )). 515 516%----Definition of homomorphism. 517%----a:xh:a:xf1:a:xf2: (homomorphism(xh,xf1,xf2) <=> 518%---- operation(xf1) & operation(xf2) & compatible(xh,xf1,xf2) & 519%---- a:x:a:y:(([x,y] e domain_of(xf1)) ==> (((xf2 apply [(xh apply x), 520%----(xh apply y)]) = (xh apply (xf1 apply [x,y])))). 521%----Singleton variables OK. 522cnf(homomorphism1,axiom, 523 ( ~ homomorphism(Xh,Xf1,Xf2) 524 | operation(Xf1) )). 525 526%----Singleton variables OK. 527cnf(homomorphism2,axiom, 528 ( ~ homomorphism(Xh,Xf1,Xf2) 529 | operation(Xf2) )). 530 531cnf(homomorphism3,axiom, 532 ( ~ homomorphism(Xh,Xf1,Xf2) 533 | compatible(Xh,Xf1,Xf2) )). 534 535cnf(homomorphism4,axiom, 536 ( ~ homomorphism(Xh,Xf1,Xf2) 537 | ~ member(ordered_pair(X,Y),domain_of(Xf1)) 538 | apply(Xf2,ordered_pair(apply(Xh,X),apply(Xh,Y))) = apply(Xh,apply(Xf1,ordered_pair(X,Y))) )). 539 540cnf(homomorphism5,axiom, 541 ( ~ operation(Xf1) 542 | ~ operation(Xf2) 543 | ~ compatible(Xh,Xf1,Xf2) 544 | member(ordered_pair(not_homomorphism1(Xh,Xf1,Xf2),not_homomorphism2(Xh,Xf1,Xf2)),domain_of(Xf1)) 545 | homomorphism(Xh,Xf1,Xf2) )). 546 547cnf(homomorphism6,axiom, 548 ( ~ operation(Xf1) 549 | ~ operation(Xf2) 550 | ~ compatible(Xh,Xf1,Xf2) 551 | apply(Xf2,ordered_pair(apply(Xh,not_homomorphism1(Xh,Xf1,Xf2)),apply(Xh,not_homomorphism2(Xh,Xf1,Xf2)))) != apply(Xh,apply(Xf1,ordered_pair(not_homomorphism1(Xh,Xf1,Xf2),not_homomorphism2(Xh,Xf1,Xf2)))) 552 | homomorphism(Xh,Xf1,Xf2) )). 553 554%-------------------------------------------------------------------------- 555