Browsing Interface : Welcome guest : log in
|
Browsing Interface : Welcome guest : log in |
[
Home |
Graph |
LogLearn |
Editor |
]
KB:
Language:
Formal Language:
|
| OneToOneFunction(one to one function) |
| appearance as argument number 1 |
|
| (subclass OneToOneFunction UnaryFunction) | Merge.kif 3482-3482 | One to one function is a subclass of unary function |
| (documentation OneToOneFunction EnglishLanguage "The Class of UnaryFunctions which are one to one. A function F is one to one just in case for all X, Y in the domain of F, if X is not identical to Y, then F(X) is not identical to F(Y).") | Merge.kif 3484-3486 | One to one function is a subclass of unary function |
| appearance as argument number 2 |
|
|
| (subclass SequenceFunction OneToOneFunction) | Merge.kif 3500-3500 | Sequence function is a subclass of one to one function |
| (format EnglishLanguage OneToOneFunction "the one to one function of %1") | domainEnglishFormat.kif 1837-1837 | Sequence function is a subclass of one to one function |
| (format ChineseTraditionalLanguage OneToOneFunction "%1 的 one 對一 功能") | domainEnglishFormat.kif 1838-1838 | Sequence function is a subclass of one to one function |
| (format ChineseLanguage OneToOneFunction "%1 的 one 对一 功能") | domainEnglishFormat.kif 1839-1839 | Sequence function is a subclass of one to one function |
| (termFormat EnglishLanguage OneToOneFunction "one to one function") | english_format.kif 1047-1047 | Sequence function is a subclass of one to one function |
| antecedent |
|
|
| (=> (instance ?FUN OneToOneFunction) (forall (?ARG1 ?ARG2) (=> (exists (?CLASS) (and (domain ?FUN 1 ?CLASS) (instance ?ARG1 ?CLASS) (instance ?ARG2 ?CLASS) (not (equal ?ARG1 ?ARG2)))) (not (equal (AssignmentFn ?FUN ?ARG1) (AssignmentFn ?FUN ?ARG2)))))) |
Merge.kif 3488-3498 | If X is an instance of one to one function, then For all Entities Y and Z: if there exists W such that the number 1 argument of X is an instance of W, Y is an instance of W, Z is an instance of W, equal Y, and Z, then equal X(Y) and X(Z) |
|