Relation Item

Instance-Of@Frame-Ontology: Binary-Relation@Ol-User%Kif-Relations, Relation@Ol-User%Kif-Relations, Set@Ol-User%Kif-Sets
Range@Frame-Ontology: List
Arity@Frame-Ontology: 2
The sentence {tt (item $tau_1$ $tau_2$)} is true if and only if the object denoted by $tau_2$ is a non-empty list and the object denoted by $tau_1$ is either the first item of that list or an item in the rest of the list.

Implication Axioms for Item:

(=> (Item ?X ?List) (Or (= ?X (First ?List)) (Item ?X (Rest ?List))))

Axioms for Item:

(Not (Null ?List))

Implication Axioms mentioning Item:

(=> (= (Union@Ol-User%Kif-Sets @Sets) ?Set)
    (=> (Item ?S (Listof @Sets)) (Set@Ol-User%Kif-Sets ?S)))

(=> (= (Intersection@Ol-User%Kif-Sets @Sets) ?Set)
    (=> (Item ?S (Listof @Sets)) (Set@Ol-User%Kif-Sets ?S)))

(=> (= (Difference@Ol-User%Kif-Sets ?Set @Sets) ?Diff-Set)
    (=> (Item ?S (Listof @Sets)) (Set@Ol-User%Kif-Sets ?S)))

(=> (Item ?R ?List-Of-Relations)
    (Binary-Relation@Ol-User%Kif-Relations ?R))

(=> (= (Compose@Frame-Ontology @Binary-Relations) ?Composed-Relation)
    (Forall (?R)
            (=> (Item ?R (Listof @Binary-Relations))
                (Binary-Relation@Ol-User%Kif-Relations ?R))))

Equivalence Axioms mentioning Item:

(<=> (Pairwise-Disjoint@Ol-User%Kif-Sets @Sets)
     (Forall (?S1 ?S2)
             (=> (Item ?S1 (Listof @Sets))
                 (Item ?S2 (Listof @Sets))
                 (Or (= ?S1 ?S2) (Disjoint@Ol-User%Kif-Sets ?S1 ?S2)))))

(<=> (Composition-Of@Frame-Ontology ?Binary-Relation
     (And (Binary-Relation@Ol-User%Kif-Relations ?Binary-Relation)
          (List ?List-Of-Relations)
          (Not (Null ?List-Of-Relations))
          (=> (Item ?R ?List-Of-Relations)
              (Binary-Relation@Ol-User%Kif-Relations ?R))
          (Or (And (Single ?List-Of-Relations)
                   (= ?Binary-Relation (First ?List-Of-Relations)))
              (And (Double ?List-Of-Relations)
                   (= ?Binary-Relation
                          (First (Rest ?List-Of-Relations))
                          (First ?List-Of-Relations))))
                  (And (= ?Binary-Relation
                              (Last ?List-Of-Relations)
                           (Butlast ?List-Of-Relations)))))))

(<=> (Relation-Universe@Frame-Ontology ?Relation)
     (And (Relation@Ol-User%Kif-Relations ?Relation)
          (Class@Frame-Ontology ?Type-Class)
          (Forall (?X)
                  (<=> (Exists (?Tuple)
                               (And (Member@Ol-User%Kif-Sets ?Tuple
                                    (Item ?X ?Tuple)))
                       (Instance-Of@Frame-Ontology ?X ?Type-Class)))))

(<=> (Expression@Ol-User%Kif-Meta ?Expr)
     (Or (Word@Ol-User%Kif-Meta ?Expr)
         (And (List ?Expr)
              (Forall (?Subexpr)
                      (=> (Item ?Subexpr ?Expr)
                          (Expression@Ol-User%Kif-Meta ?Subexpr))))))

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