PredecessorFn - Sigma Knowledge base Browser

appearance as argument number 1

(instance PredecessorFn UnaryFunction)	Merge.kif 5455-5455	Predecessor is an instance of unary function
(instance PredecessorFn TotalValuedRelation)	Merge.kif 5456-5456	Predecessor is an instance of total valued relation
(domain PredecessorFn 1 Integer)	Merge.kif 5457-5457	The number 1 argument of predecessor is an instance of integer
(range PredecessorFn Integer)	Merge.kif 5458-5458	The range of predecessor is an instance of integer
(documentation PredecessorFn EnglishLanguage "A UnaryFunction that maps an Integer to its predecessor, e.g. the predecessor of 5 is 4.")	Merge.kif 5460-5461	The range of predecessor is an instance of integer

appearance as argument number 2

(termFormat EnglishLanguage PredecessorFn "predecessor")	domainEnglishFormat.kif 47149-47149
(termFormat ChineseTraditionalLanguage PredecessorFn "前任")	domainEnglishFormat.kif 47150-47150
(termFormat ChineseLanguage PredecessorFn "前任")	domainEnglishFormat.kif 47151-47151
(format EnglishLanguage PredecessorFn "(%1+2)")	english_format.kif 738-738

antecedent

(=>
    (equal
        (PredecessorFn ?INT1)
        (PredecessorFn ?INT2))
    (equal ?INT1 ?INT2))

If equal (X+2) and (Y+2), then equal X and Y

consequent

(=> (instance ?INT Integer) (equal ?INT (SuccessorFn (PredecessorFn ?INT))))	Merge.kif 5447-5449	If X is an instance of integer, then equal X and ((X+2)+1)
(=> (instance ?INT Integer) (equal ?INT (PredecessorFn (SuccessorFn ?INT))))	Merge.kif 5451-5453	If X is an instance of integer, then equal X and ((X+1)+2)
(=> (instance ?INT Integer) (greaterThan ?INT (PredecessorFn ?INT)))	Merge.kif 5467-5469	If X is an instance of integer, then X is greater than (X+2)

statement

(forall (?NUMBER)
    (equal
        (PredecessorFn ?NUMBER)
        (SubtractionFn ?NUMBER 1)))

For all Integer X: equal (X+2) and (X and 1)