list concatenate fn (ListConcatenateFn)

A Function that returns the concatenation of the two Lists that are given as arguments. For example, the value of (ListConcatenateFn (ListFn Monday Tuesday) (ListFn Wednesday Thursday)) would be (ListFn Monday Tuesday Wednesday Thursday).

Ontology

SUMO / BASE-ONTOLOGY

Class(es)

Classe

inheritable relation

FunzioneBinaria

list concatenate fn

Coordinate term(s)

addition fn day fn density fn division fn edition fn exponentiation fn graph path fn hour fn intersection fn interval fn kappa fn list order fn log fn max fn maximal weighted path fn measure fn mereological difference fn mereological product fn mereological sum fn min fn minimal weighted path fn minute fn month fn multiplication fn periodical issue fn recurrent time interval fn relative complement fn relative time fn remainder fn second fn series volume fn speed fn subtraction fn temporal composition fn time interval fn union fn where fn

Type restrictions

Lista ListConcatenateFn(Lista, Lista)

Axioms (1)

list3 is uguale a "la lista composta di list1 e list2" se e solo se per ogni number1,number2 vale: se number1 é minore o uguale a "lunghezza di list1" e number2 é minore o uguale a "lunghezza di list2" e number1 é un' istanza di NumeroInteroPositivo e number2 é un' istanza di NumeroInteroPositivo, allora "number1th elemento di list3" is uguale a "number1th elemento di list1" e ""("lunghezza di list1"+number2"th elemento di list3" is uguale a "number2th elemento di list2".

(<=>
      (equal
            ?LIST3
            (ListConcatenateFn ?LIST1 ?LIST2))
      (forall
            (?NUMBER1 ?NUMBER2)
            (=>
                  (and
                        (lessThanOrEqualTo
                              ?NUMBER1
                              (ListLengthFn ?LIST1))
                        (lessThanOrEqualTo
                              ?NUMBER2
                              (ListLengthFn ?LIST2))
                        (instance ?NUMBER1 PositiveInteger)
                        (instance ?NUMBER2 PositiveInteger))
                  (and
                        (equal
                              (ListOrderFn ?LIST3 ?NUMBER1)
                              (ListOrderFn ?LIST1 ?NUMBER1))
                        (equal
                              (ListOrderFn
                                    ?LIST3
                                    (AdditionFn
                                          (ListLengthFn ?LIST1)
                                          ?NUMBER2))
                              (ListOrderFn ?LIST2 ?NUMBER2))))))