Function Cons

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 cons} adds the object specified as its first argument to the front of the list specified as its second argument.

Axioms for Cons:

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

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


Equivalence Axioms mentioning Cons:

(<=> (Logterm@Ol-User%Kif-Meta ?X)
     (Or (Exists (?P1 ?T1)
                 (And (Sentence@Ol-User%Kif-Meta ?P1)
                      (Term@Ol-User%Kif-Meta ?T1)
                      (= ?X (Listof 'If ?P1 ?T1))))
         (Exists (?P1 ?T1 ?T2)
                 (And (Sentence@Ol-User%Kif-Meta ?P1)
                      (Term@Ol-User%Kif-Meta ?T1)
                      (Term@Ol-User%Kif-Meta ?T2)
                      (= ?X (Listof 'If ?P1 ?T1 ?T2))))
         (Exists (?Clist)
                 (And (List ?Clist)
                      (=> (Item ?C ?Clist)
                          (Exists (?P ?T)
                                  (And (Sentence@Ol-User%Kif-Meta ?P)
                                       (Term@Ol-User%Kif-Meta ?T)
                                       (= ?C (Listof ?P ?T)))))
                      (= ?X (Cons 'Cond ?Clist))))))

(<=> (Relsent@Ol-User%Kif-Meta ?X)
     (Exists (?R ?Tlist)
             (And (Or (Relconst@Ol-User%Kif-Meta ?R)
                      (Funconst@Ol-User%Kif-Meta ?R))
                  (List ?Tlist)
                  (>= (Length ?Tlist) 1)
                  (=> (Item ?T ?Tlist) (Term@Ol-User%Kif-Meta ?T))
                  (= ?X (Cons ?R ?Tlist)))))

(<=> (Conjunction@Ol-User%Kif-Meta ?X)
     (Exists (?Plist)
             (And (List ?Plist)
                  (>= (Length ?Plist) 1)
                  (=> (Item ?P ?Plist)
                      (Sentence@Ol-User%Kif-Meta ?P))
                  (= ?X (Cons 'And ?Plist)))))

(<=> (Disjunction@Ol-User%Kif-Meta ?X)
     (Exists (?Plist)
             (And (List ?Plist)
                  (>= (Length ?Plist) 1)
                  (=> (Item ?P ?Plist)
                      (Sentence@Ol-User%Kif-Meta ?P))
                  (= ?X (Cons 'Or ?Plist)))))

(<=> (Implication@Ol-User%Kif-Meta ?X)
     (Exists (?Plist)
             (And (List ?Plist)
                  (>= (Length ?Plist) 2)
                  (=> (Item ?P ?Plist)
                      (Sentence@Ol-User%Kif-Meta ?P))
                  (= ?X (Cons '=> ?Plist)))))