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

**has axiom** (=> (*and* (*instance* ?INT1 Integer) (*instance* ?INT2 Integer)) (*not* (*and* (*lessThan* ?INT2 ?INT1) (*lessThan* (*PredecessorFn* ?INT1) ?INT2))))
| |

**has axiom** (=> (*equal* (*PredecessorFn* ?INT1) (*PredecessorFn* ?INT2)) (*equal* ?INT1 ?INT2))
| |

**has axiom** (=> (*instance* ?INT Integer) (*equal* ?INT (*SuccessorFn* (*PredecessorFn* ?INT))))
| |

**has axiom** (=> (*instance* ?INT Integer) (*equal* ?INT (*PredecessorFn* (*SuccessorFn* ?INT))))
| |

**has axiom** (=> (*instance* ?INT Integer) (*greaterThan* ?INT (*PredecessorFn* ?INT)))
| |

**has domain1** Integer | |

**has ***range* Integer | |

**is an ***instance* of UnaryFunction | |

BinaryRelation | **is first ***domain* of *DomainFn* | |

**is first ***domain* of *equivalenceRelationOn* | |

**is first ***domain* of *inverse* | |

**is first ***domain* of *irreflexiveOn* | |

**is first ***domain* of *partialOrderingOn* | |

**is first ***domain* of *RangeFn* | |

**is first ***domain* of *reflexiveOn* | |

**is first ***domain* of *totalOrderingOn* | |

**is first ***domain* of *trichotomizingOn* | |

**is second ***domain* of *inverse* | |

Function | **is first ***domain* of *AssignmentFn* | |

**is first ***domain* of *closedOn* | |

**is first ***domain* of *range* | |

**is first ***domain* of *rangeSubclass* | |

Class | **is third ***domain* of *domain* | |

**is third ***domain* of *domainSubclass* | |

Abstract | **is ***disjoint* from Physical | |