Function Append

Instance-Of@Frame-Ontology: Function@Ol-User%Kif-Relations, Relation@Ol-User%Kif-Relations, Set@Ol-User%Kif-Sets
Arity@Frame-Ontology: 3
Documentation@Ol%Frame-Ontology:
The function {tt append} adds the items in the list specified as its first argument to the list specified as its second argument. .

Axioms for Append:

(Nth-Domain@Frame-Ontology Append 3 List)

(Nth-Domain@Frame-Ontology Append 2 List)

(Nth-Domain@Frame-Ontology Append 1 List)


Equivalence Axioms mentioning Append:

(<=> (Quanterm@Ol-User%Kif-Meta ?X)
     (Or (Exists (?T ?P)
                 (And (Term@Ol-User%Kif-Meta ?T)
                      (Sentence@Ol-User%Kif-Meta ?P)
                      (= ?X (Listof 'The ?T ?P))))
         (Exists (?T ?P)
                 (And (Term@Ol-User%Kif-Meta ?T)
                      (Sentence@Ol-User%Kif-Meta ?P)
                      (= ?X (Listof 'Setofall ?T ?P))))
         (Exists (?Vlist ?P)
                 (And (List ?Vlist)
                      (Sentence@Ol-User%Kif-Meta ?P)
                      (>= (Length ?Vlist) 1)
                      (=> (Item ?V ?Vlistp)
                          (Indvar@Ol-User%Kif-Meta ?V))
                      (= ?X (Listof 'Kappa ?Vlistp ?P))))
         (Exists (?Vlist ?Sv ?P)
                 (And (List ?Vlist)
                      (Seqvar@Ol-User%Kif-Meta ?Sv)
                      (Sentence@Ol-User%Kif-Meta ?P)
                      (=> (Item ?V ?Vlist)
                          (Indvar@Ol-User%Kif-Meta ?V))
                      (= ?X
                         (Listof 'Kappa
                                 (Append ?Vlist (Listof ?Sv))
                                 ?P))))
         (Exists (?Vlist ?T)
                 (And (List ?Vlist)
                      (Term@Ol-User%Kif-Meta ?T)
                      (>= (Length ?Vlist) 1)
                      (=> (Item ?V ?Vlistp)
                          (Indvar@Ol-User%Kif-Meta ?V))
                      (= ?X (Listof 'Lambda ?Vlistp ?T))))
         (Exists (?Vlist ?Sv ?T)
                 (And (List ?Vlist)
                      (Seqvar@Ol-User%Kif-Meta ?Sv)
                      (Sentence@Ol-User%Kif-Meta ?T)
                      (=> (Item ?V ?Vlist)
                          (Indvar@Ol-User%Kif-Meta ?V))
                      (= ?X
                         (Listof 'Lambda
                                 (Append ?Vlist (Listof ?Sv))
                                 ?T))))))