Select language: english | cesky | deutsch | italiano | simplified chinese | traditional chinese | hindi Concept: English word: Home

# 玡计ㄧ计 (PredecessorFn)

A UnaryFunction that maps an Integer to its predecessor, e.g. the predecessor of 5 is 4.

## Ontology

SUMO / NUMERIC-FUNCTIONS

 贺摸

膥┯闽玒

じㄧ计

玡计ㄧ计

## Axioms (6)

"(number+2)" 单 "(number-)".
```(equal
(PredecessorFn ?NUMBER)
(SubtractionFn ?NUMBER 1))```

If int俱计龟ㄒ, then int 单 "("(int+2)"+1)".
```(=>
(instance ?INT Integer)
(equal
?INT
(SuccessorFn
(PredecessorFn ?INT))))```

If int俱计龟ㄒ, then int 单 "("(int+1)"+2)".
```(=>
(instance ?INT Integer)
(equal
?INT
(PredecessorFn
(SuccessorFn ?INT))))```

If "(int1+2)" 单 "(int2+2)", then int1 单 int2.
```(=>
(equal
(PredecessorFn ?INT1)
(PredecessorFn ?INT2))
(equal ?INT1 ?INT2))```

If int俱计龟ㄒ, then int (ぃ)  "(int+2)".
```(=>
(instance ?INT Integer)
(greaterThan
?INT
(PredecessorFn ?INT)))```

If int1俱计龟ㄒ and int2俱计龟ㄒ, then int2  int1 or "(int1+2)"  int2.
```(=>
(and
(instance ?INT1 Integer)
(instance ?INT2 Integer))
(not
(and
(lessThan ?INT2 ?INT1)
(lessThan
(PredecessorFn ?INT1)
?INT2))))```