		Search-engine friendly clone of the ACL2 documentation.

Previous-subsumer-hints

Hints to prove a theorem directly from previously-proved theorems.

General Form:
(previous-subsumer-hints term wrld)

where term is a translated term (see term) and wrld is a logical world, such as (w state). See defthm<w for an explanation of what this function returns: in short, it either returns nil or suitable hints for proving term. Here is a log that illustrates this function.

ACL2 !>(previous-subsumer-hints '(equal (car (cons u v)) u) (w state))
(:BY CAR-CONS
     :DO-NOT *ALL-BUT-SIMPLIFY*)
ACL2 !>:trans (and (equal (car (cons u v)) u)
                   (equal (cdr (cons a b)) b))

(IF (EQUAL (CAR (CONS U V)) U)
    (EQUAL (CDR (CONS A B)) B)
    'NIL)

=> *

ACL2 !>(previous-subsumer-hints '(IF (EQUAL (CAR (CONS U V)) U)
                                     (EQUAL (CDR (CONS A B)) B)
                                     'NIL)
                                 (w state))
(:USE ((:INSTANCE CAR-CONS (Y V) (X U))
       (:INSTANCE CDR-CONS (Y B) (X A)))
      :IN-THEORY (THEORY 'MINIMAL-THEORY)
      :DO-NOT *ALL-BUT-SIMPLIFY*)
ACL2 !>