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

Class(es)

贺摸
is instance of
  膥┯闽玒  
is instance of
  じㄧ计  
is instance of
  玡计ㄧ计  

Coordinate term(s)

荡癸ㄧ计  磞瓃ㄧ计  ┓緇┒  ┓タ┒  ┓タち  はㄧ计  丁秨﹍ㄧ计  程竊翴ㄧ计  璸计ㄧ计  ㄧ计  が干ㄧ计  緇┒ㄧ计  ユ隔畖ㄧ计  虫ㄧ计  丁挡ㄧΑ  程竊翴ㄧ计  絛瞅ㄧ计  ㄧ计  タㄧ计  丁ゼㄓㄧΑ  阀てㄧ计  阀て羛栋ㄧ计  货璸ㄧ计  店计ㄧ计  程ゼㄓ丁ㄧ计  程筁丁ㄧ计  癬﹍竊翴ㄧ计  俱计キよㄧ计  璸ㄧ计  ㄧ计  计ㄧ计  κ窾璸ㄧ计  κ窾だぇ璸ㄧ计  だぇ璸ㄧ计  程ユ隔畖ㄧ计  ーμㄧ计  だㄧ计  舱麓ㄧ计  筁丁ㄧΑ  隔畖秖ㄧ计  だぇ璸ㄧ计  经栋ㄧ计  砰ㄧ计  ┪礛瞯ㄧ计  疭┦ㄧ计  Τ瞶计ㄧ计  龟计ㄧ计  计ㄧ计  俱计ㄧ计  タ璽腹ㄧ计  タ┒ㄧ计  ブㄧ计  キよㄧ计  计ㄧ计  タちㄧ计  璸ㄧ计  沧竊翴ㄧ计  癩玻ㄧ计  丁ㄧ计  ㄧ计 

Type restrictions

俱计 PredecessorFn(俱计)

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))))