antecedent

(=>     (and         (exactCardinality ?REL ?ARG 1)         (instance ?REL Predicate))     (exists (?X @ARGS)         (and             (?REL @ARGS)             (equal ?X                 (ListOrderFn                     (ListFn @ARGS) ?ARG))             (not                 (exists (?Y)                     (and                         (equal ?Y                             (ListOrderFn                                 (ListFn @ARGS) ?ARG))                         (not                             (equal ?X ?Y))))))))	Media.kif 2022-2037	If there can be 1 values to argument X of Y and Y is an instance of predicate, then there exist Z and @ARGS such that Y @ARGS and equal Z and V element of (@ARGS) and there doesn't exist U such that equal U and V element of (@ARGS) and equal Z and U
(=>     (and         (exactCardinality ?REL ?ARG 1)         (instance ?REL Predicate)         (?REL @ARGS)         (equal ?X             (ListOrderFn                 (ListFn @ARGS) ?ARG)))     (not         (exists (?Y)             (and                 (equal ?Y                     (ListOrderFn                         (ListFn @ARGS) ?ARG))                 (not                     (equal ?X ?Y))))))	Media.kif 2040-2050	If there can be 1 values to argument X of Y, Y is an instance of predicate, Y @ARGS, and equal W and V element of (@ARGS), then there doesn't exist U such that equal U and V element of (@ARGS) and equal W and U
(=>     (and         (exactCardinality ?REL ?ARG 1)         (instance ?REL Predicate)         (?REL @ARGS)         (equal ?X             (ListOrderFn                 (ListFn @ARGS) ?ARG))         (equal ?Y             (ListOrderFn                 (ListFn @ARGS) ?ARG)))     (equal ?X ?Y))	Media.kif 2053-2060	If there can be 1 values to argument X of Y, Y is an instance of predicate, Y @ARGS, equal W and V element of (@ARGS), and equal U and V element of (@ARGS), then equal W and U
(=>     (exactCardinality ?REL ?ARG ?COUNT)     (exists (?EL @ARGS)         (equal             (CardinalityFn                 (KappaFn ?EL                     (and                         (?REL @ARGS)                         (equal ?EL                             (ListOrderFn                                 (ListFn @ARGS) ?ARG))))) ?COUNT)))	Media.kif 2072-2081	If there can be X values to argument Y of Z, then there exist W, @ARGS such that equal the number of instances in the class described by W, and X
(=>     (and         (exactCardinality ?REL ?ARG ?COUNT)         (instance ?REL Predicate))     (exists (?S ?EL @ARGS)         (and             (instance ?S SetOrClass)             (=>                 (and                     (?REL @ARGS)                     (equal ?EL                         (ListOrderFn                             (ListFn @ARGS) ?ARG)))                 (and                     (instance ?EL ?S)                     (equal                         (CardinalityFn ?S) ?COUNT))))))	Media.kif 2084-2097	If there can be X values to argument Y of Z and Z is an instance of predicate, then there exist W, V and @ARGS such that W is an instance of set or class and Z @ARGS and equal V and T element of (@ARGS)V is an instance of W and equal the number of instances in W and X

Show simplified definition (without tree view)
Show simplified definition (with tree view)