Function REST

• Defined in theory: Kif-lists
• Source code: kif-lists.lisp

Slots on this function:

Instance-Of: Function

Arity: 2

Equivalence Axioms:

(<=> (Rest ?List)
     (Or (And (Null ?List) (= ?Rest-List ?List))
         (Exists (?X @Items)
                 (And (= ?List (Listof ?X @Items))
                      (= ?Rest-List (Listof @Items))))))

Other Related Axioms:

(=> (= (Rest ?List) ?Rest-List)
    (Or (And (Null ?List) (= ?Rest-List ?List))
        (Exists (?X @Items)
                (And (= ?List (Listof ?X @Items))
                     (= ?Rest-List (Listof @Items))))))

(<- (Last ?List)
    (Cond ((Null ?List) Bottom)
          ((Null (Rest ?List)) (First ?List))
          (True (Last (Rest ?List)))))

(<- (Butlast ?List)
    (Cond ((Null ?List) Bottom)
          ((Null (Rest ?List)) Nil)
          (True (Cons (First ?List) (Butlast (Rest ?List))))))

(=> (Item ?X ?List)
    (And (Not (Null ?List))
         (Or (= ?X (First ?List)) (Item ?X (Rest ?List)))))

(=> (Sublist ?L1 ?L2) (Or (= ?L1 ?L2) (Sublist ?L1 (Rest ?L2))))

(<- (Append ?L1 ?L2)
    (If (Null ?L1)
        (If (List ?L2) ?L2)
        (Cons (First ?L1) (Append (Rest ?L1) ?L2))))

(<- (Revappend ?L1 ?L2)
    (If (Null ?L1)
        (If (List ?L2) ?L2)
        (Revappend (Rest ?L1) (Cons (First ?L1) ?L2))))

(<- (Remove ?X ?List)
    (Cond ((Null ?List) Nil)
          ((And (= ?X (First ?List)) (List ?List))
           (Remove ?X (Rest ?List)))
          ((List ?List) (Cons ?X (Remove ?X (Rest ?List))))))

(<- (Subst ?X ?Y ?Z)
    (Cond ((= ?Y ?Z) ?X)
          ((Null ?Z) Nil)
          ((List ?Z)
           (Cons (Subst ?X ?Y (First ?Z)) (Subst ?X ?Y (Rest ?Z))))
          (True ?Z)))

(<- (Length ?List)
    (Cond ((Null ?List) 0) ((List ?List) (1+ (Length (Rest ?List))))))

(<- (Nth ?List ?N)
    (Cond ((= ?N 1) (First ?List))
          ((Positive ?N) (Nth (Rest ?List) (1- ?N)))))

(<- (Nthrest ?List ?N)
    (Cond ((= ?N 0) (If (List ?List) ?List))
          ((Positive ?N) (Nthrest (Rest ?List) (1- ?N)))))