# HG changeset patch # User berghofe # Date 1170868378 -3600 # Node ID bbc76be6efb49e0643910eb0a909c536efc688b3 # Parent 8d6d489f6ab36dc8e31cad45a37f99c5d19227ed Renamed member to memb to avoid confusion with member function defined in Predicate theory. diff -r 8d6d489f6ab3 -r bbc76be6efb4 src/HOL/ex/mesontest2.ML --- a/src/HOL/ex/mesontest2.ML Wed Feb 07 18:12:02 2007 +0100 +++ b/src/HOL/ex/mesontest2.ML Wed Feb 07 18:12:58 2007 +0100 @@ -1320,43 +1320,43 @@ meson_tac 1); val SET004_0_ax = - "(\\X U Y. subclass(X::'a,Y) & member(U::'a,X) --> member(U::'a,Y)) & \ -\ (\\X Y. member(not_subclass_element(X::'a,Y),X) | subclass(X::'a,Y)) & \ -\ (\\X Y. member(not_subclass_element(X::'a,Y),Y) --> subclass(X::'a,Y)) & \ + "(\\X U Y. subclass(X::'a,Y) & memb(U::'a,X) --> memb(U::'a,Y)) & \ +\ (\\X Y. memb(not_subclass_element(X::'a,Y),X) | subclass(X::'a,Y)) & \ +\ (\\X Y. memb(not_subclass_element(X::'a,Y),Y) --> subclass(X::'a,Y)) & \ \ (\\X. subclass(X::'a,universal_class)) & \ \ (\\X Y. equal(X::'a,Y) --> subclass(X::'a,Y)) & \ \ (\\Y X. equal(X::'a,Y) --> subclass(Y::'a,X)) & \ \ (\\X Y. subclass(X::'a,Y) & subclass(Y::'a,X) --> equal(X::'a,Y)) & \ -\ (\\X U Y. member(U::'a,unordered_pair(X::'a,Y)) --> equal(U::'a,X) | equal(U::'a,Y)) & \ -\ (\\X Y. member(X::'a,universal_class) --> member(X::'a,unordered_pair(X::'a,Y))) & \ -\ (\\X Y. member(Y::'a,universal_class) --> member(Y::'a,unordered_pair(X::'a,Y))) & \ -\ (\\X Y. member(unordered_pair(X::'a,Y),universal_class)) & \ +\ (\\X U Y. memb(U::'a,unordered_pair(X::'a,Y)) --> equal(U::'a,X) | equal(U::'a,Y)) & \ +\ (\\X Y. memb(X::'a,universal_class) --> memb(X::'a,unordered_pair(X::'a,Y))) & \ +\ (\\X Y. memb(Y::'a,universal_class) --> memb(Y::'a,unordered_pair(X::'a,Y))) & \ +\ (\\X Y. memb(unordered_pair(X::'a,Y),universal_class)) & \ \ (\\X. equal(unordered_pair(X::'a,X),singleton(X))) & \ \ (\\X Y. equal(unordered_pair(singleton(X),unordered_pair(X::'a,singleton(Y))),ordered_pair(X::'a,Y))) & \ -\ (\\V Y U X. member(ordered_pair(U::'a,V),cross_product(X::'a,Y)) --> member(U::'a,X)) & \ -\ (\\U X V Y. member(ordered_pair(U::'a,V),cross_product(X::'a,Y)) --> member(V::'a,Y)) & \ -\ (\\U V X Y. member(U::'a,X) & member(V::'a,Y) --> member(ordered_pair(U::'a,V),cross_product(X::'a,Y))) & \ -\ (\\X Y Z. member(Z::'a,cross_product(X::'a,Y)) --> equal(ordered_pair(first(Z),second(Z)),Z)) & \ +\ (\\V Y U X. memb(ordered_pair(U::'a,V),cross_product(X::'a,Y)) --> memb(U::'a,X)) & \ +\ (\\U X V Y. memb(ordered_pair(U::'a,V),cross_product(X::'a,Y)) --> memb(V::'a,Y)) & \ +\ (\\U V X Y. memb(U::'a,X) & memb(V::'a,Y) --> memb(ordered_pair(U::'a,V),cross_product(X::'a,Y))) & \ +\ (\\X Y Z. memb(Z::'a,cross_product(X::'a,Y)) --> equal(ordered_pair(first(Z),second(Z)),Z)) & \ \ (subclass(element_relation::'a,cross_product(universal_class::'a,universal_class))) & \ -\ (\\X Y. member(ordered_pair(X::'a,Y),element_relation) --> member(X::'a,Y)) & \ -\ (\\X Y. member(ordered_pair(X::'a,Y),cross_product(universal_class::'a,universal_class)) & member(X::'a,Y) --> member(ordered_pair(X::'a,Y),element_relation)) & \ -\ (\\Y Z X. member(Z::'a,intersection(X::'a,Y)) --> member(Z::'a,X)) & \ -\ (\\X Z Y. member(Z::'a,intersection(X::'a,Y)) --> member(Z::'a,Y)) & \ -\ (\\Z X Y. member(Z::'a,X) & member(Z::'a,Y) --> member(Z::'a,intersection(X::'a,Y))) & \ -\ (\\Z X. ~(member(Z::'a,complement(X)) & member(Z::'a,X))) & \ -\ (\\Z X. member(Z::'a,universal_class) --> member(Z::'a,complement(X)) | member(Z::'a,X)) & \ +\ (\\X Y. memb(ordered_pair(X::'a,Y),element_relation) --> memb(X::'a,Y)) & \ +\ (\\X Y. memb(ordered_pair(X::'a,Y),cross_product(universal_class::'a,universal_class)) & memb(X::'a,Y) --> memb(ordered_pair(X::'a,Y),element_relation)) & \ +\ (\\Y Z X. memb(Z::'a,intersection(X::'a,Y)) --> memb(Z::'a,X)) & \ +\ (\\X Z Y. memb(Z::'a,intersection(X::'a,Y)) --> memb(Z::'a,Y)) & \ +\ (\\Z X Y. memb(Z::'a,X) & memb(Z::'a,Y) --> memb(Z::'a,intersection(X::'a,Y))) & \ +\ (\\Z X. ~(memb(Z::'a,complement(X)) & memb(Z::'a,X))) & \ +\ (\\Z X. memb(Z::'a,universal_class) --> memb(Z::'a,complement(X)) | memb(Z::'a,X)) & \ \ (\\X Y. equal(complement(intersection(complement(X),complement(Y))),union(X::'a,Y))) & \ \ (\\X Y. equal(intersection(complement(intersection(X::'a,Y)),complement(intersection(complement(X),complement(Y)))),difference(X::'a,Y))) & \ \ (\\Xr X Y. equal(intersection(Xr::'a,cross_product(X::'a,Y)),restrct(Xr::'a,X,Y))) & \ \ (\\Xr X Y. equal(intersection(cross_product(X::'a,Y),Xr),restrct(Xr::'a,X,Y))) & \ -\ (\\Z X. ~(equal(restrct(X::'a,singleton(Z),universal_class),null_class) & member(Z::'a,domain_of(X)))) & \ -\ (\\Z X. member(Z::'a,universal_class) --> equal(restrct(X::'a,singleton(Z),universal_class),null_class) | member(Z::'a,domain_of(X))) & \ +\ (\\Z X. ~(equal(restrct(X::'a,singleton(Z),universal_class),null_class) & memb(Z::'a,domain_of(X)))) & \ +\ (\\Z X. memb(Z::'a,universal_class) --> equal(restrct(X::'a,singleton(Z),universal_class),null_class) | memb(Z::'a,domain_of(X))) & \ \ (\\X. subclass(rot(X),cross_product(cross_product(universal_class::'a,universal_class),universal_class))) & \ -\ (\\V W U X. member(ordered_pair(ordered_pair(U::'a,V),W),rot(X)) --> member(ordered_pair(ordered_pair(V::'a,W),U),X)) & \ -\ (\\U V W X. member(ordered_pair(ordered_pair(V::'a,W),U),X) & member(ordered_pair(ordered_pair(U::'a,V),W),cross_product(cross_product(universal_class::'a,universal_class),universal_class)) --> member(ordered_pair(ordered_pair(U::'a,V),W),rot(X))) & \ +\ (\\V W U X. memb(ordered_pair(ordered_pair(U::'a,V),W),rot(X)) --> memb(ordered_pair(ordered_pair(V::'a,W),U),X)) & \ +\ (\\U V W X. memb(ordered_pair(ordered_pair(V::'a,W),U),X) & memb(ordered_pair(ordered_pair(U::'a,V),W),cross_product(cross_product(universal_class::'a,universal_class),universal_class)) --> memb(ordered_pair(ordered_pair(U::'a,V),W),rot(X))) & \ \ (\\X. subclass(flip(X),cross_product(cross_product(universal_class::'a,universal_class),universal_class))) & \ -\ (\\V U W X. member(ordered_pair(ordered_pair(U::'a,V),W),flip(X)) --> member(ordered_pair(ordered_pair(V::'a,U),W),X)) & \ -\ (\\U V W X. member(ordered_pair(ordered_pair(V::'a,U),W),X) & member(ordered_pair(ordered_pair(U::'a,V),W),cross_product(cross_product(universal_class::'a,universal_class),universal_class)) --> member(ordered_pair(ordered_pair(U::'a,V),W),flip(X))) & \ +\ (\\V U W X. memb(ordered_pair(ordered_pair(U::'a,V),W),flip(X)) --> memb(ordered_pair(ordered_pair(V::'a,U),W),X)) & \ +\ (\\U V W X. memb(ordered_pair(ordered_pair(V::'a,U),W),X) & memb(ordered_pair(ordered_pair(U::'a,V),W),cross_product(cross_product(universal_class::'a,universal_class),universal_class)) --> memb(ordered_pair(ordered_pair(U::'a,V),W),flip(X))) & \ \ (\\Y. equal(domain_of(flip(cross_product(Y::'a,universal_class))),INVERSE(Y))) & \ \ (\\Z. equal(domain_of(INVERSE(Z)),range_of(Z))) & \ \ (\\Z X Y. equal(first(not_subclass_element(restrct(Z::'a,X,singleton(Y)),null_class)),domain(Z::'a,X,Y))) & \ @@ -1364,32 +1364,32 @@ \ (\\Xr X. equal(range_of(restrct(Xr::'a,X,universal_class)),image_(Xr::'a,X))) & \ \ (\\X. equal(union(X::'a,singleton(X)),successor(X))) & \ \ (subclass(successor_relation::'a,cross_product(universal_class::'a,universal_class))) & \ -\ (\\X Y. member(ordered_pair(X::'a,Y),successor_relation) --> equal(successor(X),Y)) & \ -\ (\\X Y. equal(successor(X),Y) & member(ordered_pair(X::'a,Y),cross_product(universal_class::'a,universal_class)) --> member(ordered_pair(X::'a,Y),successor_relation)) & \ -\ (\\X. inductive(X) --> member(null_class::'a,X)) & \ +\ (\\X Y. memb(ordered_pair(X::'a,Y),successor_relation) --> equal(successor(X),Y)) & \ +\ (\\X Y. equal(successor(X),Y) & memb(ordered_pair(X::'a,Y),cross_product(universal_class::'a,universal_class)) --> memb(ordered_pair(X::'a,Y),successor_relation)) & \ +\ (\\X. inductive(X) --> memb(null_class::'a,X)) & \ \ (\\X. inductive(X) --> subclass(image_(successor_relation::'a,X),X)) & \ -\ (\\X. member(null_class::'a,X) & subclass(image_(successor_relation::'a,X),X) --> inductive(X)) & \ +\ (\\X. memb(null_class::'a,X) & subclass(image_(successor_relation::'a,X),X) --> inductive(X)) & \ \ (inductive(omega)) & \ \ (\\Y. inductive(Y) --> subclass(omega::'a,Y)) & \ -\ (member(omega::'a,universal_class)) & \ +\ (memb(omega::'a,universal_class)) & \ \ (\\X. equal(domain_of(restrct(element_relation::'a,universal_class,X)),sum_class(X))) & \ -\ (\\X. member(X::'a,universal_class) --> member(sum_class(X),universal_class)) & \ +\ (\\X. memb(X::'a,universal_class) --> memb(sum_class(X),universal_class)) & \ \ (\\X. equal(complement(image_(element_relation::'a,complement(X))),powerClass(X))) & \ -\ (\\U. member(U::'a,universal_class) --> member(powerClass(U),universal_class)) & \ +\ (\\U. memb(U::'a,universal_class) --> memb(powerClass(U),universal_class)) & \ \ (\\Yr Xr. subclass(compos(Yr::'a,Xr),cross_product(universal_class::'a,universal_class))) & \ -\ (\\Z Yr Xr Y. member(ordered_pair(Y::'a,Z),compos(Yr::'a,Xr)) --> member(Z::'a,image_(Yr::'a,image_(Xr::'a,singleton(Y))))) & \ -\ (\\Y Z Yr Xr. member(Z::'a,image_(Yr::'a,image_(Xr::'a,singleton(Y)))) & member(ordered_pair(Y::'a,Z),cross_product(universal_class::'a,universal_class)) --> member(ordered_pair(Y::'a,Z),compos(Yr::'a,Xr))) & \ +\ (\\Z Yr Xr Y. memb(ordered_pair(Y::'a,Z),compos(Yr::'a,Xr)) --> memb(Z::'a,image_(Yr::'a,image_(Xr::'a,singleton(Y))))) & \ +\ (\\Y Z Yr Xr. memb(Z::'a,image_(Yr::'a,image_(Xr::'a,singleton(Y)))) & memb(ordered_pair(Y::'a,Z),cross_product(universal_class::'a,universal_class)) --> memb(ordered_pair(Y::'a,Z),compos(Yr::'a,Xr))) & \ \ (\\X. single_valued_class(X) --> subclass(compos(X::'a,INVERSE(X)),identity_relation)) & \ \ (\\X. subclass(compos(X::'a,INVERSE(X)),identity_relation) --> single_valued_class(X)) & \ \ (\\Xf. function(Xf) --> subclass(Xf::'a,cross_product(universal_class::'a,universal_class))) & \ \ (\\Xf. function(Xf) --> subclass(compos(Xf::'a,INVERSE(Xf)),identity_relation)) & \ \ (\\Xf. subclass(Xf::'a,cross_product(universal_class::'a,universal_class)) & subclass(compos(Xf::'a,INVERSE(Xf)),identity_relation) --> function(Xf)) & \ -\ (\\Xf X. function(Xf) & member(X::'a,universal_class) --> member(image_(Xf::'a,X),universal_class)) & \ -\ (\\X. equal(X::'a,null_class) | member(regular(X),X)) & \ +\ (\\Xf X. function(Xf) & memb(X::'a,universal_class) --> memb(image_(Xf::'a,X),universal_class)) & \ +\ (\\X. equal(X::'a,null_class) | memb(regular(X),X)) & \ \ (\\X. equal(X::'a,null_class) | equal(intersection(X::'a,regular(X)),null_class)) & \ \ (\\Xf Y. equal(sum_class(image_(Xf::'a,singleton(Y))),apply(Xf::'a,Y))) & \ \ (function(choice)) & \ -\ (\\Y. member(Y::'a,universal_class) --> equal(Y::'a,null_class) | member(apply(choice::'a,Y),Y)) & \ +\ (\\Y. memb(Y::'a,universal_class) --> equal(Y::'a,null_class) | memb(apply(choice::'a,Y),Y)) & \ \ (\\Xf. one_to_one(Xf) --> function(Xf)) & \ \ (\\Xf. one_to_one(Xf) --> function(INVERSE(Xf))) & \ \ (\\Xf. function(INVERSE(Xf)) & function(Xf) --> one_to_one(Xf)) & \ @@ -1408,8 +1408,8 @@ \ (\\Xh Xf2 Xf1. homomorphism(Xh::'a,Xf1,Xf2) --> operation(Xf1)) & \ \ (\\Xh Xf1 Xf2. homomorphism(Xh::'a,Xf1,Xf2) --> operation(Xf2)) & \ \ (\\Xh Xf1 Xf2. homomorphism(Xh::'a,Xf1,Xf2) --> compatible(Xh::'a,Xf1,Xf2)) & \ -\ (\\Xf2 Xh Xf1 X Y. homomorphism(Xh::'a,Xf1,Xf2) & member(ordered_pair(X::'a,Y),domain_of(Xf1)) --> equal(apply(Xf2::'a,ordered_pair(apply(Xh::'a,X),apply(Xh::'a,Y))),apply(Xh::'a,apply(Xf1::'a,ordered_pair(X::'a,Y))))) & \ -\ (\\Xh Xf1 Xf2. operation(Xf1) & operation(Xf2) & compatible(Xh::'a,Xf1,Xf2) --> member(ordered_pair(not_homomorphism1(Xh::'a,Xf1,Xf2),not_homomorphism2(Xh::'a,Xf1,Xf2)),domain_of(Xf1)) | homomorphism(Xh::'a,Xf1,Xf2)) & \ +\ (\\Xf2 Xh Xf1 X Y. homomorphism(Xh::'a,Xf1,Xf2) & memb(ordered_pair(X::'a,Y),domain_of(Xf1)) --> equal(apply(Xf2::'a,ordered_pair(apply(Xh::'a,X),apply(Xh::'a,Y))),apply(Xh::'a,apply(Xf1::'a,ordered_pair(X::'a,Y))))) & \ +\ (\\Xh Xf1 Xf2. operation(Xf1) & operation(Xf2) & compatible(Xh::'a,Xf1,Xf2) --> memb(ordered_pair(not_homomorphism1(Xh::'a,Xf1,Xf2),not_homomorphism2(Xh::'a,Xf1,Xf2)),domain_of(Xf1)) | homomorphism(Xh::'a,Xf1,Xf2)) & \ \ (\\Xh Xf1 Xf2. operation(Xf1) & operation(Xf2) & compatible(Xh::'a,Xf1,Xf2) & equal(apply(Xf2::'a,ordered_pair(apply(Xh::'a,not_homomorphism1(Xh::'a,Xf1,Xf2)),apply(Xh::'a,not_homomorphism2(Xh::'a,Xf1,Xf2)))),apply(Xh::'a,apply(Xf1::'a,ordered_pair(not_homomorphism1(Xh::'a,Xf1,Xf2),not_homomorphism2(Xh::'a,Xf1,Xf2))))) --> homomorphism(Xh::'a,Xf1,Xf2))"; val SET004_0_eq = @@ -1471,8 +1471,8 @@ \ (\\P6 R6 Q6 S6. equal(P6::'a,Q6) & homomorphism(R6::'a,P6,S6) --> homomorphism(R6::'a,Q6,S6)) & \ \ (\\T6 V6 W6 U6. equal(T6::'a,U6) & homomorphism(V6::'a,W6,T6) --> homomorphism(V6::'a,W6,U6)) & \ \ (\\X6 Y6. equal(X6::'a,Y6) & inductive(X6) --> inductive(Y6)) & \ -\ (\\Z6 A7 B7. equal(Z6::'a,A7) & member(Z6::'a,B7) --> member(A7::'a,B7)) & \ -\ (\\C7 E7 D7. equal(C7::'a,D7) & member(E7::'a,C7) --> member(E7::'a,D7)) & \ +\ (\\Z6 A7 B7. equal(Z6::'a,A7) & memb(Z6::'a,B7) --> memb(A7::'a,B7)) & \ +\ (\\C7 E7 D7. equal(C7::'a,D7) & memb(E7::'a,C7) --> memb(E7::'a,D7)) & \ \ (\\F7 G7. equal(F7::'a,G7) & one_to_one(F7) --> one_to_one(G7)) & \ \ (\\H7 I7. equal(H7::'a,I7) & operation(H7) --> operation(I7)) & \ \ (\\J7 K7. equal(J7::'a,K7) & single_valued_class(J7) --> single_valued_class(K7)) & \ @@ -1481,22 +1481,22 @@ val SET004_1_ax = "(\\X. subclass(compose_class(X),cross_product(universal_class::'a,universal_class))) & \ -\ (\\X Y Z. member(ordered_pair(Y::'a,Z),compose_class(X)) --> equal(compos(X::'a,Y),Z)) & \ -\ (\\Y Z X. member(ordered_pair(Y::'a,Z),cross_product(universal_class::'a,universal_class)) & equal(compos(X::'a,Y),Z) --> member(ordered_pair(Y::'a,Z),compose_class(X))) & \ +\ (\\X Y Z. memb(ordered_pair(Y::'a,Z),compose_class(X)) --> equal(compos(X::'a,Y),Z)) & \ +\ (\\Y Z X. memb(ordered_pair(Y::'a,Z),cross_product(universal_class::'a,universal_class)) & equal(compos(X::'a,Y),Z) --> memb(ordered_pair(Y::'a,Z),compose_class(X))) & \ \ (subclass(composition_function::'a,cross_product(universal_class::'a,cross_product(universal_class::'a,universal_class)))) & \ -\ (\\X Y Z. member(ordered_pair(X::'a,ordered_pair(Y::'a,Z)),composition_function) --> equal(compos(X::'a,Y),Z)) & \ -\ (\\X Y. member(ordered_pair(X::'a,Y),cross_product(universal_class::'a,universal_class)) --> member(ordered_pair(X::'a,ordered_pair(Y::'a,compos(X::'a,Y))),composition_function)) & \ +\ (\\X Y Z. memb(ordered_pair(X::'a,ordered_pair(Y::'a,Z)),composition_function) --> equal(compos(X::'a,Y),Z)) & \ +\ (\\X Y. memb(ordered_pair(X::'a,Y),cross_product(universal_class::'a,universal_class)) --> memb(ordered_pair(X::'a,ordered_pair(Y::'a,compos(X::'a,Y))),composition_function)) & \ \ (subclass(domain_relation::'a,cross_product(universal_class::'a,universal_class))) & \ -\ (\\X Y. member(ordered_pair(X::'a,Y),domain_relation) --> equal(domain_of(X),Y)) & \ -\ (\\X. member(X::'a,universal_class) --> member(ordered_pair(X::'a,domain_of(X)),domain_relation)) & \ +\ (\\X Y. memb(ordered_pair(X::'a,Y),domain_relation) --> equal(domain_of(X),Y)) & \ +\ (\\X. memb(X::'a,universal_class) --> memb(ordered_pair(X::'a,domain_of(X)),domain_relation)) & \ \ (\\X. equal(first(not_subclass_element(compos(X::'a,INVERSE(X)),identity_relation)),single_valued1(X))) & \ \ (\\X. equal(second(not_subclass_element(compos(X::'a,INVERSE(X)),identity_relation)),single_valued2(X))) & \ \ (\\X. equal(domain(X::'a,image_(INVERSE(X),singleton(single_valued1(X))),single_valued2(X)),single_valued3(X))) & \ \ (equal(intersection(complement(compos(element_relation::'a,complement(identity_relation))),element_relation),singleton_relation)) & \ \ (subclass(application_function::'a,cross_product(universal_class::'a,cross_product(universal_class::'a,universal_class)))) & \ -\ (\\Z Y X. member(ordered_pair(X::'a,ordered_pair(Y::'a,Z)),application_function) --> member(Y::'a,domain_of(X))) & \ -\ (\\X Y Z. member(ordered_pair(X::'a,ordered_pair(Y::'a,Z)),application_function) --> equal(apply(X::'a,Y),Z)) & \ -\ (\\Z X Y. member(ordered_pair(X::'a,ordered_pair(Y::'a,Z)),cross_product(universal_class::'a,cross_product(universal_class::'a,universal_class))) & member(Y::'a,domain_of(X)) --> member(ordered_pair(X::'a,ordered_pair(Y::'a,apply(X::'a,Y))),application_function)) & \ +\ (\\Z Y X. memb(ordered_pair(X::'a,ordered_pair(Y::'a,Z)),application_function) --> memb(Y::'a,domain_of(X))) & \ +\ (\\X Y Z. memb(ordered_pair(X::'a,ordered_pair(Y::'a,Z)),application_function) --> equal(apply(X::'a,Y),Z)) & \ +\ (\\Z X Y. memb(ordered_pair(X::'a,ordered_pair(Y::'a,Z)),cross_product(universal_class::'a,cross_product(universal_class::'a,universal_class))) & memb(Y::'a,domain_of(X)) --> memb(ordered_pair(X::'a,ordered_pair(Y::'a,apply(X::'a,Y))),application_function)) & \ \ (\\X Y Xf. maps(Xf::'a,X,Y) --> function(Xf)) & \ \ (\\Y Xf X. maps(Xf::'a,X,Y) --> equal(domain_of(Xf),X)) & \ \ (\\X Xf Y. maps(Xf::'a,X,Y) --> subclass(range_of(Xf),Y)) & \ @@ -1523,41 +1523,41 @@ \ (\\Xr Y. equal(restrct(intersection(Xr::'a,INVERSE(Xr)),Y,Y),null_class) --> asymmetric(Xr::'a,Y)) & \ \ (\\Xr Y Z. equal(segment(Xr::'a,Y,Z),domain_of(restrct(Xr::'a,Y,singleton(Z))))) & \ \ (\\X Y. well_ordering(X::'a,Y) --> connected(X::'a,Y)) & \ -\ (\\Y Xr U. well_ordering(Xr::'a,Y) & subclass(U::'a,Y) --> equal(U::'a,null_class) | member(least(Xr::'a,U),U)) & \ -\ (\\Y V Xr U. well_ordering(Xr::'a,Y) & subclass(U::'a,Y) & member(V::'a,U) --> member(least(Xr::'a,U),U)) & \ +\ (\\Y Xr U. well_ordering(Xr::'a,Y) & subclass(U::'a,Y) --> equal(U::'a,null_class) | memb(least(Xr::'a,U),U)) & \ +\ (\\Y V Xr U. well_ordering(Xr::'a,Y) & subclass(U::'a,Y) & memb(V::'a,U) --> memb(least(Xr::'a,U),U)) & \ \ (\\Y Xr U. well_ordering(Xr::'a,Y) & subclass(U::'a,Y) --> equal(segment(Xr::'a,U,least(Xr::'a,U)),null_class)) & \ -\ (\\Y V U Xr. ~(well_ordering(Xr::'a,Y) & subclass(U::'a,Y) & member(V::'a,U) & member(ordered_pair(V::'a,least(Xr::'a,U)),Xr))) & \ +\ (\\Y V U Xr. ~(well_ordering(Xr::'a,Y) & subclass(U::'a,Y) & memb(V::'a,U) & memb(ordered_pair(V::'a,least(Xr::'a,U)),Xr))) & \ \ (\\Xr Y. connected(Xr::'a,Y) & equal(not_well_ordering(Xr::'a,Y),null_class) --> well_ordering(Xr::'a,Y)) & \ \ (\\Xr Y. connected(Xr::'a,Y) --> subclass(not_well_ordering(Xr::'a,Y),Y) | well_ordering(Xr::'a,Y)) & \ -\ (\\V Xr Y. member(V::'a,not_well_ordering(Xr::'a,Y)) & equal(segment(Xr::'a,not_well_ordering(Xr::'a,Y),V),null_class) & connected(Xr::'a,Y) --> well_ordering(Xr::'a,Y)) & \ +\ (\\V Xr Y. memb(V::'a,not_well_ordering(Xr::'a,Y)) & equal(segment(Xr::'a,not_well_ordering(Xr::'a,Y),V),null_class) & connected(Xr::'a,Y) --> well_ordering(Xr::'a,Y)) & \ \ (\\Xr Y Z. section(Xr::'a,Y,Z) --> subclass(Y::'a,Z)) & \ \ (\\Xr Z Y. section(Xr::'a,Y,Z) --> subclass(domain_of(restrct(Xr::'a,Z,Y)),Y)) & \ \ (\\Xr Y Z. subclass(Y::'a,Z) & subclass(domain_of(restrct(Xr::'a,Z,Y)),Y) --> section(Xr::'a,Y,Z)) & \ -\ (\\X. member(X::'a,ordinal_numbers) --> well_ordering(element_relation::'a,X)) & \ -\ (\\X. member(X::'a,ordinal_numbers) --> subclass(sum_class(X),X)) & \ -\ (\\X. well_ordering(element_relation::'a,X) & subclass(sum_class(X),X) & member(X::'a,universal_class) --> member(X::'a,ordinal_numbers)) & \ -\ (\\X. well_ordering(element_relation::'a,X) & subclass(sum_class(X),X) --> member(X::'a,ordinal_numbers) | equal(X::'a,ordinal_numbers)) & \ +\ (\\X. memb(X::'a,ordinal_numbers) --> well_ordering(element_relation::'a,X)) & \ +\ (\\X. memb(X::'a,ordinal_numbers) --> subclass(sum_class(X),X)) & \ +\ (\\X. well_ordering(element_relation::'a,X) & subclass(sum_class(X),X) & memb(X::'a,universal_class) --> memb(X::'a,ordinal_numbers)) & \ +\ (\\X. well_ordering(element_relation::'a,X) & subclass(sum_class(X),X) --> memb(X::'a,ordinal_numbers) | equal(X::'a,ordinal_numbers)) & \ \ (equal(union(singleton(null_class),image_(successor_relation::'a,ordinal_numbers)),kind_1_ordinals)) & \ \ (equal(intersection(complement(kind_1_ordinals),ordinal_numbers),limit_ordinals)) & \ \ (\\X. subclass(rest_of(X),cross_product(universal_class::'a,universal_class))) & \ -\ (\\V U X. member(ordered_pair(U::'a,V),rest_of(X)) --> member(U::'a,domain_of(X))) & \ -\ (\\X U V. member(ordered_pair(U::'a,V),rest_of(X)) --> equal(restrct(X::'a,U,universal_class),V)) & \ -\ (\\U V X. member(U::'a,domain_of(X)) & equal(restrct(X::'a,U,universal_class),V) --> member(ordered_pair(U::'a,V),rest_of(X))) & \ +\ (\\V U X. memb(ordered_pair(U::'a,V),rest_of(X)) --> memb(U::'a,domain_of(X))) & \ +\ (\\X U V. memb(ordered_pair(U::'a,V),rest_of(X)) --> equal(restrct(X::'a,U,universal_class),V)) & \ +\ (\\U V X. memb(U::'a,domain_of(X)) & equal(restrct(X::'a,U,universal_class),V) --> memb(ordered_pair(U::'a,V),rest_of(X))) & \ \ (subclass(rest_relation::'a,cross_product(universal_class::'a,universal_class))) & \ -\ (\\X Y. member(ordered_pair(X::'a,Y),rest_relation) --> equal(rest_of(X),Y)) & \ -\ (\\X. member(X::'a,universal_class) --> member(ordered_pair(X::'a,rest_of(X)),rest_relation)) & \ -\ (\\X Z. member(X::'a,recursion_equation_functions(Z)) --> function(Z)) & \ -\ (\\Z X. member(X::'a,recursion_equation_functions(Z)) --> function(X)) & \ -\ (\\Z X. member(X::'a,recursion_equation_functions(Z)) --> member(domain_of(X),ordinal_numbers)) & \ -\ (\\Z X. member(X::'a,recursion_equation_functions(Z)) --> equal(compos(Z::'a,rest_of(X)),X)) & \ -\ (\\X Z. function(Z) & function(X) & member(domain_of(X),ordinal_numbers) & equal(compos(Z::'a,rest_of(X)),X) --> member(X::'a,recursion_equation_functions(Z))) & \ +\ (\\X Y. memb(ordered_pair(X::'a,Y),rest_relation) --> equal(rest_of(X),Y)) & \ +\ (\\X. memb(X::'a,universal_class) --> memb(ordered_pair(X::'a,rest_of(X)),rest_relation)) & \ +\ (\\X Z. memb(X::'a,recursion_equation_functions(Z)) --> function(Z)) & \ +\ (\\Z X. memb(X::'a,recursion_equation_functions(Z)) --> function(X)) & \ +\ (\\Z X. memb(X::'a,recursion_equation_functions(Z)) --> memb(domain_of(X),ordinal_numbers)) & \ +\ (\\Z X. memb(X::'a,recursion_equation_functions(Z)) --> equal(compos(Z::'a,rest_of(X)),X)) & \ +\ (\\X Z. function(Z) & function(X) & memb(domain_of(X),ordinal_numbers) & equal(compos(Z::'a,rest_of(X)),X) --> memb(X::'a,recursion_equation_functions(Z))) & \ \ (subclass(union_of_range_map::'a,cross_product(universal_class::'a,universal_class))) & \ -\ (\\X Y. member(ordered_pair(X::'a,Y),union_of_range_map) --> equal(sum_class(range_of(X)),Y)) & \ -\ (\\X Y. member(ordered_pair(X::'a,Y),cross_product(universal_class::'a,universal_class)) & equal(sum_class(range_of(X)),Y) --> member(ordered_pair(X::'a,Y),union_of_range_map)) & \ +\ (\\X Y. memb(ordered_pair(X::'a,Y),union_of_range_map) --> equal(sum_class(range_of(X)),Y)) & \ +\ (\\X Y. memb(ordered_pair(X::'a,Y),cross_product(universal_class::'a,universal_class)) & equal(sum_class(range_of(X)),Y) --> memb(ordered_pair(X::'a,Y),union_of_range_map)) & \ \ (\\X Y. equal(apply(recursion(X::'a,successor_relation,union_of_range_map),Y),ordinal_add(X::'a,Y))) & \ \ (\\X Y. equal(recursion(null_class::'a,apply(add_relation::'a,X),union_of_range_map),ordinal_multiply(X::'a,Y))) & \ -\ (\\X. member(X::'a,omega) --> equal(integer_of(X),X)) & \ -\ (\\X. member(X::'a,omega) | equal(integer_of(X),null_class))"; +\ (\\X. memb(X::'a,omega) --> equal(integer_of(X),X)) & \ +\ (\\X. memb(X::'a,omega) | equal(integer_of(X),null_class))"; val NUM004_0_eq = "(\\D E. equal(D::'a,E) --> equal(integer_of(D),integer_of(E))) & \ @@ -2191,18 +2191,18 @@ (*35532 inferences so far. Searching to depth 19. 54.3 secs*) val SET005_1 = prove_hard - ("(\\Subset Element Superset. member(Element::'a,Subset) & subset(Subset::'a,Superset) --> member(Element::'a,Superset)) & \ -\ (\\Superset Subset. subset(Subset::'a,Superset) | member(member_of_1_not_of_2(Subset::'a,Superset),Subset)) & \ -\ (\\Subset Superset. member(member_of_1_not_of_2(Subset::'a,Superset),Superset) --> subset(Subset::'a,Superset)) & \ + ("(\\Subset Element Superset. memb(Element::'a,Subset) & subset(Subset::'a,Superset) --> memb(Element::'a,Superset)) & \ +\ (\\Superset Subset. subset(Subset::'a,Superset) | memb(member_of_1_not_of_2(Subset::'a,Superset),Subset)) & \ +\ (\\Subset Superset. memb(member_of_1_not_of_2(Subset::'a,Superset),Superset) --> subset(Subset::'a,Superset)) & \ \ (\\Subset Superset. equal_sets(Subset::'a,Superset) --> subset(Subset::'a,Superset)) & \ \ (\\Subset Superset. equal_sets(Superset::'a,Subset) --> subset(Subset::'a,Superset)) & \ \ (\\Set2 Set1. subset(Set1::'a,Set2) & subset(Set2::'a,Set1) --> equal_sets(Set2::'a,Set1)) & \ -\ (\\Set2 Intersection Element Set1. intersection(Set1::'a,Set2,Intersection) & member(Element::'a,Intersection) --> member(Element::'a,Set1)) & \ -\ (\\Set1 Intersection Element Set2. intersection(Set1::'a,Set2,Intersection) & member(Element::'a,Intersection) --> member(Element::'a,Set2)) & \ -\ (\\Set2 Set1 Element Intersection. intersection(Set1::'a,Set2,Intersection) & member(Element::'a,Set2) & member(Element::'a,Set1) --> member(Element::'a,Intersection)) & \ -\ (\\Set2 Intersection Set1. member(h(Set1::'a,Set2,Intersection),Intersection) | intersection(Set1::'a,Set2,Intersection) | member(h(Set1::'a,Set2,Intersection),Set1)) & \ -\ (\\Set1 Intersection Set2. member(h(Set1::'a,Set2,Intersection),Intersection) | intersection(Set1::'a,Set2,Intersection) | member(h(Set1::'a,Set2,Intersection),Set2)) & \ -\ (\\Set1 Set2 Intersection. member(h(Set1::'a,Set2,Intersection),Intersection) & member(h(Set1::'a,Set2,Intersection),Set2) & member(h(Set1::'a,Set2,Intersection),Set1) --> intersection(Set1::'a,Set2,Intersection)) & \ +\ (\\Set2 Intersection Element Set1. intersection(Set1::'a,Set2,Intersection) & memb(Element::'a,Intersection) --> memb(Element::'a,Set1)) & \ +\ (\\Set1 Intersection Element Set2. intersection(Set1::'a,Set2,Intersection) & memb(Element::'a,Intersection) --> memb(Element::'a,Set2)) & \ +\ (\\Set2 Set1 Element Intersection. intersection(Set1::'a,Set2,Intersection) & memb(Element::'a,Set2) & memb(Element::'a,Set1) --> memb(Element::'a,Intersection)) & \ +\ (\\Set2 Intersection Set1. memb(h(Set1::'a,Set2,Intersection),Intersection) | intersection(Set1::'a,Set2,Intersection) | memb(h(Set1::'a,Set2,Intersection),Set1)) & \ +\ (\\Set1 Intersection Set2. memb(h(Set1::'a,Set2,Intersection),Intersection) | intersection(Set1::'a,Set2,Intersection) | memb(h(Set1::'a,Set2,Intersection),Set2)) & \ +\ (\\Set1 Set2 Intersection. memb(h(Set1::'a,Set2,Intersection),Intersection) & memb(h(Set1::'a,Set2,Intersection),Set2) & memb(h(Set1::'a,Set2,Intersection),Set1) --> intersection(Set1::'a,Set2,Intersection)) & \ \ (intersection(a::'a,b,aIb)) & \ \ (intersection(b::'a,c,bIc)) & \ \ (intersection(a::'a,bIc,aIbIc)) & \ @@ -2212,18 +2212,18 @@ (*6450 inferences so far. Searching to depth 14. 4.2 secs*) val SET009_1 = prove - ("(\\Subset Element Superset. member(Element::'a,Subset) & ssubset(Subset::'a,Superset) --> member(Element::'a,Superset)) & \ -\ (\\Superset Subset. ssubset(Subset::'a,Superset) | member(member_of_1_not_of_2(Subset::'a,Superset),Subset)) & \ -\ (\\Subset Superset. member(member_of_1_not_of_2(Subset::'a,Superset),Superset) --> ssubset(Subset::'a,Superset)) & \ + ("(\\Subset Element Superset. memb(Element::'a,Subset) & ssubset(Subset::'a,Superset) --> memb(Element::'a,Superset)) & \ +\ (\\Superset Subset. ssubset(Subset::'a,Superset) | memb(member_of_1_not_of_2(Subset::'a,Superset),Subset)) & \ +\ (\\Subset Superset. memb(member_of_1_not_of_2(Subset::'a,Superset),Superset) --> ssubset(Subset::'a,Superset)) & \ \ (\\Subset Superset. equal_sets(Subset::'a,Superset) --> ssubset(Subset::'a,Superset)) & \ \ (\\Subset Superset. equal_sets(Superset::'a,Subset) --> ssubset(Subset::'a,Superset)) & \ \ (\\Set2 Set1. ssubset(Set1::'a,Set2) & ssubset(Set2::'a,Set1) --> equal_sets(Set2::'a,Set1)) & \ -\ (\\Set2 Difference Element Set1. difference(Set1::'a,Set2,Difference) & member(Element::'a,Difference) --> member(Element::'a,Set1)) & \ -\ (\\Element A_set Set1 Set2. ~(member(Element::'a,Set1) & member(Element::'a,Set2) & difference(A_set::'a,Set1,Set2))) & \ -\ (\\Set1 Difference Element Set2. member(Element::'a,Set1) & difference(Set1::'a,Set2,Difference) --> member(Element::'a,Difference) | member(Element::'a,Set2)) & \ -\ (\\Set1 Set2 Difference. difference(Set1::'a,Set2,Difference) | member(k(Set1::'a,Set2,Difference),Set1) | member(k(Set1::'a,Set2,Difference),Difference)) & \ -\ (\\Set1 Set2 Difference. member(k(Set1::'a,Set2,Difference),Set2) --> member(k(Set1::'a,Set2,Difference),Difference) | difference(Set1::'a,Set2,Difference)) & \ -\ (\\Set1 Set2 Difference. member(k(Set1::'a,Set2,Difference),Difference) & member(k(Set1::'a,Set2,Difference),Set1) --> member(k(Set1::'a,Set2,Difference),Set2) | difference(Set1::'a,Set2,Difference)) & \ +\ (\\Set2 Difference Element Set1. difference(Set1::'a,Set2,Difference) & memb(Element::'a,Difference) --> memb(Element::'a,Set1)) & \ +\ (\\Element A_set Set1 Set2. ~(memb(Element::'a,Set1) & memb(Element::'a,Set2) & difference(A_set::'a,Set1,Set2))) & \ +\ (\\Set1 Difference Element Set2. memb(Element::'a,Set1) & difference(Set1::'a,Set2,Difference) --> memb(Element::'a,Difference) | memb(Element::'a,Set2)) & \ +\ (\\Set1 Set2 Difference. difference(Set1::'a,Set2,Difference) | memb(k(Set1::'a,Set2,Difference),Set1) | memb(k(Set1::'a,Set2,Difference),Difference)) & \ +\ (\\Set1 Set2 Difference. memb(k(Set1::'a,Set2,Difference),Set2) --> memb(k(Set1::'a,Set2,Difference),Difference) | difference(Set1::'a,Set2,Difference)) & \ +\ (\\Set1 Set2 Difference. memb(k(Set1::'a,Set2,Difference),Difference) & memb(k(Set1::'a,Set2,Difference),Set1) --> memb(k(Set1::'a,Set2,Difference),Set2) | difference(Set1::'a,Set2,Difference)) & \ \ (ssubset(d::'a,a)) & \ \ (difference(b::'a,a,bDa)) & \ \ (difference(b::'a,d,bDd)) & \ @@ -2233,13 +2233,13 @@ (*34726 inferences so far. Searching to depth 6. 2420 secs: 40 mins! BIG*) val SET025_4 = prove_hard (EQU001_0_ax ^ " & \ -\ (\\Y X. member(X::'a,Y) --> little_set(X)) & \ +\ (\\Y X. memb(X::'a,Y) --> little_set(X)) & \ \ (\\X Y. little_set(f1(X::'a,Y)) | equal(X::'a,Y)) & \ -\ (\\X Y. member(f1(X::'a,Y),X) | member(f1(X::'a,Y),Y) | equal(X::'a,Y)) & \ -\ (\\X Y. member(f1(X::'a,Y),X) & member(f1(X::'a,Y),Y) --> equal(X::'a,Y)) & \ -\ (\\X U Y. member(U::'a,non_ordered_pair(X::'a,Y)) --> equal(U::'a,X) | equal(U::'a,Y)) & \ -\ (\\Y U X. little_set(U) & equal(U::'a,X) --> member(U::'a,non_ordered_pair(X::'a,Y))) & \ -\ (\\X U Y. little_set(U) & equal(U::'a,Y) --> member(U::'a,non_ordered_pair(X::'a,Y))) & \ +\ (\\X Y. memb(f1(X::'a,Y),X) | memb(f1(X::'a,Y),Y) | equal(X::'a,Y)) & \ +\ (\\X Y. memb(f1(X::'a,Y),X) & memb(f1(X::'a,Y),Y) --> equal(X::'a,Y)) & \ +\ (\\X U Y. memb(U::'a,non_ordered_pair(X::'a,Y)) --> equal(U::'a,X) | equal(U::'a,Y)) & \ +\ (\\Y U X. little_set(U) & equal(U::'a,X) --> memb(U::'a,non_ordered_pair(X::'a,Y))) & \ +\ (\\X U Y. little_set(U) & equal(U::'a,Y) --> memb(U::'a,non_ordered_pair(X::'a,Y))) & \ \ (\\X Y. little_set(non_ordered_pair(X::'a,Y))) & \ \ (\\X. equal(singleton_set(X),non_ordered_pair(X::'a,X))) & \ \ (\\X Y. equal(ordered_pair(X::'a,Y),non_ordered_pair(singleton_set(X),non_ordered_pair(X::'a,Y)))) & \ @@ -2247,110 +2247,110 @@ \ (\\X. ordered_pair_predicate(X) --> little_set(f3(X))) & \ \ (\\X. ordered_pair_predicate(X) --> equal(X::'a,ordered_pair(f2(X),f3(X)))) & \ \ (\\X Y Z. little_set(Y) & little_set(Z) & equal(X::'a,ordered_pair(Y::'a,Z)) --> ordered_pair_predicate(X)) & \ -\ (\\Z X. member(Z::'a,first(X)) --> little_set(f4(Z::'a,X))) & \ -\ (\\Z X. member(Z::'a,first(X)) --> little_set(f5(Z::'a,X))) & \ -\ (\\Z X. member(Z::'a,first(X)) --> equal(X::'a,ordered_pair(f4(Z::'a,X),f5(Z::'a,X)))) & \ -\ (\\Z X. member(Z::'a,first(X)) --> member(Z::'a,f4(Z::'a,X))) & \ -\ (\\X V Z U. little_set(U) & little_set(V) & equal(X::'a,ordered_pair(U::'a,V)) & member(Z::'a,U) --> member(Z::'a,first(X))) & \ -\ (\\Z X. member(Z::'a,second(X)) --> little_set(f6(Z::'a,X))) & \ -\ (\\Z X. member(Z::'a,second(X)) --> little_set(f7(Z::'a,X))) & \ -\ (\\Z X. member(Z::'a,second(X)) --> equal(X::'a,ordered_pair(f6(Z::'a,X),f7(Z::'a,X)))) & \ -\ (\\Z X. member(Z::'a,second(X)) --> member(Z::'a,f7(Z::'a,X))) & \ -\ (\\X U Z V. little_set(U) & little_set(V) & equal(X::'a,ordered_pair(U::'a,V)) & member(Z::'a,V) --> member(Z::'a,second(X))) & \ -\ (\\Z. member(Z::'a,estin) --> ordered_pair_predicate(Z)) & \ -\ (\\Z. member(Z::'a,estin) --> member(first(Z),second(Z))) & \ -\ (\\Z. little_set(Z) & ordered_pair_predicate(Z) & member(first(Z),second(Z)) --> member(Z::'a,estin)) & \ -\ (\\Y Z X. member(Z::'a,intersection(X::'a,Y)) --> member(Z::'a,X)) & \ -\ (\\X Z Y. member(Z::'a,intersection(X::'a,Y)) --> member(Z::'a,Y)) & \ -\ (\\X Z Y. member(Z::'a,X) & member(Z::'a,Y) --> member(Z::'a,intersection(X::'a,Y))) & \ -\ (\\Z X. ~(member(Z::'a,complement(X)) & member(Z::'a,X))) & \ -\ (\\Z X. little_set(Z) --> member(Z::'a,complement(X)) | member(Z::'a,X)) & \ +\ (\\Z X. memb(Z::'a,first(X)) --> little_set(f4(Z::'a,X))) & \ +\ (\\Z X. memb(Z::'a,first(X)) --> little_set(f5(Z::'a,X))) & \ +\ (\\Z X. memb(Z::'a,first(X)) --> equal(X::'a,ordered_pair(f4(Z::'a,X),f5(Z::'a,X)))) & \ +\ (\\Z X. memb(Z::'a,first(X)) --> memb(Z::'a,f4(Z::'a,X))) & \ +\ (\\X V Z U. little_set(U) & little_set(V) & equal(X::'a,ordered_pair(U::'a,V)) & memb(Z::'a,U) --> memb(Z::'a,first(X))) & \ +\ (\\Z X. memb(Z::'a,second(X)) --> little_set(f6(Z::'a,X))) & \ +\ (\\Z X. memb(Z::'a,second(X)) --> little_set(f7(Z::'a,X))) & \ +\ (\\Z X. memb(Z::'a,second(X)) --> equal(X::'a,ordered_pair(f6(Z::'a,X),f7(Z::'a,X)))) & \ +\ (\\Z X. memb(Z::'a,second(X)) --> memb(Z::'a,f7(Z::'a,X))) & \ +\ (\\X U Z V. little_set(U) & little_set(V) & equal(X::'a,ordered_pair(U::'a,V)) & memb(Z::'a,V) --> memb(Z::'a,second(X))) & \ +\ (\\Z. memb(Z::'a,estin) --> ordered_pair_predicate(Z)) & \ +\ (\\Z. memb(Z::'a,estin) --> memb(first(Z),second(Z))) & \ +\ (\\Z. little_set(Z) & ordered_pair_predicate(Z) & memb(first(Z),second(Z)) --> memb(Z::'a,estin)) & \ +\ (\\Y Z X. memb(Z::'a,intersection(X::'a,Y)) --> memb(Z::'a,X)) & \ +\ (\\X Z Y. memb(Z::'a,intersection(X::'a,Y)) --> memb(Z::'a,Y)) & \ +\ (\\X Z Y. memb(Z::'a,X) & memb(Z::'a,Y) --> memb(Z::'a,intersection(X::'a,Y))) & \ +\ (\\Z X. ~(memb(Z::'a,complement(X)) & memb(Z::'a,X))) & \ +\ (\\Z X. little_set(Z) --> memb(Z::'a,complement(X)) | memb(Z::'a,X)) & \ \ (\\X Y. equal(union(X::'a,Y),complement(intersection(complement(X),complement(Y))))) & \ -\ (\\Z X. member(Z::'a,domain_of(X)) --> ordered_pair_predicate(f8(Z::'a,X))) & \ -\ (\\Z X. member(Z::'a,domain_of(X)) --> member(f8(Z::'a,X),X)) & \ -\ (\\Z X. member(Z::'a,domain_of(X)) --> equal(Z::'a,first(f8(Z::'a,X)))) & \ -\ (\\X Z Xp. little_set(Z) & ordered_pair_predicate(Xp) & member(Xp::'a,X) & equal(Z::'a,first(Xp)) --> member(Z::'a,domain_of(X))) & \ -\ (\\X Y Z. member(Z::'a,cross_product(X::'a,Y)) --> ordered_pair_predicate(Z)) & \ -\ (\\Y Z X. member(Z::'a,cross_product(X::'a,Y)) --> member(first(Z),X)) & \ -\ (\\X Z Y. member(Z::'a,cross_product(X::'a,Y)) --> member(second(Z),Y)) & \ -\ (\\X Z Y. little_set(Z) & ordered_pair_predicate(Z) & member(first(Z),X) & member(second(Z),Y) --> member(Z::'a,cross_product(X::'a,Y))) & \ -\ (\\X Z. member(Z::'a,inv1 X) --> ordered_pair_predicate(Z)) & \ -\ (\\Z X. member(Z::'a,inv1 X) --> member(ordered_pair(second(Z),first(Z)),X)) & \ -\ (\\Z X. little_set(Z) & ordered_pair_predicate(Z) & member(ordered_pair(second(Z),first(Z)),X) --> member(Z::'a,inv1 X)) & \ -\ (\\Z X. member(Z::'a,rot_right(X)) --> little_set(f9(Z::'a,X))) & \ -\ (\\Z X. member(Z::'a,rot_right(X)) --> little_set(f10(Z::'a,X))) & \ -\ (\\Z X. member(Z::'a,rot_right(X)) --> little_set(f11(Z::'a,X))) & \ -\ (\\Z X. member(Z::'a,rot_right(X)) --> equal(Z::'a,ordered_pair(f9(Z::'a,X),ordered_pair(f10(Z::'a,X),f11(Z::'a,X))))) & \ -\ (\\Z X. member(Z::'a,rot_right(X)) --> member(ordered_pair(f10(Z::'a,X),ordered_pair(f11(Z::'a,X),f9(Z::'a,X))),X)) & \ -\ (\\Z V W U X. little_set(Z) & little_set(U) & little_set(V) & little_set(W) & equal(Z::'a,ordered_pair(U::'a,ordered_pair(V::'a,W))) & member(ordered_pair(V::'a,ordered_pair(W::'a,U)),X) --> member(Z::'a,rot_right(X))) & \ -\ (\\Z X. member(Z::'a,flip_range_of(X)) --> little_set(f12(Z::'a,X))) & \ -\ (\\Z X. member(Z::'a,flip_range_of(X)) --> little_set(f13(Z::'a,X))) & \ -\ (\\Z X. member(Z::'a,flip_range_of(X)) --> little_set(f14(Z::'a,X))) & \ -\ (\\Z X. member(Z::'a,flip_range_of(X)) --> equal(Z::'a,ordered_pair(f12(Z::'a,X),ordered_pair(f13(Z::'a,X),f14(Z::'a,X))))) & \ -\ (\\Z X. member(Z::'a,flip_range_of(X)) --> member(ordered_pair(f12(Z::'a,X),ordered_pair(f14(Z::'a,X),f13(Z::'a,X))),X)) & \ -\ (\\Z U W V X. little_set(Z) & little_set(U) & little_set(V) & little_set(W) & equal(Z::'a,ordered_pair(U::'a,ordered_pair(V::'a,W))) & member(ordered_pair(U::'a,ordered_pair(W::'a,V)),X) --> member(Z::'a,flip_range_of(X))) & \ +\ (\\Z X. memb(Z::'a,domain_of(X)) --> ordered_pair_predicate(f8(Z::'a,X))) & \ +\ (\\Z X. memb(Z::'a,domain_of(X)) --> memb(f8(Z::'a,X),X)) & \ +\ (\\Z X. memb(Z::'a,domain_of(X)) --> equal(Z::'a,first(f8(Z::'a,X)))) & \ +\ (\\X Z Xp. little_set(Z) & ordered_pair_predicate(Xp) & memb(Xp::'a,X) & equal(Z::'a,first(Xp)) --> memb(Z::'a,domain_of(X))) & \ +\ (\\X Y Z. memb(Z::'a,cross_product(X::'a,Y)) --> ordered_pair_predicate(Z)) & \ +\ (\\Y Z X. memb(Z::'a,cross_product(X::'a,Y)) --> memb(first(Z),X)) & \ +\ (\\X Z Y. memb(Z::'a,cross_product(X::'a,Y)) --> memb(second(Z),Y)) & \ +\ (\\X Z Y. little_set(Z) & ordered_pair_predicate(Z) & memb(first(Z),X) & memb(second(Z),Y) --> memb(Z::'a,cross_product(X::'a,Y))) & \ +\ (\\X Z. memb(Z::'a,inv1 X) --> ordered_pair_predicate(Z)) & \ +\ (\\Z X. memb(Z::'a,inv1 X) --> memb(ordered_pair(second(Z),first(Z)),X)) & \ +\ (\\Z X. little_set(Z) & ordered_pair_predicate(Z) & memb(ordered_pair(second(Z),first(Z)),X) --> memb(Z::'a,inv1 X)) & \ +\ (\\Z X. memb(Z::'a,rot_right(X)) --> little_set(f9(Z::'a,X))) & \ +\ (\\Z X. memb(Z::'a,rot_right(X)) --> little_set(f10(Z::'a,X))) & \ +\ (\\Z X. memb(Z::'a,rot_right(X)) --> little_set(f11(Z::'a,X))) & \ +\ (\\Z X. memb(Z::'a,rot_right(X)) --> equal(Z::'a,ordered_pair(f9(Z::'a,X),ordered_pair(f10(Z::'a,X),f11(Z::'a,X))))) & \ +\ (\\Z X. memb(Z::'a,rot_right(X)) --> memb(ordered_pair(f10(Z::'a,X),ordered_pair(f11(Z::'a,X),f9(Z::'a,X))),X)) & \ +\ (\\Z V W U X. little_set(Z) & little_set(U) & little_set(V) & little_set(W) & equal(Z::'a,ordered_pair(U::'a,ordered_pair(V::'a,W))) & memb(ordered_pair(V::'a,ordered_pair(W::'a,U)),X) --> memb(Z::'a,rot_right(X))) & \ +\ (\\Z X. memb(Z::'a,flip_range_of(X)) --> little_set(f12(Z::'a,X))) & \ +\ (\\Z X. memb(Z::'a,flip_range_of(X)) --> little_set(f13(Z::'a,X))) & \ +\ (\\Z X. memb(Z::'a,flip_range_of(X)) --> little_set(f14(Z::'a,X))) & \ +\ (\\Z X. memb(Z::'a,flip_range_of(X)) --> equal(Z::'a,ordered_pair(f12(Z::'a,X),ordered_pair(f13(Z::'a,X),f14(Z::'a,X))))) & \ +\ (\\Z X. memb(Z::'a,flip_range_of(X)) --> memb(ordered_pair(f12(Z::'a,X),ordered_pair(f14(Z::'a,X),f13(Z::'a,X))),X)) & \ +\ (\\Z U W V X. little_set(Z) & little_set(U) & little_set(V) & little_set(W) & equal(Z::'a,ordered_pair(U::'a,ordered_pair(V::'a,W))) & memb(ordered_pair(U::'a,ordered_pair(W::'a,V)),X) --> memb(Z::'a,flip_range_of(X))) & \ \ (\\X. equal(successor(X),union(X::'a,singleton_set(X)))) & \ -\ (\\Z. ~member(Z::'a,empty_set)) & \ -\ (\\Z. little_set(Z) --> member(Z::'a,universal_set)) & \ +\ (\\Z. ~memb(Z::'a,empty_set)) & \ +\ (\\Z. little_set(Z) --> memb(Z::'a,universal_set)) & \ \ (little_set(infinity)) & \ -\ (member(empty_set::'a,infinity)) & \ -\ (\\X. member(X::'a,infinity) --> member(successor(X),infinity)) & \ -\ (\\Z X. member(Z::'a,sigma(X)) --> member(f16(Z::'a,X),X)) & \ -\ (\\Z X. member(Z::'a,sigma(X)) --> member(Z::'a,f16(Z::'a,X))) & \ -\ (\\X Z Y. member(Y::'a,X) & member(Z::'a,Y) --> member(Z::'a,sigma(X))) & \ +\ (memb(empty_set::'a,infinity)) & \ +\ (\\X. memb(X::'a,infinity) --> memb(successor(X),infinity)) & \ +\ (\\Z X. memb(Z::'a,sigma(X)) --> memb(f16(Z::'a,X),X)) & \ +\ (\\Z X. memb(Z::'a,sigma(X)) --> memb(Z::'a,f16(Z::'a,X))) & \ +\ (\\X Z Y. memb(Y::'a,X) & memb(Z::'a,Y) --> memb(Z::'a,sigma(X))) & \ \ (\\U. little_set(U) --> little_set(sigma(U))) & \ -\ (\\X U Y. ssubset(X::'a,Y) & member(U::'a,X) --> member(U::'a,Y)) & \ -\ (\\Y X. ssubset(X::'a,Y) | member(f17(X::'a,Y),X)) & \ -\ (\\X Y. member(f17(X::'a,Y),Y) --> ssubset(X::'a,Y)) & \ +\ (\\X U Y. ssubset(X::'a,Y) & memb(U::'a,X) --> memb(U::'a,Y)) & \ +\ (\\Y X. ssubset(X::'a,Y) | memb(f17(X::'a,Y),X)) & \ +\ (\\X Y. memb(f17(X::'a,Y),Y) --> ssubset(X::'a,Y)) & \ \ (\\X Y. proper_subset(X::'a,Y) --> ssubset(X::'a,Y)) & \ \ (\\X Y. ~(proper_subset(X::'a,Y) & equal(X::'a,Y))) & \ \ (\\X Y. ssubset(X::'a,Y) --> proper_subset(X::'a,Y) | equal(X::'a,Y)) & \ -\ (\\Z X. member(Z::'a,powerset(X)) --> ssubset(Z::'a,X)) & \ -\ (\\Z X. little_set(Z) & ssubset(Z::'a,X) --> member(Z::'a,powerset(X))) & \ +\ (\\Z X. memb(Z::'a,powerset(X)) --> ssubset(Z::'a,X)) & \ +\ (\\Z X. little_set(Z) & ssubset(Z::'a,X) --> memb(Z::'a,powerset(X))) & \ \ (\\U. little_set(U) --> little_set(powerset(U))) & \ -\ (\\Z X. relation(Z) & member(X::'a,Z) --> ordered_pair_predicate(X)) & \ -\ (\\Z. relation(Z) | member(f18(Z),Z)) & \ +\ (\\Z X. relation(Z) & memb(X::'a,Z) --> ordered_pair_predicate(X)) & \ +\ (\\Z. relation(Z) | memb(f18(Z),Z)) & \ \ (\\Z. ordered_pair_predicate(f18(Z)) --> relation(Z)) & \ -\ (\\U X V W. single_valued_set(X) & little_set(U) & little_set(V) & little_set(W) & member(ordered_pair(U::'a,V),X) & member(ordered_pair(U::'a,W),X) --> equal(V::'a,W)) & \ +\ (\\U X V W. single_valued_set(X) & little_set(U) & little_set(V) & little_set(W) & memb(ordered_pair(U::'a,V),X) & memb(ordered_pair(U::'a,W),X) --> equal(V::'a,W)) & \ \ (\\X. single_valued_set(X) | little_set(f19(X))) & \ \ (\\X. single_valued_set(X) | little_set(f20(X))) & \ \ (\\X. single_valued_set(X) | little_set(f21(X))) & \ -\ (\\X. single_valued_set(X) | member(ordered_pair(f19(X),f20(X)),X)) & \ -\ (\\X. single_valued_set(X) | member(ordered_pair(f19(X),f21(X)),X)) & \ +\ (\\X. single_valued_set(X) | memb(ordered_pair(f19(X),f20(X)),X)) & \ +\ (\\X. single_valued_set(X) | memb(ordered_pair(f19(X),f21(X)),X)) & \ \ (\\X. equal(f20(X),f21(X)) --> single_valued_set(X)) & \ \ (\\Xf. function(Xf) --> relation(Xf)) & \ \ (\\Xf. function(Xf) --> single_valued_set(Xf)) & \ \ (\\Xf. relation(Xf) & single_valued_set(Xf) --> function(Xf)) & \ -\ (\\Z X Xf. member(Z::'a,image_(X::'a,Xf)) --> ordered_pair_predicate(f22(Z::'a,X,Xf))) & \ -\ (\\Z X Xf. member(Z::'a,image_(X::'a,Xf)) --> member(f22(Z::'a,X,Xf),Xf)) & \ -\ (\\Z Xf X. member(Z::'a,image_(X::'a,Xf)) --> member(first(f22(Z::'a,X,Xf)),X)) & \ -\ (\\X Xf Z. member(Z::'a,image_(X::'a,Xf)) --> equal(second(f22(Z::'a,X,Xf)),Z)) & \ -\ (\\Xf X Y Z. little_set(Z) & ordered_pair_predicate(Y) & member(Y::'a,Xf) & member(first(Y),X) & equal(second(Y),Z) --> member(Z::'a,image_(X::'a,Xf))) & \ +\ (\\Z X Xf. memb(Z::'a,image_(X::'a,Xf)) --> ordered_pair_predicate(f22(Z::'a,X,Xf))) & \ +\ (\\Z X Xf. memb(Z::'a,image_(X::'a,Xf)) --> memb(f22(Z::'a,X,Xf),Xf)) & \ +\ (\\Z Xf X. memb(Z::'a,image_(X::'a,Xf)) --> memb(first(f22(Z::'a,X,Xf)),X)) & \ +\ (\\X Xf Z. memb(Z::'a,image_(X::'a,Xf)) --> equal(second(f22(Z::'a,X,Xf)),Z)) & \ +\ (\\Xf X Y Z. little_set(Z) & ordered_pair_predicate(Y) & memb(Y::'a,Xf) & memb(first(Y),X) & equal(second(Y),Z) --> memb(Z::'a,image_(X::'a,Xf))) & \ \ (\\X Xf. little_set(X) & function(Xf) --> little_set(image_(X::'a,Xf))) & \ -\ (\\X U Y. ~(disjoint(X::'a,Y) & member(U::'a,X) & member(U::'a,Y))) & \ -\ (\\Y X. disjoint(X::'a,Y) | member(f23(X::'a,Y),X)) & \ -\ (\\X Y. disjoint(X::'a,Y) | member(f23(X::'a,Y),Y)) & \ -\ (\\X. equal(X::'a,empty_set) | member(f24(X),X)) & \ +\ (\\X U Y. ~(disjoint(X::'a,Y) & memb(U::'a,X) & memb(U::'a,Y))) & \ +\ (\\Y X. disjoint(X::'a,Y) | memb(f23(X::'a,Y),X)) & \ +\ (\\X Y. disjoint(X::'a,Y) | memb(f23(X::'a,Y),Y)) & \ +\ (\\X. equal(X::'a,empty_set) | memb(f24(X),X)) & \ \ (\\X. equal(X::'a,empty_set) | disjoint(f24(X),X)) & \ \ (function(f25)) & \ -\ (\\X. little_set(X) --> equal(X::'a,empty_set) | member(f26(X),X)) & \ -\ (\\X. little_set(X) --> equal(X::'a,empty_set) | member(ordered_pair(X::'a,f26(X)),f25)) & \ -\ (\\Z X. member(Z::'a,range_of(X)) --> ordered_pair_predicate(f27(Z::'a,X))) & \ -\ (\\Z X. member(Z::'a,range_of(X)) --> member(f27(Z::'a,X),X)) & \ -\ (\\Z X. member(Z::'a,range_of(X)) --> equal(Z::'a,second(f27(Z::'a,X)))) & \ -\ (\\X Z Xp. little_set(Z) & ordered_pair_predicate(Xp) & member(Xp::'a,X) & equal(Z::'a,second(Xp)) --> member(Z::'a,range_of(X))) & \ -\ (\\Z. member(Z::'a,identity_relation) --> ordered_pair_predicate(Z)) & \ -\ (\\Z. member(Z::'a,identity_relation) --> equal(first(Z),second(Z))) & \ -\ (\\Z. little_set(Z) & ordered_pair_predicate(Z) & equal(first(Z),second(Z)) --> member(Z::'a,identity_relation)) & \ +\ (\\X. little_set(X) --> equal(X::'a,empty_set) | memb(f26(X),X)) & \ +\ (\\X. little_set(X) --> equal(X::'a,empty_set) | memb(ordered_pair(X::'a,f26(X)),f25)) & \ +\ (\\Z X. memb(Z::'a,range_of(X)) --> ordered_pair_predicate(f27(Z::'a,X))) & \ +\ (\\Z X. memb(Z::'a,range_of(X)) --> memb(f27(Z::'a,X),X)) & \ +\ (\\Z X. memb(Z::'a,range_of(X)) --> equal(Z::'a,second(f27(Z::'a,X)))) & \ +\ (\\X Z Xp. little_set(Z) & ordered_pair_predicate(Xp) & memb(Xp::'a,X) & equal(Z::'a,second(Xp)) --> memb(Z::'a,range_of(X))) & \ +\ (\\Z. memb(Z::'a,identity_relation) --> ordered_pair_predicate(Z)) & \ +\ (\\Z. memb(Z::'a,identity_relation) --> equal(first(Z),second(Z))) & \ +\ (\\Z. little_set(Z) & ordered_pair_predicate(Z) & equal(first(Z),second(Z)) --> memb(Z::'a,identity_relation)) & \ \ (\\X Y. equal(restrct(X::'a,Y),intersection(X::'a,cross_product(Y::'a,universal_set)))) & \ \ (\\Xf. one_to_one_function(Xf) --> function(Xf)) & \ \ (\\Xf. one_to_one_function(Xf) --> function(inv1 Xf)) & \ \ (\\Xf. function(Xf) & function(inv1 Xf) --> one_to_one_function(Xf)) & \ -\ (\\Z Xf Y. member(Z::'a,apply(Xf::'a,Y)) --> ordered_pair_predicate(f28(Z::'a,Xf,Y))) & \ -\ (\\Z Y Xf. member(Z::'a,apply(Xf::'a,Y)) --> member(f28(Z::'a,Xf,Y),Xf)) & \ -\ (\\Z Xf Y. member(Z::'a,apply(Xf::'a,Y)) --> equal(first(f28(Z::'a,Xf,Y)),Y)) & \ -\ (\\Z Xf Y. member(Z::'a,apply(Xf::'a,Y)) --> member(Z::'a,second(f28(Z::'a,Xf,Y)))) & \ -\ (\\Xf Y Z W. ordered_pair_predicate(W) & member(W::'a,Xf) & equal(first(W),Y) & member(Z::'a,second(W)) --> member(Z::'a,apply(Xf::'a,Y))) & \ +\ (\\Z Xf Y. memb(Z::'a,apply(Xf::'a,Y)) --> ordered_pair_predicate(f28(Z::'a,Xf,Y))) & \ +\ (\\Z Y Xf. memb(Z::'a,apply(Xf::'a,Y)) --> memb(f28(Z::'a,Xf,Y),Xf)) & \ +\ (\\Z Xf Y. memb(Z::'a,apply(Xf::'a,Y)) --> equal(first(f28(Z::'a,Xf,Y)),Y)) & \ +\ (\\Z Xf Y. memb(Z::'a,apply(Xf::'a,Y)) --> memb(Z::'a,second(f28(Z::'a,Xf,Y)))) & \ +\ (\\Xf Y Z W. ordered_pair_predicate(W) & memb(W::'a,Xf) & equal(first(W),Y) & memb(Z::'a,second(W)) --> memb(Z::'a,apply(Xf::'a,Y))) & \ \ (\\Xf X Y. equal(apply_to_two_arguments(Xf::'a,X,Y),apply(Xf::'a,ordered_pair(X::'a,Y)))) & \ \ (\\X Y Xf. maps(Xf::'a,X,Y) --> function(Xf)) & \ \ (\\Y Xf X. maps(Xf::'a,X,Y) --> equal(domain_of(Xf),X)) & \ @@ -2360,19 +2360,19 @@ \ (\\Xs Xf. closed(Xs::'a,Xf) --> little_set(Xf)) & \ \ (\\Xf Xs. closed(Xs::'a,Xf) --> maps(Xf::'a,cross_product(Xs::'a,Xs),Xs)) & \ \ (\\Xf Xs. little_set(Xs) & little_set(Xf) & maps(Xf::'a,cross_product(Xs::'a,Xs),Xs) --> closed(Xs::'a,Xf)) & \ -\ (\\Z Xf Xg. member(Z::'a,composition(Xf::'a,Xg)) --> little_set(f29(Z::'a,Xf,Xg))) & \ -\ (\\Z Xf Xg. member(Z::'a,composition(Xf::'a,Xg)) --> little_set(f30(Z::'a,Xf,Xg))) & \ -\ (\\Z Xf Xg. member(Z::'a,composition(Xf::'a,Xg)) --> little_set(f31(Z::'a,Xf,Xg))) & \ -\ (\\Z Xf Xg. member(Z::'a,composition(Xf::'a,Xg)) --> equal(Z::'a,ordered_pair(f29(Z::'a,Xf,Xg),f30(Z::'a,Xf,Xg)))) & \ -\ (\\Z Xg Xf. member(Z::'a,composition(Xf::'a,Xg)) --> member(ordered_pair(f29(Z::'a,Xf,Xg),f31(Z::'a,Xf,Xg)),Xf)) & \ -\ (\\Z Xf Xg. member(Z::'a,composition(Xf::'a,Xg)) --> member(ordered_pair(f31(Z::'a,Xf,Xg),f30(Z::'a,Xf,Xg)),Xg)) & \ -\ (\\Z X Xf W Y Xg. little_set(Z) & little_set(X) & little_set(Y) & little_set(W) & equal(Z::'a,ordered_pair(X::'a,Y)) & member(ordered_pair(X::'a,W),Xf) & member(ordered_pair(W::'a,Y),Xg) --> member(Z::'a,composition(Xf::'a,Xg))) & \ +\ (\\Z Xf Xg. memb(Z::'a,composition(Xf::'a,Xg)) --> little_set(f29(Z::'a,Xf,Xg))) & \ +\ (\\Z Xf Xg. memb(Z::'a,composition(Xf::'a,Xg)) --> little_set(f30(Z::'a,Xf,Xg))) & \ +\ (\\Z Xf Xg. memb(Z::'a,composition(Xf::'a,Xg)) --> little_set(f31(Z::'a,Xf,Xg))) & \ +\ (\\Z Xf Xg. memb(Z::'a,composition(Xf::'a,Xg)) --> equal(Z::'a,ordered_pair(f29(Z::'a,Xf,Xg),f30(Z::'a,Xf,Xg)))) & \ +\ (\\Z Xg Xf. memb(Z::'a,composition(Xf::'a,Xg)) --> memb(ordered_pair(f29(Z::'a,Xf,Xg),f31(Z::'a,Xf,Xg)),Xf)) & \ +\ (\\Z Xf Xg. memb(Z::'a,composition(Xf::'a,Xg)) --> memb(ordered_pair(f31(Z::'a,Xf,Xg),f30(Z::'a,Xf,Xg)),Xg)) & \ +\ (\\Z X Xf W Y Xg. little_set(Z) & little_set(X) & little_set(Y) & little_set(W) & equal(Z::'a,ordered_pair(X::'a,Y)) & memb(ordered_pair(X::'a,W),Xf) & memb(ordered_pair(W::'a,Y),Xg) --> memb(Z::'a,composition(Xf::'a,Xg))) & \ \ (\\Xh Xs2 Xf2 Xs1 Xf1. homomorphism(Xh::'a,Xs1,Xf1,Xs2,Xf2) --> closed(Xs1::'a,Xf1)) & \ \ (\\Xh Xs1 Xf1 Xs2 Xf2. homomorphism(Xh::'a,Xs1,Xf1,Xs2,Xf2) --> closed(Xs2::'a,Xf2)) & \ \ (\\Xf1 Xf2 Xh Xs1 Xs2. homomorphism(Xh::'a,Xs1,Xf1,Xs2,Xf2) --> maps(Xh::'a,Xs1,Xs2)) & \ -\ (\\Xs2 Xs1 Xf1 Xf2 X Xh Y. homomorphism(Xh::'a,Xs1,Xf1,Xs2,Xf2) & member(X::'a,Xs1) & member(Y::'a,Xs1) --> equal(apply(Xh::'a,apply_to_two_arguments(Xf1::'a,X,Y)),apply_to_two_arguments(Xf2::'a,apply(Xh::'a,X),apply(Xh::'a,Y)))) & \ -\ (\\Xh Xf1 Xs2 Xf2 Xs1. closed(Xs1::'a,Xf1) & closed(Xs2::'a,Xf2) & maps(Xh::'a,Xs1,Xs2) --> homomorphism(Xh::'a,Xs1,Xf1,Xs2,Xf2) | member(f32(Xh::'a,Xs1,Xf1,Xs2,Xf2),Xs1)) & \ -\ (\\Xh Xf1 Xs2 Xf2 Xs1. closed(Xs1::'a,Xf1) & closed(Xs2::'a,Xf2) & maps(Xh::'a,Xs1,Xs2) --> homomorphism(Xh::'a,Xs1,Xf1,Xs2,Xf2) | member(f33(Xh::'a,Xs1,Xf1,Xs2,Xf2),Xs1)) & \ +\ (\\Xs2 Xs1 Xf1 Xf2 X Xh Y. homomorphism(Xh::'a,Xs1,Xf1,Xs2,Xf2) & memb(X::'a,Xs1) & memb(Y::'a,Xs1) --> equal(apply(Xh::'a,apply_to_two_arguments(Xf1::'a,X,Y)),apply_to_two_arguments(Xf2::'a,apply(Xh::'a,X),apply(Xh::'a,Y)))) & \ +\ (\\Xh Xf1 Xs2 Xf2 Xs1. closed(Xs1::'a,Xf1) & closed(Xs2::'a,Xf2) & maps(Xh::'a,Xs1,Xs2) --> homomorphism(Xh::'a,Xs1,Xf1,Xs2,Xf2) | memb(f32(Xh::'a,Xs1,Xf1,Xs2,Xf2),Xs1)) & \ +\ (\\Xh Xf1 Xs2 Xf2 Xs1. closed(Xs1::'a,Xf1) & closed(Xs2::'a,Xf2) & maps(Xh::'a,Xs1,Xs2) --> homomorphism(Xh::'a,Xs1,Xf1,Xs2,Xf2) | memb(f33(Xh::'a,Xs1,Xf1,Xs2,Xf2),Xs1)) & \ \ (\\Xh Xs1 Xf1 Xs2 Xf2. closed(Xs1::'a,Xf1) & closed(Xs2::'a,Xf2) & maps(Xh::'a,Xs1,Xs2) & equal(apply(Xh::'a,apply_to_two_arguments(Xf1::'a,f32(Xh::'a,Xs1,Xf1,Xs2,Xf2),f33(Xh::'a,Xs1,Xf1,Xs2,Xf2))),apply_to_two_arguments(Xf2::'a,apply(Xh::'a,f32(Xh::'a,Xs1,Xf1,Xs2,Xf2)),apply(Xh::'a,f33(Xh::'a,Xs1,Xf1,Xs2,Xf2)))) --> homomorphism(Xh::'a,Xs1,Xf1,Xs2,Xf2)) & \ \ (\\A B C. equal(A::'a,B) --> equal(f1(A::'a,C),f1(B::'a,C))) & \ \ (\\D F' E. equal(D::'a,E) --> equal(f1(F'::'a,D),f1(F'::'a,E))) & \ @@ -2486,8 +2486,8 @@ \ (\\Q14 R14 S14 T14. equal(Q14::'a,R14) & maps(Q14::'a,S14,T14) --> maps(R14::'a,S14,T14)) & \ \ (\\U14 W14 V14 X14. equal(U14::'a,V14) & maps(W14::'a,U14,X14) --> maps(W14::'a,V14,X14)) & \ \ (\\Y14 A15 B15 Z14. equal(Y14::'a,Z14) & maps(A15::'a,B15,Y14) --> maps(A15::'a,B15,Z14)) & \ -\ (\\C15 D15 E15. equal(C15::'a,D15) & member(C15::'a,E15) --> member(D15::'a,E15)) & \ -\ (\\F15 H15 G15. equal(F15::'a,G15) & member(H15::'a,F15) --> member(H15::'a,G15)) & \ +\ (\\C15 D15 E15. equal(C15::'a,D15) & memb(C15::'a,E15) --> memb(D15::'a,E15)) & \ +\ (\\F15 H15 G15. equal(F15::'a,G15) & memb(H15::'a,F15) --> memb(H15::'a,G15)) & \ \ (\\I15 J15. equal(I15::'a,J15) & one_to_one_function(I15) --> one_to_one_function(J15)) & \ \ (\\K15 L15. equal(K15::'a,L15) & ordered_pair_predicate(K15) --> ordered_pair_predicate(L15)) & \ \ (\\M15 N15 O15. equal(M15::'a,N15) & proper_subset(M15::'a,O15) --> proper_subset(N15::'a,O15)) & \