(<=> (>= ?X ?Y) (Or (> ?X ?Y) (= ?X ?Y)))
(=> (Nonnegative-Integer ?X) (>= ?X 0))
(=> (Non-Negative-Integer@Kif-Extensions ?X) (>= ?X 0))
(=> (Nth-Domain@Frame-Ontology ?Relation ?N ?Type)
(Forall
(?Tuple)
(=> (Member@Ol-User%Kif-Sets ?Tuple ?Relation)
(And (>= (Length@Ol-User%Kif-Lists ?Tuple) ?N)
(Instance-Of@Frame-Ontology
(Nth@Ol-User%Kif-Lists ?Tuple ?N)
?Type)))))
(=> (Minimum-Value-Cardinality@Frame-Ontology ?Instance
?Binary-Relation
?N)
(>= (Value-Cardinality@Frame-Ontology ?Instance ?Binary-Relation)
?N))
(=> (Has-At-Least@Ol-User%Slot-Constraint-Sugar ?Instance
?Binary-Relation
?N)
(>= (Value-Cardinality@Frame-Ontology ?Instance ?Binary-Relation)
?N))
(<=> (Non-Negative-Integer@Kif-Extensions ?X)
(And (Integer ?X) (>= ?X 0)))
(<=> (Nth-Domain@Frame-Ontology ?Relation ?N ?Type)
(And (Defined@Ol-User%Kif-Extensions
(Arity@Frame-Ontology ?Relation))
(Positive-Integer@Ol-User%Kif-Extensions ?N)
(Class@Frame-Ontology ?Type)
(Forall
(?Tuple)
(=> (Member@Ol-User%Kif-Sets ?Tuple ?Relation)
(And (>= (Length@Ol-User%Kif-Lists ?Tuple) ?N)
(Instance-Of@Frame-Ontology
(Nth@Ol-User%Kif-Lists ?Tuple ?N)
?Type))))))
(<=> (Minimum-Value-Cardinality@Frame-Ontology ?Instance
?Binary-Relation
?N)
(And (Binary-Relation@Ol-User%Kif-Relations ?Binary-Relation)
(Nonnegative-Integer ?N)
(>= (Value-Cardinality@Frame-Ontology ?Instance
?Binary-Relation)
?N)))
(<=> (Minimum-Slot-Cardinality@Frame-Ontology ?Domain-Class
?Relation
?N)
(=> (Instance-Of@Frame-Ontology ?Instance ?Domain-Class)
(>= (Value-Cardinality@Frame-Ontology ?Instance ?Relation)
?N)))
(<=> (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@Ol-User%Kif-Lists ?Vlist)
(Sentence@Ol-User%Kif-Meta ?P)
(>= (Length@Ol-User%Kif-Lists ?Vlist) 1)
(=> (Item@Ol-User%Kif-Lists ?V ?Vlistp)
(Indvar@Ol-User%Kif-Meta ?V))
(= ?X (Listof 'Kappa ?Vlistp ?P))))
(Exists (?Vlist ?Sv ?P)
(And (List@Ol-User%Kif-Lists ?Vlist)
(Seqvar@Ol-User%Kif-Meta ?Sv)
(Sentence@Ol-User%Kif-Meta ?P)
(=> (Item@Ol-User%Kif-Lists ?V ?Vlist)
(Indvar@Ol-User%Kif-Meta ?V))
(= ?X
(Listof 'Kappa
(Append@Ol-User%Kif-Lists ?Vlist
(Listof ?Sv))
?P))))
(Exists (?Vlist ?T)
(And (List@Ol-User%Kif-Lists ?Vlist)
(Term@Ol-User%Kif-Meta ?T)
(>= (Length@Ol-User%Kif-Lists ?Vlist) 1)
(=> (Item@Ol-User%Kif-Lists ?V ?Vlistp)
(Indvar@Ol-User%Kif-Meta ?V))
(= ?X (Listof 'Lambda ?Vlistp ?T))))
(Exists (?Vlist ?Sv ?T)
(And (List@Ol-User%Kif-Lists ?Vlist)
(Seqvar@Ol-User%Kif-Meta ?Sv)
(Sentence@Ol-User%Kif-Meta ?T)
(=> (Item@Ol-User%Kif-Lists ?V ?Vlist)
(Indvar@Ol-User%Kif-Meta ?V))
(= ?X
(Listof 'Lambda
(Append@Ol-User%Kif-Lists ?Vlist
(Listof ?Sv))
?T))))))
(>= (Value-Cardinality@Frame-Ontology ?Instance ?Binary-Relation) 1)