successor fn (SuccessorFn)

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

Ontologie

SUMO / NUMERIC-FUNCTIONS

Class(es)

třída

inheritable relation

unární funkce

successor fn

Související termín(y)

absolute value fn abstraction fn arc cosine fn arc sine fn arc tangent fn back fn begin fn begin node fn cardinality fn ceiling fn complement fn cosine fn cut set fn denominator fn end fn end node fn extension fn floor fn front fn future fn generalized intersection fn generalized union fn giga fn imaginary part fn immediate future fn immediate past fn initial node fn integer square root fn kilo fn list length fn magnitude fn mega fn micro fn milli fn minimal cut set fn nano fn numerator fn organization fn past fn path weight fn pico fn power set fn predecessor fn principal host fn probability fn property fn rational number fn real number fn reciprocal fn round fn signum fn sine fn skin fn square root fn tangent fn tera fn terminal node fn wealth fn when fn year fn

Typy argumentů

celé číslo SuccessorFn(celé číslo)

Axiomy (8)

"length of "(,item)"" se rovná "("length of "()""+1)".

(equal
      (ListLengthFn
            (ListFn @ROW ?ITEM))
      (SuccessorFn
            (ListLengthFn
                  (ListFn @ROW))))

Jestliže "length of list1" se rovná number, potom existuje list2 tak, že list1 starts list2 a "(number+1)" se rovná "length of list2" a ""(number+1)"th element of list2" se rovná item.

(=>
      (equal
            (ListLengthFn ?LIST1)
            ?NUMBER)
      (exists
            (?LIST2)
            (and
                  (initialList ?LIST1 ?LIST2)
                  (equal
                        (SuccessorFn ?NUMBER)
                        (ListLengthFn ?LIST2))
                  (equal
                        (ListOrderFn
                              ?LIST2
                              (SuccessorFn ?NUMBER))
                        ?ITEM))))

"(number+1)" se rovná "(number+)".

(equal
      (SuccessorFn ?NUMBER)
      (AdditionFn ?NUMBER 1))

Jestliže "(int1+1)" se rovná "(int2+1)", potom int1 se rovná int2.

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

Jestliže int je instancí třídy celé číslo, potom int je menší než "(int+1)".

(=>
      (instance ?INT Integer)
      (lessThan
            ?INT
            (SuccessorFn ?INT)))

Jestliže int1 je instancí třídy celé číslo a int2 je instancí třídy celé číslo, potom int1 není menší než int2 nebo int2 není menší než "(int1+1)".

(=>
      (and
            (instance ?INT1 Integer)
            (instance ?INT2 Integer))
      (not
            (and
                  (lessThan ?INT1 ?INT2)
                  (lessThan
                        ?INT2
                        (SuccessorFn ?INT1)))))

Jestliže int je instancí třídy celé číslo, potom int se rovná "("(int+2)"+1)".

(=>
      (instance ?INT Integer)
      (equal
            ?INT
            (SuccessorFn
                  (PredecessorFn ?INT))))

Jestliže int je instancí třídy celé číslo, potom int se rovná "("(int+1)"+2)".

(=>
      (instance ?INT Integer)
      (equal
            ?INT
            (PredecessorFn
                  (SuccessorFn ?INT))))