consequent

(=>     (and         (equal             (RemainderFn ?NUMBER1 ?NUMBER2) ?NUMBER)         (not             (equal ?NUMBER 0))         (not             (equal ?NUMBER1 0))         (not             (equal ?NUMBER2 0)))     (equal         (SignumFn ?NUMBER2)         (SignumFn ?NUMBER)))	Merge.kif 5242-5254	If equal X mod Y and Z, equal Z and 0, equal X and 0, and equal Y and 0, then equal the sign of Y and the sign of Z
(=>     (instance ?NUMBER NonnegativeRealNumber)     (or         (equal             (SignumFn ?NUMBER) 1)         (equal             (SignumFn ?NUMBER) 0)))	Merge.kif 5307-5311	If X is an instance of nonnegative real number, then equal the sign of X and 1 or equal the sign of X and 0
(=>     (instance ?NUMBER PositiveRealNumber)     (equal         (SignumFn ?NUMBER) 1))	Merge.kif 5313-5315	If X is an instance of positive real number, then equal the sign of X and 1
(=>     (instance ?NUMBER NegativeRealNumber)     (equal         (SignumFn ?NUMBER) -1))	Merge.kif 5317-5319	If X is an instance of negative real number, then equal the sign of X and -1

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