meson/test/selftest.sml

1682    (!Xf. function(Xf) ==> subclass(Xf,cross_product(universal_class,universal_class))) /\
1683    (!Xf. function(Xf) ==> subclass(compose(Xf,inverse(Xf)),identity_relation)) /\
1684    (!Xf. subclass(Xf,cross_product(universal_class,universal_class)) /\ subclass(compose(Xf,inverse(Xf)),identity_relation) ==> function(Xf)) /\
1685    (!Xf X. function(Xf) /\ member(X,universal_class) ==> member(image(Xf,X),universal_class)) /\
1689    (function(choice)) /\
1691    (!Xf. one_to_one(Xf) ==> function(Xf)) /\
1692    (!Xf. one_to_one(Xf) ==> function(inverse(Xf))) /\
1693    (!Xf. function(inverse(Xf)) /\ function(Xf) ==> one_to_one(Xf)) /\
1698    (!Xf. operation(Xf) ==> function(Xf)) /\
1701    (!Xf. function(Xf) /\ equal(cross_product(domain_of(domain_of(Xf)),domain_of(domain_of(Xf))),domain_of(Xf)) /\ subclass(range_of(Xf),domain_of(domain_of(Xf))) ==> operation(Xf)) /\
1702    (!Xf1 Xf2 Xh. compatible(Xh,Xf1,Xf2) ==> function(Xh)) /\
1705    (!Xh Xh1 Xf1 Xf2. function(Xh) /\ equal(domain_of(domain_of(Xf1)),domain_of(Xh)) /\ subclass(range_of(Xh),domain_of(domain_of(Xf2))) ==> compatible(Xh1,Xf1,Xf2)) /\
1765    (!J6 K6. equal(J6,K6) /\ function(J6) ==> function(K6)) /\
1794    (!X Y Xf. maps(Xf,X,Y) ==> function(Xf)) /\
1797    (!Xf Y. function(Xf) /\ subclass(range_of(Xf),Y) ==> maps(Xf,domain_of(Xf),Y)) /\
1839    (!X Z. member(X,recursion_equation_functions(Z)) ==> function(Z)) /\
1840    (!Z X. member(X,recursion_equation_functions(Z)) ==> function(X)) /\
1843    (!X Z. function(Z) /\ function(X) /\ member(domain_of(X),ordinal_numbers) /\ equal(compose(Z,rest_of(X)),X) ==> member(X,recursion_equation_functions(Z))) /\
1952    (!Xf. function(Xf) ==> subclass(Xf,cross_product(universal_class,universal_class))) /\
1953    (!Xf. function(Xf) ==> subclass(compose(Xf,inverse(Xf)),identity_relation)) /\
1954    (!Xf. subclass(Xf,cross_product(universal_class,universal_class)) /\ subclass(compose(Xf,inverse(Xf)),identity_relation) ==> function(Xf)) /\
1955    (!Xf X. function(Xf) /\ member(X,universal_class) ==> member(image(Xf,X),universal_class)) /\
1959    (function(choice)) /\
1961    (!Xf. one_to_one(Xf) ==> function(Xf)) /\
1962    (!Xf. one_to_one(Xf) ==> function(inverse(Xf))) /\
1963    (!Xf. function(inverse(Xf)) /\ function(Xf) ==> one_to_one(Xf)) /\
1968    (!Xf. operation(Xf) ==> function(Xf)) /\
1971    (!Xf. function(Xf) /\ equal(cross_product(domain_of(domain_of(Xf)),domain_of(domain_of(Xf))),domain_of(Xf)) /\ subclass(range_of(Xf),domain_of(domain_of(Xf))) ==> operation(Xf)) /\
1972    (!Xf1 Xf2 Xh. compatible(Xh,Xf1,Xf2) ==> function(Xh)) /\
1975    (!Xh Xh1 Xf1 Xf2. function(Xh) /\ equal(domain_of(domain_of(Xf1)),domain_of(Xh)) /\ subclass(range_of(Xh),domain_of(domain_of(Xf2))) ==> compatible(Xh1,Xf1,Xf2)) /\
2035    (!J6 K6. equal(J6,K6) /\ function(J6) ==> function(K6)) /\
2064    (!X Y Xf. maps(Xf,X,Y) ==> function(Xf)) /\
2067    (!Xf Y. function(Xf) /\ subclass(range_of(Xf),Y) ==> maps(Xf,domain_of(Xf),Y)) /\
2109    (!X Z. member(X,recursion_equation_functions(Z)) ==> function(Z)) /\
2110    (!Z X. member(X,recursion_equation_functions(Z)) ==> function(X)) /\
2113    (!X Z. function(Z) /\ function(X) /\ member(domain_of(X),ordinal_numbers) /\ equal(compose(Z,rest_of(X)),X) ==> member(X,recursion_equation_functions(Z))) /\
2152    (~function(z)) /\
3016    (!Xf. function(Xf) ==> relation(Xf)) /\
3017    (!Xf. function(Xf) ==> single_valued_set(Xf)) /\
3018    (!Xf. relation(Xf) /\ single_valued_set(Xf) ==> function(Xf)) /\
3024    (!X Xf. little_set(X) /\ function(Xf) ==> little_set(image(X,Xf))) /\
3030    (function(f25)) /\
3041    (!Xf. one_to_one_function(Xf) ==> function(Xf)) /\
3042    (!Xf. one_to_one_function(Xf) ==> function(converse(Xf))) /\
3043    (!Xf. function(Xf) /\ function(converse(Xf)) ==> one_to_one_function(Xf)) /\
3050    (!X Y Xf. maps(Xf,X,Y) ==> function(Xf)) /\
3053    (!X Xf Y. function(Xf) /\ equal(domain_of(Xf),X) /\ subset(range_of(Xf),Y) ==> maps(Xf,X,Y)) /\
3174    (!I13 J13. equal(I13,J13) /\ function(I13) ==> function(J13)) /\