proof-builder-b

(in-package "ACL2")

(defmacro install-new-pc-meta-or-macro
  (command-type raw-name name formals doc body)
  `(progn ,(PC-META-OR-MACRO-DEFUN RAW-NAME NAME FORMALS DOC BODY)
    (add-pc-command ,NAME ',COMMAND-TYPE)))

(defun define-pc-meta-or-macro-fn
  (command-type raw-name formals body)
  (let ((name (make-official-pc-command raw-name)))
    `(install-new-pc-meta-or-macro ,COMMAND-TYPE
      ,RAW-NAME
      ,NAME
      ,FORMALS
      nil
      ,BODY)))

(defmacro define-pc-meta
  (raw-name formals &rest body)
  (define-pc-meta-or-macro-fn 'meta raw-name formals body))

(defmacro define-pc-macro
  (raw-name formals &rest body)
  (define-pc-meta-or-macro-fn 'macro raw-name formals body))

(defmacro define-pc-atomic-macro
  (raw-name formals &rest body)
  (define-pc-meta-or-macro-fn 'atomic-macro
    raw-name
    formals
    body))

(defmacro toggle-pc-macro
  (name &optional new-tp)
  (declare (xargs :guard (and (symbolp new-tp)
        (or (null new-tp)
          (member-equal (symbol-name new-tp)
            '("MACRO" "ATOMIC-MACRO"))))))
  `(toggle-pc-macro-fn ',(MAKE-OFFICIAL-PC-COMMAND NAME)
    ',NEW-TP
    state))

(defmacro define-pc-primitive
  (raw-name formals &rest body)
  (let ((name (make-official-pc-command raw-name)))
    `(progn ,(PC-PRIMITIVE-DEFUN-FORM RAW-NAME NAME FORMALS NIL BODY)
      (add-pc-command ,NAME 'primitive))))

(define-pc-primitive comment
  (&rest x)
  (declare (ignore x))
  (mv pc-state state))

(defun non-bounded-nums
  (nums lower upper)
  (declare (xargs :guard (and (rationalp lower) (rationalp upper) (true-listp nums))))
  (if (consp nums)
    (if (and (integerp (car nums))
        (<= lower (car nums))
        (<= (car nums) upper))
      (non-bounded-nums (cdr nums) lower upper)
      (cons (car nums) (non-bounded-nums (cdr nums) lower upper)))
    nil))

(defun delete-by-position
  (lst current-index nums)
  (declare (xargs :guard (and (true-listp nums) (integerp current-index))))
  (if (consp lst)
    (if (member current-index nums)
      (delete-by-position (cdr lst) (1+ current-index) nums)
      (cons (car lst)
        (delete-by-position (cdr lst) (1+ current-index) nums)))
    nil))

(define-pc-primitive drop
  (&rest nums)
  (if nums
    (let ((bad-nums (non-bounded-nums nums 1 (length hyps))))
      (if bad-nums
        (print-no-change2 "The following are not in-range hypothesis numbers:  ~&0."
          (list (cons #\0 bad-nums)))
        (mv (change-pc-state pc-state
            :goals (cons (change goal
                (car goals)
                :hyps (delete-by-position hyps 1 nums))
              (cdr goals)))
          state)))
    (if hyps
      (mv (change-pc-state pc-state
          :goals (cons (change goal (car goals) :hyps nil) (cdr goals)))
        state)
      (print-no-change2 "There are no hypotheses to drop!"))))

(define-pc-meta lisp
  (form)
  (cond ((not (f-get-global 'in-verify-flg state)) (er soft
        'lisp
        "You may only invoke the proof-builder LISP command when ~
              you are inside the interactive loop."))
    ((and (symbolp form)
       (or (eq form t) (eq form nil) (keywordp form))) (value form))
    (t (mv-let (erp stobjs-out/vals state)
        (trans-eval-default-warning form :lisp state t)
        (let ((stobjs-out (car stobjs-out/vals)) (vals (cdr stobjs-out/vals)))
          (if (equal stobjs-out *error-triple-sig*)
            (mv (or erp (car vals)) (cadr vals) state)
            (mv erp vals state)))))))

(define-pc-primitive fail-primitive
  nil
  (declare (ignore pc-state))
  (mv nil state))

(define-pc-macro fail
  (&optional hard)
  (if hard
    (value '(lisp (mv hard nil state)))
    (value 'fail-primitive)))

(define-pc-macro illegal
  (instr)
  (pprogn (print-no-change "Illegal interactive instruction, ~x0.~%  An instruction must be a ~
                            symbol or a proper list headed by a symbol."
      (list (cons #\0 instr)))
    (value :fail)))

(defun chk-assumption-free-ttree-1
  (ttree ctx)
  (cond ((tagged-objectsp 'assumption ttree) (er hard
        ctx
        "The 'assumption ~x0 was found in the final ttree!"
        (car (tagged-objects 'assumption ttree))))
    ((tagged-objectsp 'fc-derivation ttree) (er hard
        ctx
        "The 'fc-derivation ~x0 was found in the final ttree!"
        (car (tagged-objects 'fc-derivation ttree))))
    (t t)))

(defun put-cdr-assoc-query-id
  (id val alist)
  (cond ((atom alist) (cons (cons id val) alist))
    ((eq id (caar alist)) (cons (cons id val) (cdr alist)))
    (t (cons (car alist)
        (put-cdr-assoc-query-id id val (cdr alist))))))

(defun set-query-val
  (id val state)
  (let ((alist (ld-query-control-alist state)))
    (set-ld-query-control-alist (put-cdr-assoc-query-id id
        (if (eq val 'toggle)
          (not (cdr-assoc-query-id id alist))
          val)
        alist)
      state)))

(defmacro query-on-exit
  (&optional (val 'toggle))
  `(set-query-val 'exit ',VAL state))

(defun replay-query
  (state)
  (acl2-query 'exit
    '("~%Do you want to submit this event?  Possible replies are:~%~
                         Y (Yes), R (yes and Replay commands), N (No, but exit), A (Abort exiting).~|~ " :y :y :r :r :n :n :a :a)
    nil
    state))

(define-pc-meta exit
  (&optional event-name rule-classes do-it-flg)
  (if (not (f-get-global 'in-verify-flg state))
    (er soft
      'exit
      "You may not invoke the EXIT command unless inside the ~
           interactive loop.")
    (if args
      (let* ((event-name-and-types-and-raw-term (event-name-and-types-and-raw-term state-stack)) (event-name (or event-name (car event-name-and-types-and-raw-term)))
          (instructions (instructions-of-state-stack state-stack nil)))
        (er-let* ((event-name (if event-name
               (value event-name)
               (pprogn (io? proof-builder
                   nil
                   state
                   nil
                   (fms0 "Please supply an event name (or :A to ~
                                   abort)~%>> "))
                 (read-object *standard-oi* state)))))
          (if (eq event-name :a)
            (pprogn (io? proof-builder nil state nil (fms0 "~|Exit aborted.~%"))
              (mv nil nil state))
            (if (null (goals t))
              (let* ((rule-classes (if (consp (cdr args))
                     rule-classes
                     (if (and (consp args) (eq (car args) nil))
                       (cadr event-name-and-types-and-raw-term)
                       '(:rewrite)))) (event-form `(defthm ,EVENT-NAME
                      ,(CADDR EVENT-NAME-AND-TYPES-AND-RAW-TERM)
                      ,@(IF (EQUAL RULE-CLASSES '(:REWRITE))
      NIL
      (LIST :RULE-CLASSES RULE-CLASSES))
                      :instructions ,INSTRUCTIONS)))
                (mv-let (erp stobjs-out/vals state)
                  (pprogn (print-pc-defthm event-form state)
                    (mv-let (erp ans state)
                      (cond (do-it-flg (value :y))
                        ((eq event-name t) (value :n))
                        (t (replay-query state)))
                      (declare (ignore erp))
                      (case ans
                        (:y (trans-eval-default-warning event-form
                            'exit
                            state
                            t))
                        (:r (pprogn (state-from-instructions (caddr event-form)
                              event-name
                              rule-classes
                              instructions
                              '(signal value)
                              state)
                            (trans-eval-default-warning event-form
                              'exit
                              state
                              t)))
                        (:a (mv t '(nil . t) state))
                        (otherwise (mv t '(nil) state)))))
                  (if (or erp (null (car stobjs-out/vals)))
                    (if (eq (cdr stobjs-out/vals) t)
                      (pprogn (io? proof-builder nil state nil (fms0 "~|Exit aborted.~%"))
                        (mv nil nil state))
                      (mv *pc-complete-signal* nil state))
                    (mv *pc-complete-signal* event-name state))))
              (pprogn (io? proof-builder
                  nil
                  state
                  (instructions event-name-and-types-and-raw-term state-stack)
                  (fms0 "~%Not exiting, as there remain unproved ~
                                   goals:  ~&0.~%The original goal is:~%~ ~ ~ ~
                                   ~ ~y1~|  Here is the current instruction ~
                                   list, starting with the first:~%~ ~ ~ ~ ~
                                   ~y2~|"
                    (list (cons #\0 (goal-names (goals t)))
                      (cons #\1 (caddr event-name-and-types-and-raw-term))
                      (cons #\2 instructions))))
                (mv nil nil state))))))
      (pprogn (io? proof-builder nil state nil (fms0 "~|Exiting....~%"))
        (mv *pc-complete-signal* nil state)))))

(define-pc-meta undo
  (&optional n)
  (if (and args (not (and (integerp n) (< 0 n))))
    (pprogn (print-no-change "The optional argument to undo must be a positive integer.")
      (mv nil nil state))
    (let ((m (min (or n 1) (1- (length state-stack)))))
      (if (null (cdr state-stack))
        (pprogn (print-no-change "Already at the start.")
          (mv nil nil state))
        (pprogn (pc-assign old-ss state-stack)
          (io? proof-builder
            nil
            state
            (state-stack m)
            (fms0 "~|Undoing:  ~y0~|"
              (list (cons #\0
                  (access pc-state
                    (car (nthcdr (1- m) state-stack))
                    :instruction)))))
          (pc-assign state-stack (nthcdr m state-stack))
          (if (consp (cdr (state-stack)))
            state
            (io? proof-builder
              nil
              state
              nil
              (fms0 "Back to the start.~%")))
          (mv nil t state))))))

(define-pc-meta restore
  nil
  (let ((old-ss (pc-value old-ss)))
    (if (null old-ss)
      (pprogn (io? proof-builder
          nil
          state
          nil
          (fms0 "~%Nothing to restore from!~%"))
        (mv nil nil state))
      (let ((saved-ss state-stack))
        (pprogn (pc-assign state-stack old-ss)
          (pc-assign old-ss saved-ss)
          (mv nil t state))))))

(defun print-commands
  (indexed-instrs state)
  (if (null indexed-instrs)
    state
    (if (null (caar indexed-instrs))
      (io? proof-builder
        nil
        state
        (indexed-instrs)
        (fms0 (car (cdar indexed-instrs))
          (cdr (cdar indexed-instrs))))
      (pprogn (io? proof-builder
          nil
          state
          (indexed-instrs)
          (fms0 "~|~x0. ~y1~|"
            (list (cons #\0 (caar indexed-instrs))
              (cons #\1 (cdar indexed-instrs)))))
        (print-commands (cdr indexed-instrs) state)))))

(defun make-pretty-start-instr
  (state-stack)
  (let* ((triple (event-name-and-types-and-raw-term state-stack)) (name (car triple))
      (types (cadr triple)))
    (if name
      (list "~|[started with (~x0 ~x1 ...)]~%"
        (cons #\0 name)
        (cons #\1 types))
      (list "~|<< no event name specified at start >>~%"))))

(defun raw-indexed-instrs
  (start-index finish-index state-stack)
  (declare (xargs :guard (and (integerp start-index)
        (integerp finish-index)
        (<= start-index finish-index)
        (true-listp state-stack))))
  (if (< start-index finish-index)
    (cons (cons start-index
        (access pc-state (car state-stack) :instruction))
      (raw-indexed-instrs (1+ start-index)
        finish-index
        (cdr state-stack)))
    (if (cdr state-stack)
      (list (cons start-index
          (access pc-state (car state-stack) :instruction)))
      (list (cons nil (make-pretty-start-instr state-stack))))))

(define-pc-macro sequence-no-restore
  (instr-list)
  (value `(sequence ,INSTR-LIST nil nil nil nil t)))

(define-pc-macro skip
  nil
  (value '(sequence-no-restore nil)))

(defmacro define-pc-help
  (name args &rest body)
  `(define-pc-macro ,NAME
    ,ARGS
    ,@(BUTLAST BODY 1)
    (pprogn ,(CAR (LAST BODY)) (value 'skip))))

(defun evisc-indexed-instrs-1
  (name rev-indexed-instrs)
  (if (consp rev-indexed-instrs)
    (let ((instr (cdr (car rev-indexed-instrs))))
      (case-match instr
        ((comm ':end x . &) (if (and (eq comm (make-pretty-pc-command :comment))
              (equal x name))
            rev-indexed-instrs
            (evisc-indexed-instrs-1 name (cdr rev-indexed-instrs))))
        (& (evisc-indexed-instrs-1 name (cdr rev-indexed-instrs)))))
    nil))

(defun evisc-indexed-instrs-rec
  (rev-indexed-instrs)
  (if (consp rev-indexed-instrs)
    (let ((instr (cdr (car rev-indexed-instrs))) (evisc-cdr (evisc-indexed-instrs-rec (cdr rev-indexed-instrs))))
      (case-match instr
        ((comm ':begin name . &) (if (eq comm (make-pretty-pc-command :comment))
            (let ((rst (evisc-indexed-instrs-1 name evisc-cdr)))
              (if rst
                (cons (cons (car (car rev-indexed-instrs))
                    (cons "***HIDING***" instr))
                  (cdr rst))
                (cons (car rev-indexed-instrs) evisc-cdr)))
            (cons (car rev-indexed-instrs) evisc-cdr)))
        (& (cons (car rev-indexed-instrs) evisc-cdr))))
    nil))

(defun mark-unfinished-instrs
  (indexed-instrs)
  (if (consp indexed-instrs)
    (let ((instr (cdr (car indexed-instrs))))
      (case-match instr
        ((comm ':begin & . &) (if (eq comm (make-pretty-pc-command :comment))
            (cons (cons (car (car indexed-instrs))
                (cons "***UNFINISHED***" instr))
              (mark-unfinished-instrs (cdr indexed-instrs)))
            (cons (car indexed-instrs)
              (mark-unfinished-instrs (cdr indexed-instrs)))))
        (& (cons (car indexed-instrs)
            (mark-unfinished-instrs (cdr indexed-instrs))))))
    nil))

(defun evisc-indexed-instrs
  (indexed-instrs)
  (mark-unfinished-instrs (reverse (evisc-indexed-instrs-rec (reverse indexed-instrs)))))

(define-pc-help commands
  (&optional n evisc-p)
  (if (and n (not (and (integerp n) (> n 0))))
    (io? proof-builder
      nil
      state
      (n)
      (fms0 "*** The first optional argument to the COMMANDS command must ~
                  be a positive integer, but ~x0 is not.~|"
        (list (cons #\0 n))))
    (let* ((indexed-instrs (raw-indexed-instrs 1
           (if n
             (min n (length state-stack))
             (length state-stack))
           state-stack)))
      (print-commands (if evisc-p
          (evisc-indexed-instrs indexed-instrs)
          indexed-instrs)
        state))))

(define-pc-macro comm
  (&optional n)
  (value (list 'commands n t)))

(defun promote-guts
  (pc-state goals hyps x y no-flatten-flg)
  (change-pc-state pc-state
    :goals (cons (change goal
        (car goals)
        :hyps (append hyps
          (if no-flatten-flg
            (list x)
            (flatten-ands-in-lit x)))
        :conc y)
      (cdr goals))))

(define-pc-primitive promote
  (&optional do-not-flatten-flag)
  (if current-addr
    (print-no-change2 "You must be at the top ~
                         of the goal in order to promote the ~
                         antecedents of an implication. Try TOP first.")
    (case-match conc
      (('implies x y) (mv (promote-guts pc-state goals hyps x y do-not-flatten-flag)
          state))
      (('if x y *t*) (mv (promote-guts pc-state goals hyps x y do-not-flatten-flag)
          state))
      (& (print-no-change2 "The goal must be of the form ~x0 or ~x1."
          (list (cons #\0 '(implies p q))
            (cons #\1
              '(if p
                q
                t))))))))

(defun remove-by-indices
  (m indices lst)
  (if (consp lst)
    (if (member-equal m indices)
      (remove-by-indices (1+ m) indices (cdr lst))
      (cons (car lst)
        (remove-by-indices (1+ m) indices (cdr lst))))
    nil))

(define-pc-macro print
  (form &optional without-evisc)
  (let ((print-form `(fms0 "~|~y0~|" (list (cons #\0 ,FORM)))))
    (value `(lisp ,(IF WITHOUT-EVISC
     `(WITHOUT-EVISC ,PRINT-FORM)
     PRINT-FORM)))))

(defun fetch-term-and-cl
  (term addr cl)
  (declare (xargs :guard (bounded-integer-listp 1 'infinity addr)))
  (cond ((eq cl t) (mv nil t))
    ((null addr) (mv term cl))
    ((or (variablep term) (fquotep term)) (mv nil t))
    ((and (integerp (car addr))
       (< 0 (car addr))
       (< (car addr) (length term))) (case-match term
        (('if t1 t2 t3) (cond ((= 1 (car addr)) (fetch-term-and-cl t1 (cdr addr) cl))
            ((= 2 (car addr)) (fetch-term-and-cl t2 (cdr addr) (cons t1 cl)))
            (t (fetch-term-and-cl t3
                (cdr addr)
                (cons (dumb-negate-lit t1) cl)))))
        (('implies t1 t2) (cond ((= 1 (car addr)) (fetch-term-and-cl t1
                (cdr addr)
                (cons (dumb-negate-lit t2) cl)))
            (t (fetch-term-and-cl t2 (cdr addr) (cons t1 cl)))))
        (& (fetch-term-and-cl (nth (1- (car addr)) (fargs term))
            (cdr addr)
            cl))))
    (t (mv nil t))))

(defun fetch-term
  (term addr)
  (mv-let (term cl)
    (fetch-term-and-cl term addr nil)
    (if (eq cl t)
      (er hard
        'fetch-term
        "FETCH-TERM-AND-CL did not find a subterm of ~x0 at address ~x1."
        term
        addr)
      term)))

(defun governors
  (term addr)
  (mv-let (term cl)
    (fetch-term-and-cl term addr nil)
    (declare (ignore term))
    cl))

(defun term-id-iff
  (term address iff-flg)
  (if (null address)
    iff-flg
    (term-id-iff (nth (car address) term)
      (cdr address)
      (cond ((eq (ffn-symb term) 'if) (if (= (car address) 1)
            t
            iff-flg))
        ((member-eq (ffn-symb term) '(implies iff not)) t)
        (t nil)))))

(defmacro ? (x) `(?-fn ',X))

(defstub ?-fn (x) t)

(defun abbreviations-alist
  (abbreviations)
  (if (consp abbreviations)
    (cons (cons (fcons-term* '?-fn (kwote (caar abbreviations)))
        (cdar abbreviations))
      (abbreviations-alist (cdr abbreviations)))
    nil))

(mutual-recursion (defun chk-?s
    (term ctx state)
    (cond ((or (variablep term) (fquotep term)) (value nil))
      ((eq (ffn-symb term) '?-fn) (case-match term
          ((& ('quote var)) (if (variablep var)
              (er soft
                ctx
                "The variable ~x0 is not among the current abbreviations."
                var)
              (er soft ctx "Expected a variable in place of ~x0." var)))
          (& (value (er hard
                ctx
                "Bad call of ?-FN, ~x0.  ?-FN must be called on the quotation of ~
                                        a variable."
                term)))))
      ((flambdap (ffn-symb term)) (er-progn (chk-?s (lambda-body (ffn-symb term)) ctx state)
          (chk-?s-lst (fargs term) ctx state)))
      (t (chk-?s-lst (fargs term) ctx state))))
  (defun chk-?s-lst
    (term-lst ctx state)
    (if (consp term-lst)
      (er-progn (chk-?s (car term-lst) ctx state)
        (chk-?s-lst (cdr term-lst) ctx state))
      (value nil))))

(defun remove-?s
  (term abbreviations-alist ctx state)
  (let ((newterm (sublis-expr-non-quoteps abbreviations-alist term)))
    (er-progn (chk-?s newterm ctx state) (value newterm))))

(defun translate-abb
  (x abbreviations ctx state)
  (mv-let (erp term state)
    (translate x t t t ctx (w state) state)
    (if erp
      (mv erp term state)
      (remove-?s term
        (abbreviations-alist abbreviations)
        ctx
        state))))

(defmacro trans0
  (x &optional abbreviations ctx)
  `(translate-abb ,X ,ABBREVIATIONS ,(OR CTX ''TRANS0) state))

(defun p-body
  (conc current-addr abbreviations state)
  (io? proof-builder
    nil
    state
    (abbreviations current-addr conc)
    (fms0 "~|~y0~|"
      (list (cons #\0
          (untrans0 (fetch-term conc current-addr)
            (term-id-iff conc current-addr t)
            abbreviations))))))

(define-pc-help p
  nil
  (when-goals (p-body (conc t) (current-addr t) (abbreviations t) state)))

(define-pc-help pp
  nil
  (when-goals (io? proof-builder
      nil
      state
      (state-stack)
      (fms0 "~|~y0~|"
        (list (cons #\0 (fetch-term (conc t) (current-addr t))))))))

(defun take-by-indices
  (m indices lst)
  (if (consp lst)
    (if (member-equal m indices)
      (cons (car lst) (take-by-indices (1+ m) indices (cdr lst)))
      (take-by-indices (1+ m) indices (cdr lst)))
    nil))

(defun print-hyps
  (indexed-hyps ndigits abbreviations state)
  (declare (xargs :guard (and (eqlable-alistp indexed-hyps)
        (integerp ndigits)
        (> ndigits 0))))
  (if (null indexed-hyps)
    state
    (pprogn (io? proof-builder
        nil
        state
        (abbreviations ndigits indexed-hyps)
        (fms0 "~c0. ~y1~|"
          (list (cons #\0 (cons (caar indexed-hyps) ndigits))
            (cons #\1 (untrans0 (cdar indexed-hyps) t abbreviations)))))
      (print-hyps (cdr indexed-hyps) ndigits abbreviations state))))

(defun some->
  (lst n)
  (declare (xargs :guard (and (rational-listp lst) (rationalp n))))
  (if lst
    (or (> (car lst) n) (some-> (cdr lst) n))
    nil))

(defun print-hyps-top
  (indexed-hyps abbreviations state)
  (declare (xargs :guard (eqlable-alistp indexed-hyps)))
  (if (null indexed-hyps)
    (io? proof-builder
      nil
      state
      nil
      (fms0 "~|There are no top-level hypotheses.~|"))
    (print-hyps indexed-hyps
      (if (some-> (strip-cars indexed-hyps) 9)
        2
        1)
      abbreviations
      state)))

(defun print-governors-top
  (indexed-hyps abbreviations state)
  (declare (xargs :guard (eqlable-alistp indexed-hyps)))
  (if (null indexed-hyps)
    (io? proof-builder
      nil
      state
      nil
      (fms0 "~|There are no governors.~|"))
    (print-hyps indexed-hyps
      (if (some-> (strip-cars indexed-hyps) 9)
        2
        1)
      abbreviations
      state)))

(defun pair-indices
  (seed indices lst)
  (declare (xargs :guard (and (integerp seed)
        (true-listp lst)
        (bounded-integer-listp 1 (length lst) indices))))
  (if lst
    (let ((rest-lst (pair-indices (1+ seed) indices (cdr lst))))
      (if (member seed indices)
        (cons (cons seed (car lst)) rest-lst)
        rest-lst))
    nil))

(define-pc-macro hyps
  (&optional hyps-indices govs-indices)
  (when-goals-trip (let* ((hyps (hyps t)) (len-hyps (length hyps))
        (govs (and govs-indices (governors (conc t) (current-addr t))))
        (len-govs (length govs))
        (abbs (abbreviations t))
        (hyps-indices (or hyps-indices (null args))))
      (cond ((not (or (eq hyps-indices t)
             (bounded-integer-listp 1 len-hyps hyps-indices))) (pprogn (io? proof-builder
              nil
              state
              (len-hyps hyps-indices)
              (fms0 "~|Bad hypothesis-list argument to HYPS, ~X0n.  The ~
                    hypothesis-list argument should either be T or should be a ~
                    list of integers between 1 and the number of top-level ~
                    hypotheses, ~x1.~%"
                (list (cons #\0 hyps-indices)
                  (cons #\n nil)
                  (cons #\1 len-hyps))))
            (value :fail)))
        ((not (or (eq govs-indices t)
             (bounded-integer-listp 1 len-govs govs-indices))) (pprogn (io? proof-builder
              nil
              state
              (len-govs govs-indices)
              (fms0 "~|Bad governors-list argument to HYPS,~%  ~X0n.~%The ~
                    governors-list argument should either be T or should be a ~
                    list of integers between 1 and the number of top-level ~
                    governors, ~x1."
                (list (cons #\0 govs-indices)
                  (cons #\n nil)
                  (cons #\1 len-govs))))
            (value :fail)))
        ((and (null hyps-indices) (null govs-indices)) (pprogn (io? proof-builder
              nil
              state
              nil
              (fms0 "~|You have specified no printing of either hypotheses or ~
                    governors!  Perhaps you should read the documentation for ~
                    the HYPS command.~|"))
            (value :fail)))
        (t (let ((hyps-to-print (if (eq hyps-indices t)
                 (count-off 1 hyps)
                 (pair-indices 1 hyps-indices hyps))) (govs-to-print (if (eq govs-indices t)
                  (count-off 1 govs)
                  (pair-indices 1 govs-indices govs))))
            (pprogn (if hyps-indices
                (pprogn (if (eq hyps-indices t)
                    (io? proof-builder
                      nil
                      state
                      nil
                      (fms0 "~|*** Top-level hypotheses:~|"))
                    (io? proof-builder
                      nil
                      state
                      nil
                      (fms0 "~|*** Specified top-level hypotheses:~|")))
                  (print-hyps-top hyps-to-print abbs state))
                state)
              (if govs-indices
                (pprogn (if (eq govs-indices t)
                    (io? proof-builder
                      nil
                      state
                      nil
                      (fms0 "~|~%*** Governors:~|"))
                    (io? proof-builder
                      nil
                      state
                      nil
                      (fms0 "~|~%*** Specified governors:~|")))
                  (print-governors-top govs-to-print abbs state))
                state)
              (value 'skip))))))))

(define-pc-primitive demote
  (&rest rest-args)
  (cond (current-addr (print-no-change2 "You must be at the top of the conclusion in order to ~
                       demote hypotheses. Try TOP first."))
    ((null hyps) (print-no-change2 "There are no top-level hypotheses."))
    (t (let ((badindices (non-bounded-nums rest-args 1 (length hyps))))
        (if badindices
          (print-no-change2 "The arguments to DEMOTE ~
                             must be indices of active top-level hypotheses, ~
                             but the following are not:  ~&0."
            (list (cons #\0 badindices)))
          (mv (change-pc-state pc-state
              :goals (cons (change goal
                  (car goals)
                  :hyps (if rest-args
                    (remove-by-indices 1 rest-args hyps)
                    nil)
                  :conc (make-implication (if rest-args
                      (take-by-indices 1 rest-args hyps)
                      hyps)
                    conc))
                (cdr goals)))
            state))))))

(defun pair-keywords
  (keywords lst)
  (declare (xargs :guard (and (keyword-listp keywords) (keyword-value-listp lst))))
  (if (consp keywords)
    (mv-let (alist rst)
      (pair-keywords (cdr keywords) lst)
      (let ((tail (assoc-keyword (car keywords) rst)))
        (if tail
          (mv (cons (cons (car tail) (cadr tail)) alist)
            (remove-keyword (car keywords) rst))
          (mv alist rst))))
    (mv nil lst)))

(defun null-pool
  (pool)
  (cond ((null pool) t)
    ((eq (access pool-element (car pool) :tag)
       'being-proved-by-induction) (null-pool (cdr pool)))
    (t nil)))

(defun initial-pspv
  (term displayed-goal
    otf-flg
    ens
    wrld
    state
    splitter-output
    orig-hints)
  (change prove-spec-var
    *empty-prove-spec-var*
    :rewrite-constant (initial-rcnst-from-ens ens wrld state splitter-output)
    :user-supplied-term term
    :displayed-goal displayed-goal
    :otf-flg otf-flg
    :orig-hints orig-hints))

(defun pc-prove
  (term displayed-goal hints otf-flg ens wrld ctx state)
  (er-let* ((ttree (let ((pspv (initial-pspv term
              displayed-goal
              otf-flg
              ens
              wrld
              state
              (splitter-output)
              hints)) (clauses (list (list term))))
         (if (f-get-global 'in-verify-flg state)
           (state-global-let* ((saved-output-p t) (saved-output-token-lst :all))
             (pprogn (f-put-global 'saved-output-reversed nil state)
               (push-current-acl2-world 'saved-output-reversed state)
               (prove-loop clauses pspv hints ens wrld ctx state)))
           (prove-loop clauses pspv hints ens wrld ctx state)))))
    (er-progn (chk-assumption-free-ttree ttree ctx state)
      (value ttree))))

(defun abbreviations-alist-?
  (abbreviations)
  (if (consp abbreviations)
    (cons (cons (fcons-term* '? (caar abbreviations))
        (cdar abbreviations))
      (abbreviations-alist-? (cdr abbreviations)))
    nil))

(defun find-?-fn
  (x)
  (if (atom x)
    nil
    (if (eq (car x) '?-fn)
      (list (cadr x))
      (union-equal (find-?-fn (car x)) (find-?-fn (cdr x))))))

(defun unproved-pc-prove-clauses
  (ttree)
  (reverse-strip-cdrs (tagged-objects :bye ttree) nil))

(defun prover-call
  (comm term-to-prove rest-args pc-state state)
  (declare (xargs :guard (keywordp comm)))
  (let ((prover-call-abbreviations (access pc-state pc-state :abbreviations)) (prover-call-wrld (w state)))
    (let ((prover-call-pc-ens (make-pc-ens (access pc-state pc-state :pc-ens) state)))
      (mv-let (prover-call-pairs prover-call-tail)
        (pair-keywords '(:otf-flg :hints) rest-args)
        (if prover-call-tail
          (pprogn (print-no-change "The only keywords allowed in the arguments to the ~x0 command ~
                     are :otf-flg and :hints.  Your ~
                     instruction ~x1 violates this requirement."
              (list (cons #\0 comm)
                (cons #\1 (make-pretty-pc-instr (cons comm rest-args)))))
            (mv t nil state))
          (mv-let (prover-call-erp prover-call-hints state)
            (let ((un-?-hints (sublis-equal (abbreviations-alist-? prover-call-abbreviations)
                   (cdr (assoc-eq :hints prover-call-pairs)))))
              (let ((?-exprs (find-?-fn un-?-hints)))
                (if ?-exprs
                  (pprogn (print-no-change "You appear to have attempted to use the following ~
                                   abbreviation variable~#0~[~/~/s~], which however ~
                                   ~#0~[~/is~/are~] not among ~
                                   the current abbreviation variables (see SHOW-ABBREVIATIONS):  ~&1."
                      (list (cons #\0 (zero-one-or-more (length ?-exprs)))
                        (cons #\1 ?-exprs)))
                    (mv t nil state))
                  (pprogn (io? proof-builder
                      nil
                      state
                      nil
                      (fms0 "~|***** Now entering the theorem ~
                                           prover *****~|"))
                    (translate-hints+ 'proof-builder
                      un-?-hints
                      (default-hints prover-call-wrld)
                      comm
                      prover-call-wrld
                      state)))))
            (if prover-call-erp
              (pprogn (print-no-change "Failed to translate hints successfully.")
                (mv t nil state))
              (let ((prover-call-otf-flg (cdr (assoc-eq :otf-flg prover-call-pairs))))
                (mv-let (prover-call-erp prover-call-ttree state)
                  (pc-prove term-to-prove
                    (untranslate term-to-prove t prover-call-wrld)
                    prover-call-hints
                    prover-call-otf-flg
                    prover-call-pc-ens
                    prover-call-wrld
                    comm
                    state)
                  (pprogn (io? proof-builder nil state nil (fms0 "~%"))
                    (if prover-call-erp
                      (pprogn (print-no-change "Proof failed.") (mv t nil state))
                      (mv nil prover-call-ttree state))))))))))))

(defun make-new-goals
  (cl-set goal-name start-index)
  (if (consp cl-set)
    (cons (make goal
        :conc (car (last (car cl-set)))
        :hyps (dumb-negate-lit-lst (butlast (car cl-set) 1))
        :current-addr nil
        :goal-name (cons goal-name start-index)
        :depends-on 1)
      (make-new-goals (cdr cl-set) goal-name (1+ start-index)))
    nil))

(defun same-goal
  (goal1 goal2)
  (and (equal (access goal goal1 :hyps) (access goal goal2 :hyps))
    (equal (access goal goal1 :conc) (access goal goal2 :conc))))

(defun remove-byes-from-tag-tree
  (ttree)
  (remove-tag-from-tag-tree :bye ttree))

(define-pc-primitive prove
  (&rest rest-args)
  (cond (current-addr (print-no-change2 "The PROVE command should only be used at ~
                       the top.  Use (= T) if that is what you want."))
    ((not (keyword-value-listp rest-args)) (print-no-change2 "The argument list for the PROVE command should ~
                       be empty or a list of even length with keywords in the odd ~
                       positions.  See the documentation for examples and details."))
    (t (mv-let (erp ttree state)
        (prover-call :prove (make-implication hyps conc)
          rest-args
          pc-state
          state)
        (cond (erp (mv nil state))
          (t (let* ((new-clauses (unproved-pc-prove-clauses ttree)) (new-goals (make-new-goals new-clauses goal-name depends-on))
                (len-new-goals (length new-goals)))
              (cond ((and (equal len-new-goals 1)
                   (same-goal (car new-goals) (car goals))) (print-no-change2 "Exactly one new goal was created by your PROVE ~
                              command, and it has exactly the same hypotheses ~
                              and conclusion as did the current goal."))
                ((tagged-objects 'assumption ttree) (mv (change-pc-state pc-state
                      :goals (cons (change goal
                          (car goals)
                          :conc *t*
                          :depends-on (+ (access goal (car goals) :depends-on) len-new-goals))
                        (append new-goals (cdr goals)))
                      :local-tag-tree (remove-byes-from-tag-tree ttree))
                    state))
                (t (mv (change-pc-state pc-state
                      :goals (append new-goals (cdr goals))
                      :local-tag-tree (remove-byes-from-tag-tree ttree))
                    state))))))))))

(defun add-string-val-pair-to-string-val-alist-1
  (key key1 val alist replace-p)
  (cond ((null alist) (list (list key key1 val)))
    ((and (stringp (caar alist)) (string-equal key (caar alist))) (if (assoc-keyword key1 (cdar alist))
        (if replace-p
          (cons (list* (caar alist)
              key1
              val
              (remove-keyword key1 (cdar alist)))
            (cdr alist))
          alist)
        (cons (list* (caar alist) key1 val (cdar alist))
          (cdr alist))))
    (t (cons (car alist)
        (add-string-val-pair-to-string-val-alist-1 key
          key1
          val
          (cdr alist)
          replace-p)))))

(defun add-string-val-pair-to-string-val-alist
  (key key1 val alist)
  (add-string-val-pair-to-string-val-alist-1 key
    key1
    val
    alist
    nil))

(defun add-string-val-pair-to-string-val-alist!
  (key key1 val alist)
  (add-string-val-pair-to-string-val-alist-1 key
    key1
    val
    alist
    t))

(defconst *bash-skip-forcing-round-hints*
  '(("[1]Goal" :by nil) ("[1]Subgoal 1" :by nil)
    ("[1]Subgoal 2" :by nil)
    ("[1]Subgoal 3" :by nil)
    ("[1]Subgoal 4" :by nil)
    ("[1]Subgoal 5" :by nil)
    ("[1]Subgoal 6" :by nil)
    ("[1]Subgoal 7" :by nil)
    ("[1]Subgoal 8" :by nil)
    ("[1]Subgoal 9" :by nil)
    ("[1]Subgoal 10" :by nil)
    ("[1]Subgoal 11" :by nil)
    ("[1]Subgoal 12" :by nil)
    ("[1]Subgoal 13" :by nil)
    ("[1]Subgoal 14" :by nil)
    ("[1]Subgoal 15" :by nil)))

(define-pc-atomic-macro bash
  (&rest hints)
  (if (alistp hints)
    (value (list :prove :hints (append *bash-skip-forcing-round-hints*
          (add-string-val-pair-to-string-val-alist "Goal"
            :do-not (list 'quote
              '(generalize eliminate-destructors
                fertilize
                eliminate-irrelevance))
            (add-string-val-pair-to-string-val-alist! "Goal"
              :do-not-induct 'proof-builder
              hints)))
        :otf-flg t))
    (pprogn (print-no-change "A BASH instruction must be of the form~%~ ~ ~
              (:BASH (goal_name_1 ...) ... (goal_name_n ...)),~%and hence ~
              your instruction,~%~ ~ ~x0,~%is not legal."
        (list (cons #\0 (cons :bash hints))))
      (value :fail))))

(define-pc-primitive dive
  (n &rest rest-addr)
  (if (not (bounded-integer-listp 1 'infinity args))
    (print-no-change2 "The arguments to DIVE must all be positive integers.")
    (mv-let (subterm cl)
      (fetch-term-and-cl (fetch-term conc current-addr) args nil)
      (declare (ignore subterm))
      (if (eq cl t)
        (print-no-change2 "Unable to DIVE according to the address~%~ ~ ~y0."
          (list (cons #\0 (cons n rest-addr))))
        (mv (change-pc-state pc-state
            :goals (cons (change goal
                (car goals)
                :current-addr (append (access goal (car goals) :current-addr) args))
              (cdr goals)))
          state)))))

(define-pc-atomic-macro split
  nil
  (value '(:prove :hints (("Goal" :do-not-induct proof-builder
         :do-not '(generalize eliminate-destructors
           fertilize
           eliminate-irrelevance)
         :in-theory (theory 'minimal-theory))))))

(define-pc-primitive add-abbreviation
  (var &optional raw-term)
  (mv-let (erp term state)
    (if (cdr args)
      (trans0 raw-term abbreviations :add-abbreviation)
      (value (fetch-term conc current-addr)))
    (cond (erp (mv nil state))
      ((variablep var) (if (assoc-eq var abbreviations)
          (print-no-change2 "The abbreviation ~x0 has already been used, and stands for  ~x1."
            (list (cons #\0 var)
              (cons #\1 (untrans0 (cdr (assoc-eq var abbreviations))))))
          (mv (change-pc-state pc-state
              :abbreviations (cons (cons var term) abbreviations))
            state)))
      (t (print-no-change2 "An abbreviation must be a variable, but ~x0 is not."
          (list (cons #\0 var)))))))

(defun not-in-domain-eq
  (lst alist)
  (declare (xargs :guard (if (symbol-listp lst)
        (alistp alist)
        (symbol-alistp alist))))
  (if (consp lst)
    (if (assoc-eq (car lst) alist)
      (not-in-domain-eq (cdr lst) alist)
      (cons (car lst) (not-in-domain-eq (cdr lst) alist)))
    nil))

(define-pc-primitive remove-abbreviations
  (&rest vars)
  (if (null abbreviations)
    (print-no-change2 "There are currently no abbreviations.")
    (let ((badvars (and args (not-in-domain-eq vars abbreviations))))
      (if (and args badvars)
        (print-no-change2 "The variable~#0~[~/~/s~] ~&1 ~
                             ~#0~[~/is not currently an abbreviation variable~/~
                                    are not currently abbreviation variables~]."
          (list (cons #\0 (zero-one-or-more (length badvars)))
            (cons #\1 badvars)))
        (mv (change-pc-state pc-state
            :abbreviations (if args
              (remove1-assoc-eq-lst vars abbreviations)
              nil))
          state)))))

(defun print-abbreviations
  (vars abbreviations state)
  (declare (xargs :guard (and (true-listp vars) (symbol-alistp abbreviations))))
  (if (null vars)
    state
    (pprogn (io? proof-builder nil state nil (fms0 "~%"))
      (let ((pair (assoc-equal (car vars) abbreviations)))
        (if (null pair)
          (io? proof-builder
            nil
            state
            (vars)
            (fms0 "*** ~x0 does not abbreviate a term.~|"
              (list (cons #\0 (car vars)))))
          (let ((untrans-1 (untrans0 (cdr pair))) (untrans-2 (untrans0 (cdr pair)
                  nil
                  (remove1-assoc-eq (car pair) abbreviations))))
            (pprogn (io? proof-builder
                nil
                state
                (pair)
                (fms0 "(? ~x0) is an abbreviation for:~%~ ~ "
                  (list (cons #\0 (car pair)))))
              (io? proof-builder
                nil
                state
                (untrans-1)
                (fms0 "~y0~|" (list (cons #\0 untrans-1)) 2))
              (if (equal untrans-1 untrans-2)
                state
                (pprogn (io? proof-builder nil state nil (fms0 "i.e. for~%~ ~ "))
                  (io? proof-builder
                    nil
                    state
                    (untrans-2)
                    (fms0 "~y0~|" (list (cons #\0 untrans-2)) 2))))))))
      (print-abbreviations (cdr vars) abbreviations state))))

(define-pc-help show-abbreviations
  (&rest vars)
  (if (null (abbreviations t))
    (io? proof-builder
      nil
      state
      nil
      (fms0 "~|There are currently no abbreviations.~%"))
    (print-abbreviations (or vars (strip-cars (abbreviations t)))
      (abbreviations t)
      state)))

(defun drop-from-end
  (n l)
  (declare (xargs :guard (and (integerp n)
        (not (< n 0))
        (true-listp l)
        (<= n (length l)))))
  (take (- (length l) n) l))

(define-pc-primitive up
  (&optional n)
  (let ((n (or n 1)))
    (cond ((null current-addr) (print-no-change2 "Already at the top."))
      ((not (and (integerp n) (> n 0))) (print-no-change2 "If UP is supplied with an argument, it must be ~
                              a positive integer or NIL, unlike ~x0."
          (list (cons #\0 n))))
      ((<= n (length current-addr)) (mv (change-pc-state pc-state
            :goals (cons (change goal
                (car goals)
                :current-addr (drop-from-end n current-addr))
              (cdr goals)))
          state))
      (t (print-no-change2 "Can only go up ~x0 level~#1~[~/~/s~]."
          (list (cons #\0 (length current-addr))
            (cons #\1 (zero-one-or-more (length current-addr)))))))))

(define-pc-atomic-macro top
  nil
  (when-goals-trip (let ((current-addr (current-addr t)))
      (value (list :up (length current-addr))))))

(defmacro expand-address-recurse
  (&key (ans '(cons (car addr) rest-addr))
    (new-addr '(cdr addr))
    (new-raw-term '(nth (car addr) raw-term))
    (new-term '(nth (car addr) term))
    (new-iff-flg 'nil)
    (new-accumulated-addr-r '(cons (car addr) accumulated-addr-r)))
  `(mv-let (erp rest-addr)
    (expand-address ,NEW-ADDR
      ,NEW-RAW-TERM
      ,NEW-TERM
      abbreviations
      ,NEW-IFF-FLG
      ,NEW-ACCUMULATED-ADDR-R
      wrld)
    (if erp
      (mv erp rest-addr)
      (mv nil ,ANS))))

(defmacro dive-once-more-error
  nil
  '(mv "When diving to subterm ~x0 using address ~x1, ~
              the additional dive to ~x2 was impossible."
    (list (cons #\0 raw-term)
      (cons #\1 (reverse accumulated-addr-r))
      (cons #\2 (car addr)))))

(defun abbreviation-raw-term-p
  (x)
  (and (consp x) (eq (car x) '?)))

(defmacro addr-recur
  (pos b)
  `(if (integerp ,POS)
    (mv-let (addr new-term new-iff-flg not-flg)
      ,B
      (if (msgp addr)
        (mv addr nil nil nil)
        (mv (cons ,POS addr) new-term new-iff-flg not-flg)))
    (if (eq ,POS 'not)
      ,(CASE-MATCH B (('MV 'NIL X Y 'NIL) `(MV NIL ,X ,Y T))
             (& '(MV "a NOT term unexpected by the code; sorry" NIL NIL NIL)))
      (mv ,POS nil nil nil))))

(defun or-addr
  (n term iff-flg)
  (case-match term
    (('if x1 x1 x2) (declare (ignore x1))
      (cond ((int= n 1) (mv "of an ambiguity: the first argument of the OR term occurs ~
                  twice in the IF term that represents the OR term"
            nil
            nil
            nil))
        ((int= n 2) (addr-recur 3 (or-addr (1- n) x2 iff-flg)))
        (t (mv "of an index that is out of range" nil nil nil))))
    (('if x1 x2 *t*) (cond ((int= n 1) (cond ((ffn-symb-p x1 'not) (mv '(1) x1 t t))
            (t (mv (msg "that dive has led us to the first argument of ~
                             the term ~x0, but we expected to reach a call of ~
                             ~x1"
                  term
                  'not)
                nil
                nil
                nil))))
        (t (addr-recur 2 (or-addr (1- n) x2 iff-flg)))))
    (('if x1 *t* x2) (cond ((int= n 1) (mv '(1) x1 t nil))
        (t (addr-recur 3 (or-addr (1- n) x2 iff-flg)))))
    (& (cond ((int= n 1) (mv nil term iff-flg nil))
        (t (mv "a non-IF term was encountered when diving to the first ~
                 argument (perhaps because your DV argument was greater than ~
                 the number of disjuncts)."
            nil
            nil
            nil))))))

(defun and-addr
  (n term iff-flg)
  (case-match term
    (('if x1 x2 *nil*) (cond ((int= n 1) (mv '(1) x1 t nil))
        (t (addr-recur 2 (and-addr (1- n) x2 iff-flg)))))
    (('if x1 *nil* x2) (cond ((int= n 1) (cond ((ffn-symb-p x1 'not) (mv '(1) x1 t t))
            (t (mv "of an unexpected case of diving to the first ~
                        argument: for an if-then-else term with THEN branch ~
                        of nil, the TEST was expected to be a call of NOT"
                nil
                nil
                nil))))
        (t (addr-recur 3 (and-addr (1- n) x2 iff-flg)))))
    (& (cond ((int= n 1) (mv nil term iff-flg nil))
        (t (mv "a non-IF term was encountered when diving to the first ~
                 argument (perhaps because your DV argument was greater than ~
                 the number of conjuncts)"
            nil
            nil
            nil))))))

(set-table-guard dive-into-macros-table
  (and (symbolp key)
    (or (and (function-symbolp val world)
        (equal (stobjs-in val world) '(nil nil nil nil))
        (not (assoc-eq val *ttag-fns*))
        (not (member-eq val (global-val 'untouchable-fns world))))
      (integerp val)
      (null val))))

(defmacro add-dive-into-macro
  (name val)
  `(table dive-into-macros-table ',NAME ',VAL))

(defmacro remove-dive-into-macro
  (name)
  `(table dive-into-macros-table ',NAME nil))

(defun dive-into-macros-table
  (wrld)
  (declare (xargs :guard (plist-worldp wrld)))
  (table-alist 'dive-into-macros-table wrld))

(defun rassoc-eq-as-car
  (key alist)
  (cond ((endp alist) nil)
    ((eq key (car (cdr (car alist)))) (car alist))
    (t (rassoc-eq-as-car key (cdr alist)))))

(defconst *ca<d^n>r-alist*
  '((cadr . 2) (cdar . 2)
    (caar . 2)
    (cddr . 2)
    (caadr . 3)
    (cdadr . 3)
    (cadar . 3)
    (cddar . 3)
    (caaar . 3)
    (cdaar . 3)
    (caddr . 3)
    (cdddr . 3)
    (caaadr . 4)
    (cadadr . 4)
    (caadar . 4)
    (caddar . 4)
    (cdaadr . 4)
    (cddadr . 4)
    (cdadar . 4)
    (cdddar . 4)
    (caaaar . 4)
    (cadaar . 4)
    (caaddr . 4)
    (cadddr . 4)
    (cdaaar . 4)
    (cddaar . 4)
    (cdaddr . 4)
    (cddddr . 4)))

(defun car/cdr^n
  (n term)
  (cond ((zp n) term)
    ((or (variablep term)
       (not (member-eq (car term) '(car cdr)))) (er hard
        'car/cdr^n
        "Illegal call: ~x0.~|If you encountered this call in the ~
         proof-builder, please contact the ACL2 implementors."
        `(car/cdr^n ,N ,TERM)))
    (t (car/cdr^n (1- n) (fargn term 1)))))

(defmacro expand-address-msg
  (str &rest args)
  `(mv ,STR
    (cons (cons #\0
        (if accumulated-addr-r
          (msg "The dive via address ~x0 brings us to"
            (reverse accumulated-addr-r))
          "The current subterm is"))
      (cons (cons #\f
          (if accumulated-addr-r
            " further"
            ""))
        ,(MAKE-FMT-BINDINGS (CDR *BASE-10-CHARS*) ARGS)))))

(defun expand-address
  (addr raw-term
    term
    abbreviations
    iff-flg
    accumulated-addr-r
    wrld)
  (cond ((or (null addr) (equal addr '(0))) (mv nil nil))
    ((abbreviation-raw-term-p raw-term) (let ((pair (assoc-eq (cadr raw-term) abbreviations)))
        (if pair
          (expand-address (cdr addr)
            (cdr pair)
            term
            (remove1-equal pair abbreviations)
            iff-flg
            (cons (car addr) accumulated-addr-r)
            wrld)
          (mv t
            (er hard
              'expand-address
              "Found abbreviation variable ~x0 that is not in the ~
                        current abbreviations alist, ~x1."
              (cadr raw-term)
              abbreviations)))))
    ((not (and (integerp (car addr)) (< 0 (car addr)))) (mv "All members of an address must be positive integers (except ~
              that 0 is allowed in circumstances involving CASE, COND, and ~
              abbreviations, which do not apply here).  ~x0 violates this ~
              requirement."
        (list (cons #\0 (car addr)))))
    ((or (variablep raw-term)
       (fquotep raw-term)
       (not (< (car addr) (length raw-term)))) (dive-once-more-error))
    ((flambda-applicationp term) (cond ((eql (car addr) 2) (mv "Unable to dive to the body of a LET, which is really part of ~
                 the function symbol of the translated LAMBDA term."
            nil))
        ((and (consp raw-term)
           (eq (car raw-term) 'let)
           (>= (length addr) 3)
           (eql (car addr) 1)
           (natp (cadr addr))
           (< (cadr addr) (length (cadr raw-term)))
           (member (caddr addr) '(0 1))) (cond ((eql (caddr addr) 0) (mv "Unable to dive to a variable of a LET." nil))
            (t (expand-address-recurse :ans (cons (1+ (cadr addr)) rest-addr)
                :new-addr (cdddr addr)
                :new-raw-term (nth 1 (nth (cadr addr) (nth 1 raw-term)))
                :new-term (nth (1+ (car addr)) term)
                :new-accumulated-addr-r (cons (1+ (car addr)) accumulated-addr-r)))))
        (t (mv "Unable to expand LAMBDA (LET) term." nil))))
    ((atom raw-term) (mv t
        (er hard
          'expand-address
          "Surprise!  Found an unexpected raw-term atom, ~x0."
          raw-term)))
    (t (let ((dive-fn (cdr (assoc-eq (car raw-term) (dive-into-macros-table wrld)))))
        (cond (dive-fn (mv-let (erp val)
              (ev-fncall-w dive-fn
                (list (car addr) raw-term term wrld)
                wrld
                nil
                nil
                t
                nil
                t)
              (cond ((or erp (stringp (car val))) (mv (car val) (cdr val)))
                (t (expand-address-recurse :ans (append val rest-addr)
                    :new-iff-flg nil
                    :new-term (fetch-term term val))))))
          ((let ((pair (rassoc-eq-as-car (car raw-term) (untrans-table wrld))))
             (and pair (eql (arity (car pair) wrld) 2))) (let* ((lst (cond ((= (car addr) (1- (length raw-term))) (make-list (1- (car addr)) :initial-element 2))
                   (t (append (make-list (1- (car addr)) :initial-element 2) '(1))))) (subterm (fetch-term term lst)))
              (if subterm
                (expand-address-recurse :ans (append lst rest-addr)
                  :new-iff-flg nil
                  :new-term subterm)
                (dive-once-more-error))))
          (t (case (car raw-term)
              ((list list*) (let* ((lst0 (make-list (1- (car addr)) :initial-element 2)) (lst (if (eq (car raw-term) 'list)
                        (append lst0 '(1))
                        lst0))
                    (subterm (fetch-term term lst)))
                  (if subterm
                    (expand-address-recurse :ans (append lst rest-addr)
                      :new-iff-flg nil
                      :new-term subterm)
                    (dive-once-more-error))))
              (<= (cond ((not (member (car addr) '(1 2))) (dive-once-more-error))
                  ((= (car addr) 1) (expand-address-recurse :ans (cons 1 (cons 2 rest-addr))
                      :new-iff-flg nil
                      :new-term (nth 2 (nth 1 term))))
                  (t (expand-address-recurse :ans (cons 1 (cons 1 rest-addr))
                      :new-iff-flg nil
                      :new-term (nth 1 (nth 1 term))))))
              ((and or) (mv-let (and-or-addr new-term new-iff-flg finish-not-p)
                  (if (eq (car raw-term) 'and)
                    (and-addr (car addr)
                      (abbreviate term abbreviations)
                      iff-flg)
                    (or-addr (car addr) (abbreviate term abbreviations) iff-flg))
                  (cond ((msgp and-or-addr) (expand-address-msg "~@0 the ~x4 term~%~ ~ ~y1,~|~%which translates ~
                            to~%~ ~ ~y2.~|~%The requested dive into this ~x4 ~
                            term is problematic, because ~@3.  Try using DIVE ~
                            instead (you may use PP to find the appropriate ~
                            address)."
                        raw-term
                        term
                        and-or-addr
                        (car raw-term)))
                    (finish-not-p (cond ((and (cdr addr) (int= (cadr addr) 1)) (expand-address-recurse :ans (append and-or-addr rest-addr)
                            :new-addr (cddr addr)
                            :new-term new-term
                            :new-iff-flg new-iff-flg
                            :new-accumulated-addr-r (cons 1 (cons (car addr) accumulated-addr-r))))
                        (t (let ((accumulated-addr-r (cons (car addr) accumulated-addr-r)))
                            (expand-address-msg "~@0 the NOT term ~x1, which does not actually ~
                                exist in the internal syntax of the current ~
                                term, namely:~%~x2.  Try using DIVE instead ~
                                (you may use PP to find the appropriate ~
                                address)."
                              (nth (car addr) raw-term)
                              term)))))
                    (t (expand-address-recurse :ans (append and-or-addr rest-addr)
                        :new-term new-term
                        :new-iff-flg new-iff-flg)))))
              (case (cond ((= (car addr) 1) (expand-address-msg "~@0 the CASE term~%~ ~ ~x1,~%which corresponds to the ~
                     translated term~%~ ~ ~x2.~%A~@f dive to the first ~
                     argument doesn't really make sense here."
                      raw-term
                      term))
                  ((not (and (consp (cdr addr)) (member-equal (cadr addr) '(0 1)))) (expand-address-msg "~@0 the CASE term~%~ ~ ~x1,~%A~@f dive past argument ~
                     number ~x2 to the zeroth or first ``argument'' is ~
                     required at this point.~%"
                      raw-term
                      (car addr)))
                  ((and (= (cadr addr) 0)
                     (= (car addr) (1- (length raw-term)))) (expand-address-msg "~@0 the CASE term~%~ ~ ~x1,~%A~@f dive to the ~
                     ``otherwise'' expression is not allowed."
                      raw-term))
                  (t (let* ((lst (if (= (cadr addr) 1)
                           (if (= (car addr) (1- (length raw-term)))
                             (make-list (- (car addr) 2) :initial-element 3)
                             (append (make-list (- (car addr) 2) :initial-element 3)
                               '(2)))
                           (append (make-list (- (car addr) 2) :initial-element 3)
                             '(1 2)))) (subterm (fetch-term term lst)))
                      (if subterm
                        (expand-address-recurse :ans (append lst rest-addr)
                          :new-addr (cddr addr)
                          :new-raw-term (cadr (nth (1+ (car addr)) raw-term))
                          :new-term subterm
                          :new-iff-flg iff-flg
                          :new-accumulated-addr-r (cons (car addr) (cons (cadr addr) accumulated-addr-r)))
                        (mv t
                          (er hard
                            'expand-address
                            "Surprise!  Unable to dive into raw-term ~x0, ~
                                which is term ~x1, using list ~x2.  So far we ~
                                have DV-ed using ~x3."
                            raw-term
                            term
                            lst
                            (reverse accumulated-addr-r))))))))
              (cond (cond ((not (and (consp (cdr addr)) (member-equal (cadr addr) '(0 1)))) (expand-address-msg "~@0 the COND term~%~ ~ ~x1,~%A~@f dive past argument ~
                    number ~x2 to the zeroth or first ``argument'' is ~
                    required at this point.~%"
                      raw-term
                      (car addr)))
                  ((and (= (cadr addr) 0)
                     (= (car addr) (1- (length raw-term)))) (expand-address-msg "~@0 the COND term~%~ ~ ~x1,~%A~@f dive to the ``T'' ~
                    expression is not allowed."
                      raw-term))
                  (t (let* ((lst (if (= (cadr addr) 1)
                           (if (= (car addr) (1- (length raw-term)))
                             (make-list (1- (car addr)) :initial-element 3)
                             (append (make-list (1- (car addr)) :initial-element 3) '(2)))
                           (append (make-list (1- (car addr)) :initial-element 3) '(1)))) (subterm (fetch-term term lst)))
                      (if subterm
                        (expand-address-recurse :ans (append lst rest-addr)
                          :new-addr (cddr addr)
                          :new-raw-term (cadr (nth (1+ (car addr)) raw-term))
                          :new-term subterm
                          :new-iff-flg iff-flg
                          :new-accumulated-addr-r (cons (car addr) (cons (cadr addr) accumulated-addr-r)))
                        (mv t
                          (er hard
                            'expand-address
                            "Surprise!  Unable to dive into raw-term ~x0, ~
                               which is term ~x1, using list ~x2.  So far we ~
                               have DV-ed using ~x3."
                            raw-term
                            term
                            lst
                            (reverse accumulated-addr-r))))))))
              (if (expand-address-recurse :new-iff-flg (if (= (car addr) 1)
                    t
                    iff-flg)))
              ((implies iff) (expand-address-recurse :new-iff-flg t))
              (t (let ((pair (and (consp raw-term)
                       (assoc-eq (car raw-term) *ca<d^n>r-alist*))))
                  (cond (pair (expand-address-recurse :ans (append (make-list (cdr pair) :initial-element 1) rest-addr)
                        :new-term (car/cdr^n (cdr pair) term)))
                    (t (expand-address-recurse))))))))))))

(defmacro dv-error
  (str alist)
  `(pprogn (print-no-change (string-append "Unable to perform the requested dive.~|~%"
        ,STR)
      (cons (cons #\t current-term) ,ALIST))
    (mv t nil state)))

(define-pc-atomic-macro dv
  (&rest rest-args)
  (let* ((conc (conc t)) (current-addr (current-addr t))
      (abbreviations (abbreviations t))
      (current-term (fetch-term conc current-addr))
      (term-id-iff (term-id-iff conc current-addr t)))
    (mv-let (erp addr)
      (expand-address rest-args
        (untrans0 current-term term-id-iff abbreviations)
        current-term
        abbreviations
        term-id-iff
        nil
        (w state))
      (if erp
        (dv-error erp addr)
        (mv nil (cons ':dive addr) state)))))

(mutual-recursion (defun deposit-term
    (term addr subterm)
    (cond ((null addr) subterm)
      (t (cons-term (ffn-symb term)
          (deposit-term-lst (fargs term)
            (car addr)
            (cdr addr)
            subterm)))))
  (defun deposit-term-lst
    (lst n addr subterm)
    (cond ((= 1 n) (cons (deposit-term (car lst) addr subterm) (cdr lst)))
      (t (cons (car lst)
          (deposit-term-lst (cdr lst) (1- n) addr subterm))))))

(defun geneqv-at-subterm
  (term addr geneqv pequiv-info ens wrld)
  (cond ((null addr) geneqv)
    (t (let ((child-geneqv0 (nth (1- (car addr))
             (geneqv-lst (ffn-symb term) geneqv ens wrld))))
        (mv-let (deep-pequiv-lst shallow-pequiv-lst)
          (pequivs-for-rewrite-args (ffn-symb term)
            geneqv
            pequiv-info
            wrld
            ens)
          (mv-let (pre-rev cur/post)
            (split-at-position (car addr) (fargs term) nil)
            (mv-let (child-geneqv child-pequiv-info)
              (geneqv-and-pequiv-info-for-rewrite (ffn-symb term)
                (car addr)
                pre-rev
                cur/post
                nil
                geneqv
                child-geneqv0
                deep-pequiv-lst
                shallow-pequiv-lst
                wrld)
              (geneqv-at-subterm (car cur/post)
                (cdr addr)
                child-geneqv
                child-pequiv-info
                ens
                wrld))))))))

(defun geneqv-at-subterm-top
  (term addr ens wrld)
  (geneqv-at-subterm term addr *geneqv-iff* nil ens wrld))

(defun maybe-truncate-current-address
  (addr term orig-addr acc state)
  (declare (xargs :guard (true-listp addr)))
  (if addr
    (cond ((variablep term) (mv (er hard
            'maybe-truncate-current-address
            "Found variable with non-NIL address!")
          state))
      ((fquotep term) (let ((new-addr (reverse acc)))
          (pprogn (io? proof-builder
              nil
              state
              (new-addr orig-addr)
              (fms0 "~|NOTE:  truncating current address from ~x0 to ~
                              ~x1.  See explanation at end of help for X ~
                              command.~|"
                (list (cons #\0 orig-addr) (cons #\1 new-addr))
                0
                nil))
            (mv new-addr state))))
      (t (maybe-truncate-current-address (cdr addr)
          (nth (1- (car addr)) (fargs term))
          orig-addr
          (cons (car addr) acc)
          state)))
    (mv (reverse acc) state)))

(defun deposit-term-in-goal
  (given-goal conc current-addr new-term state)
  (let ((new-conc (deposit-term conc current-addr new-term)))
    (if (quotep new-term)
      (mv-let (new-current-addr state)
        (maybe-truncate-current-address current-addr
          new-conc
          current-addr
          nil
          state)
        (mv (change goal
            given-goal
            :conc new-conc
            :current-addr new-current-addr)
          state))
      (mv (change goal given-goal :conc new-conc) state))))

(defun split-implies
  (term)
  (if (not (ffn-symb-p term 'implies))
    (mv nil term)
    (mv-let (h c)
      (split-implies (fargn term 2))
      (mv (append (flatten-ands-in-lit (fargn term 1)) h) c))))

(defun find-equivalence-hyp-term
  (term hyps target equiv w)
  (if (consp hyps)
    (mv-let (h c)
      (split-implies (car hyps))
      (if (or (variablep c)
          (fquotep c)
          (not (symbolp (ffn-symb c)))
          (not (refinementp (ffn-symb c) equiv w)))
        (find-equivalence-hyp-term term (cdr hyps) target equiv w)
        (let ((x (fargn c 1)) (y (fargn c 2)))
          (or (and (subsetp-equal h hyps)
              (or (and (equal x term) (equal y target))
                (and (equal y term) (equal x target))))
            (find-equivalence-hyp-term term (cdr hyps) target equiv w)))))
    nil))

(define-pc-primitive equiv
  (x y &optional equiv)
  (mv-let (current-term governors)
    (fetch-term-and-cl conc current-addr nil)
    (cond ((eq governors t) (mv (er hard
            ':=
            "Found governors of T inside command ~x0!"
            (cons := args))
          state))
      (t (let* ((assumptions (append hyps governors)) (w (w state))
            (pc-ens (make-pc-ens pc-ens state)))
          (mv-let (erp new-pc-state state)
            (er-let* ((old (trans0 x abbreviations :equiv)) (new (trans0 y abbreviations :equiv))
                (equiv (if (null equiv)
                    (value 'equal)
                    (if (and (symbolp equiv) (equivalence-relationp equiv w))
                      (value equiv)
                      (er soft
                        :equiv "The name ~x0 is not currently the name of an ACL2 ~
                          equivalence relation.~@1  The current list of ~
                          ACL2 equivalence relations is ~x2."
                        equiv
                        (let ((pair (and (symbolp equiv)
                               (assoc-eq equiv (table-alist 'macro-aliases-table w)))))
                          (if (and pair (equivalence-relationp (cdr pair) w))
                            (msg "  Perhaps you intended the corresponding ~
                                     function for which it is an ~
                                     ``alias''(see :DOC macro-aliases-table), ~
                                     ~x0."
                              (cdr pair))
                            ""))
                        (getpropc 'equal 'coarsenings nil w))))))
              (if (find-equivalence-hyp-term old
                  (flatten-ands-in-lit-lst assumptions)
                  new
                  equiv
                  w)
                (mv-let (hitp new-current-term new-ttree)
                  (subst-equiv-expr1 equiv
                    new
                    old
                    (geneqv-at-subterm-top conc current-addr pc-ens w)
                    current-term
                    pc-ens
                    w
                    state
                    nil)
                  (if hitp
                    (mv-let (new-goal state)
                      (deposit-term-in-goal (car goals)
                        conc
                        current-addr
                        new-current-term
                        state)
                      (value (change-pc-state pc-state
                          :local-tag-tree new-ttree
                          :goals (cons new-goal (cdr goals)))))
                    (pprogn (print-no-change "The equivalence relation that you specified, namely ~x0, is ~
                          not appropriate at any occurrence of the ``old'' term ~x1 ~
                          inside the current term, and hence no substitution has ~
                          been made."
                        (list (cons #\0 equiv) (cons #\1 x)))
                      (value nil))))
                (pprogn (print-no-change "The ~#2~[equivalence~/equality~] of the terms ~x0 and ~x1~#2~[ with respect ~
              to the equivalence relation ~x3~/~] is not known at the ~
              current subterm from the current hypotheses and governors."
                    (list (cons #\0 x)
                      (cons #\1 y)
                      (cons #\2
                        (if (eq equiv 'equal)
                          1
                          0))
                      (cons #\3 equiv)))
                  (value nil))))
            (if erp
              (print-no-change2 "EQUIV failed.")
              (mv new-pc-state state))))))))

(define-pc-primitive casesplit
  (expr &optional use-hyps-flag do-not-flatten-flag)
  (mv-let (erp term state)
    (trans0 expr abbreviations :casesplit)
    (if erp
      (print-no-change2 "~x0 failed."
        (list (cons #\0 (cons :casesplit args))))
      (let ((claimed-term (if use-hyps-flag
             (mv-let (current-term governors)
               (fetch-term-and-cl conc current-addr nil)
               (declare (ignore current-term))
               (cond ((eq governors t) (er hard
                     ':casesplit
                     "Found governors of T inside command ~x0!"
                     (cons :casesplit args)))
                 (governors (fcons-term* 'implies (conjoin governors) term))
                 (t term)))
             term)))
        (mv (change-pc-state pc-state
            :goals (cons (change goal
                (car goals)
                :hyps (append hyps
                  (if do-not-flatten-flag
                    (list claimed-term)
                    (flatten-ands-in-lit claimed-term)))
                :depends-on (1+ depends-on))
              (cons (change goal
                  (car goals)
                  :hyps (append hyps
                    (if do-not-flatten-flag
                      (list (dumb-negate-lit claimed-term))
                      (flatten-ands-in-lit (dumb-negate-lit claimed-term))))
                  :goal-name (cons goal-name depends-on)
                  :depends-on 1)
                (cdr goals))))
          state)))))

(define-pc-macro top?
  nil
  (when-goals-trip (if (current-addr t)
      (value 'top)
      (value 'skip))))

(define-pc-macro contrapose-last
  nil
  (when-goals-trip (let ((hyps (hyps)))
      (if (null hyps)
        (pprogn (print-no-change "CONTRAPOSE-LAST failed -- no top-level hypotheses!")
          (value :fail))
        (value (list :contrapose (length hyps)))))))

(define-pc-macro drop-last
  nil
  (when-goals-trip (let ((hyps (hyps)))
      (if (null hyps)
        (pprogn (print-no-change "DROP-LAST failed -- no top-level hypotheses!")
          (value :fail))
        (value (list :drop (length hyps)))))))

(define-pc-macro drop-conc
  nil
  (value `(do-strict top? contrapose-last drop-last)))

(define-pc-atomic-macro claim
  (expr &rest rest-args)
  (when-goals-trip (value (let ((rest-args-1 (if (and rest-args
               (car rest-args)
               (not (keywordp (car rest-args))))
             (list* :hints :none (cdr rest-args))
             rest-args)))
        (mv-let (pairs remaining-rest-args)
          (pair-keywords '(:do-not-flatten) rest-args-1)
          (let ((do-not-flatten-flag (cdr (assoc-eq :do-not-flatten pairs))) (temp (cadr (member-eq :hints rest-args-1))))
            (if (and temp (atom temp))
              `(protect (casesplit ,EXPR nil ,DO-NOT-FLATTEN-FLAG)
                change-goal
                drop-conc
                pro
                change-goal)
              `(protect (casesplit ,EXPR nil ,DO-NOT-FLATTEN-FLAG)
                change-goal
                drop-conc
                (prove ,@REMAINING-REST-ARGS)))))))))

(define-pc-atomic-macro induct
  (&optional raw-term)
  (when-goals-trip (if (and (goals t) (current-addr t))
      (pprogn (print-no-change "You must be at the top of the goal in order to use the ~
                INDUCT command.  Try TOP first.")
        (value :fail))
      (let ((raw-term (or raw-term t)))
        (value `(prove :hints (("Goal" :induct ,RAW-TERM
               :do-not-induct proof-builder
               :do-not *do-not-processes*))))))))

(defun print-on-separate-lines
  (vals evisc-tuple chan state)
  (declare (xargs :guard (true-listp vals)))
  (if (null vals)
    (newline chan state)
    (pprogn (io? proof-builder
        nil
        state
        (evisc-tuple chan vals)
        (fms "~x0"
          (list (cons #\0 (car vals)))
          chan
          state
          evisc-tuple))
      (print-on-separate-lines (cdr vals) evisc-tuple chan state))))

(define-pc-help goals
  nil
  (io? proof-builder
    nil
    state
    (state-stack)
    (when-goals (print-on-separate-lines (goal-names (goals t))
        nil
        (proofs-co state)
        state))))

(defun modified-error-triple-for-sequence
  (erp val success-expr state)
  (mv-let (new-erp stobjs-out-and-vals state)
    (state-global-let* ((pc-erp erp) (pc-val val))
      (trans-eval-default-warning success-expr :sequence state t))
    (let ((stobjs-out (car stobjs-out-and-vals)) (vals (cdr stobjs-out-and-vals)))
      (if new-erp
        (mv new-erp nil state)
        (if (or (< (length stobjs-out) 2)
            (car stobjs-out)
            (cadr stobjs-out))
          (pprogn (io? proof-builder
              nil
              state
              (vals success-expr)
              (fms0 "~|WARNING -- evaluation of ~
                                      `success-expr' argument to ~
                                      :SEQUENCE, ~x0, has been ~
                                      ignored because it returned a ~
                                      single-threaded object in one ~
                                      of its first two values or ~
                                      returned fewer than two values. ~
                                      The value(s) returned was ~
                                      (were):~%~ ~ ~x1.~%"
                (list (cons #\0 success-expr) (cons #\1 vals))))
            (mv erp val state))
          (mv (car vals) (cadr vals) state))))))

(define-pc-meta sequence
  (instr-list &optional
    strict-flg
    protect-flg
    success-expr
    no-prompt-flg
    no-restore-flg)
  (if (not (true-listp instr-list))
    (pprogn (print-no-change "The first argument to the SEQUENCE command must be ~
                a true list, but~%~ ~ ~x0~| is not."
        (list (cons #\0 instr-list)))
      (mv t nil state))
    (state-global-let* ((pc-info (change pc-info
           (f-get-global 'pc-info state)
           :prompt (string-append (pc-prompt-depth-prefix) (pc-prompt)))))
      (let ((saved-old-ss (old-ss)) (saved-ss (state-stack)))
        (mv-let (erp val state)
          (pc-main-loop instr-list
            (if strict-flg
              '(signal value)
              '(signal))
            t
            (and (null no-prompt-flg) (pc-print-prompt-and-instr-flg))
            state)
          (mv-let (erp val state)
            (if success-expr
              (modified-error-triple-for-sequence erp
                val
                success-expr
                state)
              (mv erp val state))
            (if (and protect-flg (or erp (null val)))
              (pprogn (print-no-change "SEQUENCE failed, with protection on.  ~
                                     Reverting back to existing state of the ~
                                     proof-builder.~|")
                (pc-assign state-stack saved-ss)
                (pc-assign old-ss saved-old-ss)
                (mv erp val state))
              (pprogn (if no-restore-flg
                  state
                  (pc-assign old-ss saved-ss))
                (mv erp val state)))))))))

(define-pc-macro negate
  (&rest instr-list)
  (value (list :sequence instr-list
      nil
      nil
      '(mv nil
        (if (or (f-get-global 'pc-erp state)
            (null (f-get-global 'pc-val state)))
          t
          nil)))))

(define-pc-macro succeed
  (&rest instr-list)
  (mv nil
    (list :sequence instr-list nil nil '(mv nil t))
    state))

(define-pc-macro do-all
  (&rest instr-list)
  (mv nil (list :sequence instr-list) state))

(define-pc-macro do-strict
  (&rest instr-list)
  (mv nil (list :sequence instr-list t) state))

(define-pc-macro do-all-no-prompt
  (&rest instr-list)
  (mv nil (list :sequence instr-list nil nil nil t t) state))

(define-pc-macro th
  (&optional hyps-indices govs-indices)
  (declare (ignore hyps-indices govs-indices))
  (when-goals-trip (value `(do-all-no-prompt (hyps ,@ARGS)
        (lisp (io? proof-builder
            nil
            state
            nil
            (fms0 "~%The current subterm is:~%")))
        p))))

(define-pc-macro protect
  (&rest instr-list)
  (mv nil (list :sequence instr-list t t) state))

(defun extract-goal
  (name goals)
  (if (consp goals)
    (if (equal (access goal (car goals) :goal-name) name)
      (mv (car goals) (cdr goals))
      (mv-let (goal rest-goals)
        (extract-goal name (cdr goals))
        (mv goal (cons (car goals) rest-goals))))
    (mv nil goals)))

(define-pc-primitive change-goal
  (&optional name end-flg)
  (cond ((null goals) (pprogn (print-all-goals-proved-message state)
        (mv nil state)))
    ((null (cdr goals)) (print-no-change2 "The current goal is the only unproved goal."))
    ((null name) (pprogn (io? proof-builder
          nil
          state
          (goals)
          (fms0 "~|Now proving ~X0n.~%"
            (list (cons #\0 (access goal (cadr goals) :goal-name))
              (cons #\n nil))))
        (mv (change-pc-state pc-state
            :goals (if end-flg
              (cons (cadr goals) (append (cddr goals) (list (car goals))))
              (list* (cadr goals) (car goals) (cddr goals))))
          state)))
    ((equal name goal-name) (print-no-change2 "The current goal is already ~x0."
        (list (cons #\0 name))))
    (t (mv-let (gl rest-goals)
        (extract-goal name (cdr goals))
        (if gl
          (mv (change-pc-state pc-state
              :goals (if end-flg
                (cons gl (append rest-goals (list (car goals))))
                (cons gl (cons (car goals) rest-goals))))
            state)
          (print-no-change2 "There is no unproved goal named ~x0."
            (list (cons #\0 name))))))))

(define-pc-macro cg
  (&optional name)
  (value `(change-goal ,NAME t)))

(defun change-by-position
  (lst index new)
  (declare (xargs :guard (and (true-listp lst)
        (integerp index)
        (<= 0 index)
        (< index (length lst)))))
  (if (equal index 0)
    (cons new (cdr lst))
    (cons (car lst)
      (change-by-position (cdr lst) (1- index) new))))

(define-pc-primitive contrapose
  (&optional n)
  (let ((n (if args
         n
         1)))
    (if hyps
      (if current-addr
        (print-no-change2 "You must be at the top of the conclusion to apply ~
                               the CONTRAPOSE command.  Try TOP first.")
        (if (and (integerp n) (< 0 n) (<= n (length hyps)))
          (mv (change-pc-state pc-state
              :goals (cons (change goal
                  (car goals)
                  :hyps (change-by-position hyps (1- n) (dumb-negate-lit conc))
                  :conc (dumb-negate-lit (nth (1- n) hyps)))
                (cdr goals)))
            state)
          (print-no-change2 "The argument to CONTRAPOSE must be a positive integer ~
                               that does not exceed the length of the list of top-level ~
                               hypotheses.  The argument ~x0 fails to meet this requirement."
            (list (cons #\0 n)))))
      (print-no-change2 "There are no top-level hypotheses."))))

(define-pc-macro contradict
  (&optional n)
  (declare (ignore n))
  (value (cons :contrapose args)))

(define-pc-atomic-macro pro
  nil
  (value '(quiet (repeat promote))))

(define-pc-atomic-macro nx
  nil
  (when-goals-trip (let ((current-addr (current-addr t)))
      (if current-addr
        (value `(protect up ,(1+ (CAR (LAST CURRENT-ADDR)))))
        (pprogn (print-no-change "NX failed:  already at the top!")
          (value :fail))))))

(define-pc-atomic-macro bk
  nil
  (when-goals-trip (let ((current-addr (current-addr t)))
      (if current-addr
        (let ((n (car (last current-addr))))
          (if (equal n 1)
            (pprogn (print-no-change "BK failed:  already at the first argument!")
              (value :fail))
            (value `(do-strict up ,(1- N)))))
        (pprogn (print-no-change "BK failed:  already at the top!")
          (value :fail))))))

(define-pc-help p-top
  nil
  (when-goals (let ((conc (conc t)) (current-addr (current-addr t))
        (stars (intern$ "***" (f-get-global 'current-package state))))
      (io? proof-builder
        nil
        state
        (state-stack current-addr conc stars)
        (fms0 "~|~y0~|"
          (list (cons #\0
              (untrans0 (deposit-term conc
                  current-addr
                  (list stars (fetch-term conc current-addr) stars))
                t
                (abbreviations t)))))))))

(define-pc-macro repeat
  (instr)
  (value `(succeed (repeat-rec ,INSTR))))

(define-pc-macro repeat-rec
  (instr)
  (value `(do-strict ,INSTR (repeat-rec ,INSTR))))

(defmacro define-pc-bind*
  (name &rest args)
  `(define-pc-meta ,NAME
    (&rest instr-list)
    (state-global-let* (,@ARGS)
      (pc-main-loop instr-list
        nil
        t
        (pc-print-prompt-and-instr-flg)
        state))))

(define-pc-bind* quiet
  (inhibit-output-lst (union-eq '(prove proof-builder proof-tree warning observation)
      (f-get-global 'inhibit-output-lst state))))

(define-pc-bind* quiet!
  (print-clause-ids nil)
  (gag-mode nil)
  (inhibit-output-lst (if (member-eq 'error (f-get-global 'inhibit-output-lst state))
      *valid-output-names*
      (set-difference-eq *valid-output-names* '(error)))))

(define-pc-bind* noise
  (gag-mode nil)
  (inhibit-output-lst '(proof-tree)))

(define-pc-bind* noise!
  (gag-mode nil)
  (inhibit-output-lst nil))

(defun find-equivalence-hyp-term-no-target
  (index term hyps equiv w)
  (if (consp hyps)
    (mv-let (h c)
      (split-implies (car hyps))
      (if (or (variablep c)
          (fquotep c)
          (not (symbolp (ffn-symb c)))
          (not (refinementp (ffn-symb c) equiv w)))
        (find-equivalence-hyp-term-no-target (1+ index)
          term
          (cdr hyps)
          equiv
          w)
        (let* ((x (fargn c 1)) (y (fargn c 2))
            (hyp-to-use (and (subsetp-equal h hyps)
                (or (and (equal x term) y) (and (equal y term) x)))))
          (if hyp-to-use
            (mv index hyp-to-use)
            (find-equivalence-hyp-term-no-target (1+ index)
              term
              (cdr hyps)
              equiv
              w)))))
    (mv nil nil)))

(define-pc-atomic-macro if-not-proved
  (goal-name cmd)
  (if (member-equal goal-name (goal-names (goals t)))
    (if (equal goal-name (goal-name t))
      (value cmd)
      (mv-let (erp val state)
        (er soft
          'if-not-proved
          "The proof-builder's atomic macro IF-NOT-PROVED requires the ~
              indicated goal to be the current goal.  However, the current ~
              goal is ~p0 while the first argument to IF-NOT-PROVED is ~p1."
          (goal-name t)
          goal-name)
        (declare (ignore erp val))
        (value 'fail)))
    (value :skip)))

(define-pc-atomic-macro =
  (&optional x y &rest rest-args)
  (when-goals-trip (let ((conc (conc t)) (hyps (hyps t))
        (current-addr (current-addr t))
        (abbreviations (abbreviations t))
        (w (w state))
        (rest-args-1 (if (and rest-args
              (car rest-args)
              (not (keywordp (car rest-args))))
            (append '(:hints :none) (cdr rest-args))
            rest-args)))
      (if (not (keyword-value-listp rest-args-1))
        (pprogn (print-no-change "The ``rest-args'' arguments for the = command should be ~
                   empty or a list, either (i) containing one element, an ~
                   atom, or else (ii) of even length with keywords in the odd ~
                   positions.  Thus your command ~p0 is not legal.  See the ~
                   documentation for examples and details."
            (list (cons #\0 (make-pretty-pc-instr (cons := args)))))
          (value :fail))
        (mv-let (equiv-alist rest-args-1)
          (if (keyword-value-listp rest-args-1)
            (pair-keywords '(:equiv) rest-args-1)
            (mv nil rest-args-1))
          (let ((equiv (or (cdr (assoc-eq :equiv equiv-alist)) 'equal)))
            (mv-let (current-term governors)
              (fetch-term-and-cl conc current-addr nil)
              (cond ((eq governors t) (value (er hard
                      ':=
                      "Found governors of T inside command ~p0!"
                      (cons := args))))
                ((eq x :&) (pprogn (print-no-change "We do not allow the first argument of the = command ~
                         to be the keyword :&, because no other symbol with ~
                         print-name & can be a term (and hence we use it to ~
                         represent the current subterm), but :& is a ~
                         legitimate term and -- we can't be really sure ~
                         whether you intended it to represent the term :& or ~
                         the current subterm.")
                    (value :fail)))
                ((not (member-eq equiv (getpropc 'equal 'coarsenings nil w))) (pprogn (print-no-change "The ``equivalence relation'' that you supplied, ~p0, is not ~
                  known to ACL2 as an equivalence relation.~@1"
                      (list (cons #\0 equiv)
                        (cons #\1
                          (let ((pair (and (symbolp equiv)
                                 (assoc-eq equiv (table-alist 'macro-aliases-table w)))))
                            (if (and pair (equivalence-relationp (cdr pair) w))
                              (msg "  Perhaps you intended the ~
                                         corresponding function for which it ~
                                         is an ``alias''(see :DOC ~
                                         macro-aliases-table), ~x0."
                                (cdr pair))
                              "")))))
                    (value :fail)))
                ((null args) (mv-let (found-hyp new)
                    (find-equivalence-hyp-term-no-target 1
                      current-term
                      (flatten-ands-in-lit-lst (append hyps governors))
                      equiv
                      w)
                    (if found-hyp
                      (pprogn (io? proof-builder
                          nil
                          state
                          (found-hyp)
                          (fms0 "Using hypothesis #~x0.~%"
                            (list (cons #\0 found-hyp))))
                        (value (list :equiv current-term new)))
                      (pprogn (print-no-change "There is no hypothesis or governor that equates ~
                             the current term ~#0~[under the equivalence ~
                             relation ~p1 ~/~]with anything."
                          (list (cons #\0
                              (if (eq equiv 'equal)
                                1
                                0))
                            (cons #\1 equiv)))
                        (value :fail)))))
                (t (mv-let (rest-args-alist tail)
                    (pair-keywords '(:otf-flg :hints) rest-args-1)
                    (declare (ignore rest-args-alist))
                    (if tail
                      (pprogn (print-no-change "The only keywords allowed in the arguments to the = ~
                        command are :otf-flg, :hints, and :equiv.  Your ~
                        instruction ~p1 violates this requirement."
                          (list (cons #\1 (make-pretty-pc-instr (cons := args)))))
                        (value :fail))
                      (er-let* ((old (if (or (null (cdr args))
                               (and (symbolp x) (eq (intern-in-keyword-package x) :&)))
                             (value current-term)
                             (trans0 x abbreviations ':=))) (new (if (null (cdr args))
                              (trans0 x abbreviations ':=)
                              (trans0 y abbreviations ':=))))
                        (value (list :protect (list* :claim (if governors
                                (fcons-term* 'implies
                                  (conjoin governors)
                                  (list equiv old new))
                                (list equiv old new))
                              :do-not-flatten t
                              rest-args-1)
                            (list :equiv old new equiv)
                            (list :if-not-proved (goal-name t) :drop-last)))))))))))))))

(define-pc-macro set-success
  (instr form)
  (value `(sequence (,INSTR) nil nil ,FORM)))

(define-pc-macro orelse
  (instr1 instr2)
  (value `(negate (do-strict (negate ,INSTR1) (negate ,INSTR2)))))

(defun applicable-rewrite-rules
  (current-term conc
    current-addr
    target-name-or-rune
    target-index
    ens
    wrld)
  (declare (xargs :guard (not (or (variablep current-term)
          (fquotep current-term)
          (flambdap (ffn-symb current-term))))))
  (applicable-rewrite-rules1 current-term
    (geneqv-at-subterm-top conc current-addr ens wrld)
    (getpropc (ffn-symb current-term) 'lemmas nil wrld)
    1
    target-name-or-rune
    target-index
    wrld))

(define-pc-help show-rewrites
  (&optional rule-id enabled-only-flg)
  (when-goals (let ((conc (conc t)) (current-addr (current-addr t))
        (w (w state)))
      (let ((ens (make-pc-ens (pc-ens t) state)) (current-term (fetch-term conc current-addr))
          (abbreviations (abbreviations t))
          (term-id-iff (term-id-iff conc current-addr t))
          (all-hyps (union-equal (hyps t) (governors conc current-addr))))
        (show-rewrites-linears-fn 'show-rewrites
          rule-id
          enabled-only-flg
          ens
          current-term
          abbreviations
          term-id-iff
          all-hyps
          (geneqv-at-subterm-top conc current-addr ens w)
          nil
          state)))))

(define-pc-macro sr
  (&rest args)
  (value (cons :show-rewrites args)))

(define-pc-help show-linears
  (&optional rule-id enabled-only-flg)
  (when-goals (let ((conc (conc t)) (current-addr (current-addr t))
        (w (w state)))
      (let ((ens (make-pc-ens (pc-ens t) state)) (current-term (fetch-term conc current-addr))
          (abbreviations (abbreviations t))
          (term-id-iff (term-id-iff conc current-addr t))
          (all-hyps (union-equal (hyps t) (governors conc current-addr))))
        (show-rewrites-linears-fn 'show-linears
          rule-id
          enabled-only-flg
          ens
          current-term
          abbreviations
          term-id-iff
          all-hyps
          (geneqv-at-subterm-top conc current-addr ens w)
          nil
          state)))))

(define-pc-macro sls
  (&rest args)
  (value (cons :show-linears args)))

(define-pc-macro pl
  (&optional x)
  (cond (x (value `(lisp (pl ',X))))
    ((null (goals)) (pprogn (print-all-goals-proved-message state)
        (value 'skip)))
    (t (let* ((conc (conc t)) (current-addr (current-addr t))
          (current-term (fetch-term conc current-addr)))
        (cond ((or (variablep current-term)
             (fquotep current-term)
             (flambda-applicationp current-term)) (er soft
              'pl
              "The current subterm is not the application of a ~
                         function symbol."))
          (t (value `(lisp (pl ',(FFN-SYMB CURRENT-TERM))))))))))

(define-pc-macro pr
  (&optional x)
  (cond (x (value `(lisp (pr ',X))))
    ((null (goals)) (pprogn (print-all-goals-proved-message state)
        (value 'skip)))
    (t (let* ((conc (conc t)) (current-addr (current-addr t))
          (current-term (fetch-term conc current-addr)))
        (cond ((or (variablep current-term)
             (fquotep current-term)
             (flambda-applicationp current-term)) (er soft
              'pr
              "The current subterm is not the application of a ~
                         function symbol."))
          (t (value `(lisp (pr ',(FFN-SYMB CURRENT-TERM))))))))))

(define-pc-help show-type-prescriptions
  (&optional rule-id)
  (when-goals (let ((conc (conc t)) (current-addr (current-addr t)))
      (let ((ens (make-pc-ens (pc-ens t) state)) (current-term (fetch-term conc current-addr))
          (abbreviations (abbreviations t))
          (all-hyps (union-equal (hyps t) (governors conc current-addr))))
        (show-type-prescription-rules current-term
          rule-id
          abbreviations
          all-hyps
          ens
          state)))))

(define-pc-macro st
  (&rest args)
  (value (cons :show-type-prescriptions args)))

(defun translate-subst-abb1
  (sub abbreviations state)
  (declare (xargs :guard (symbol-alistp sub)))
  (if (consp sub)
    (mv-let (erp term state)
      (trans0 (cadar sub) abbreviations 'translate-subst-abb1)
      (if erp
        (mv "~|Translation error for ~x0 caused error in ~
                       translating ~xs.~|"
          (list (cons #\0 (cadar sub)))
          state)
        (mv-let (erp val state)
          (translate-subst-abb1 (cdr sub) abbreviations state)
          (if erp
            (mv erp val state)
            (mv nil (cons (cons (caar sub) term) val) state)))))
    (mv nil nil state)))

(defun single-valued-symbolp-alistp
  (alist)
  (declare (xargs :guard (symbol-alistp alist)))
  (if alist
    (and (not (assoc-eq (caar alist) (cdr alist)))
      (single-valued-symbolp-alistp (cdr alist)))
    t))

(defun check-cars-are-variables
  (alist state)
  (declare (xargs :guard (symbol-alistp alist)))
  (if alist
    (mv-let (erp val state)
      (trans0 (caar alist) nil)
      (if (or erp (not (eq val (caar alist))))
        (pprogn (io? proof-builder
            nil
            state
            (alist)
            (fms0 "~|A substitution must be an alist whose CARs ~
                               are variables, but the entry ~x0 violates this ~
                               property.~|"
              (list (cons #\0 (caar alist)))))
          (mv t state))
        (check-cars-are-variables (cdr alist) state)))
    (mv nil state)))

(defun translate-subst-abb
  (sub abbreviations state)
  (cond ((not (true-listp sub)) (pprogn (io? proof-builder
          nil
          state
          (sub)
          (fms0 "~|A substitution must be a true (nil-terminated) ~
                        list, but~%~x0 is not.~|"
            (list (cons #\0 sub))))
        (mv t nil state)))
    ((not (and (symbol-alistp sub) (single-valued-symbolp-alistp sub))) (pprogn (io? proof-builder
          nil
          state
          (sub)
          (fms0 "~|A substitution must be an alist of pairs without ~
                        duplicate keys, but ~x0 is not.~|"
            (list (cons #\0 sub))))
        (mv t nil state)))
    (t (mv-let (erp state)
        (check-cars-are-variables sub state)
        (if erp
          (mv t nil state)
          (mv-let (erp val state)
            (translate-subst-abb1 sub abbreviations state)
            (if erp
              (pprogn (io? proof-builder
                  nil
                  state
                  (val sub erp)
                  (fms0 erp (cons (cons #\s sub) val)))
                (mv t nil state))
              (mv nil val state))))))))

(defun make-rewrite-instr
  (lemma-id raw-subst instantiate-free)
  (list* (make-pretty-pc-command :rewrite)
    lemma-id
    (cond (instantiate-free (list raw-subst instantiate-free))
      (raw-subst (list raw-subst))
      (t nil))))

(define-pc-primitive rewrite
  (&optional rule-id raw-sub instantiate-free)
  (mv-let (erp sub state)
    (translate-subst-abb raw-sub abbreviations state)
    (if erp
      (print-no-change2 "~x0 failed."
        (list (cons #\0 (cons :rewrite args))))
      (let ((name (and (symbolp rule-id) rule-id)) (rune (and (consp rule-id)
              (member-eq (car rule-id) '(:rewrite :definition))
              rule-id))
          (index (if (and (integerp rule-id) (< 0 rule-id))
              rule-id
              (if rule-id
                nil
                1)))
          (pc-ens (make-pc-ens pc-ens state))
          (w (w state))
          (current-term (fetch-term conc current-addr))
          (assumptions (union-equal hyps (governors conc current-addr))))
        (cond ((or (variablep current-term)
             (fquotep current-term)
             (flambdap (ffn-symb current-term))) (print-no-change2 "It is only possible to apply rewrite rules to terms that are not ~
           variables, (quoted) constants, or applications of lambda ~
           expressions.  However, the current term is:~%~ ~ ~y0.~|"
              (list (cons #\0 current-term))))
          ((not (or name index rune)) (print-no-change2 "The rule-id argument to REWRITE must be a name, a positive ~
           integer, or a :rewrite or :definition rune, but ~x0 is none of ~
           these.~|"
              (list (cons #\0 rule-id))))
          (t (mv-let (flg hyps-type-alist ttree)
              (hyps-type-alist assumptions pc-ens w state)
              (declare (ignore ttree))
              (if flg
                (print-no-change2 "Contradiction in the hypotheses!~%The S command should ~
                complete this goal.~|")
                (let ((app-rewrite-rules (applicable-rewrite-rules current-term
                       conc
                       current-addr
                       (or name rune)
                       index
                       pc-ens
                       w)))
                  (if (null app-rewrite-rules)
                    (if (and index (> index 1))
                      (print-no-change2 "There are fewer than ~x0 applicable rewrite rules.~%"
                        (list (cons #\0 index)))
                      (print-no-change2 "There are no applicable rewrite rules.~%"))
                    (let* ((sar (car app-rewrite-rules)) (lemma (access sar sar :lemma))
                        (start-alist (access sar sar :alist))
                        (alist (append start-alist sub))
                        (rhs (access rewrite-rule lemma :rhs))
                        (lemma-hyps (access rewrite-rule lemma :hyps))
                        (lemma-rune (access rewrite-rule lemma :rune))
                        (lemma-name (base-symbol lemma-rune))
                        (lemma-id (if (cddr lemma-rune)
                            lemma-rune
                            lemma-name))
                        (non-free (union-eq (intersection-domains sub start-alist)
                            (set-difference-eq (strip-cars sub)
                              (append (all-vars rhs) (all-vars1-lst lemma-hyps nil))))))
                      (if non-free
                        (print-no-change2 "The variable~#0~[~/~/s~] ~&1 supplied by the ~
                        substitution in this instruction ~#0~[~/is~/are~] not ~
                        free for instantiation in the current context.~|"
                          (list (cons #\0 (zero-one-or-more (length non-free)))
                            (cons #\1 non-free)))
                        (mv-let (subst-hyps unify-subst ttree2)
                          (unrelieved-hyps lemma-rune
                            lemma-hyps
                            alist
                            hyps-type-alist
                            instantiate-free
                            w
                            state
                            pc-ens
                            nil)
                          (pprogn (let ((extra-alist (alist-difference-eq unify-subst alist)))
                              (if extra-alist
                                (io? proof-builder
                                  nil
                                  state
                                  (abbreviations extra-alist sub lemma-id)
                                  (fms0 "~|Rewriting with ~x0 under the ~
                                        following extension of the ~
                                        substitution generated by matching ~
                                        that rewrite rule with the current ~
                                        term~#1~[ (after extending it with ~
                                        the substitution ~x2 supplied in the ~
                                        instruction)~/~]:~|~x3.~|"
                                    (list (cons #\0 lemma-id)
                                      (cons #\1
                                        (if sub
                                          0
                                          1))
                                      (cons #\2 sub)
                                      (cons #\3
                                        (untranslate-subst-abb extra-alist abbreviations state)))))
                                (io? proof-builder
                                  nil
                                  state
                                  (lemma-id)
                                  (fms0 "~|Rewriting with ~x0.~|" (list (cons #\0 lemma-id))))))
                            (let ((runes (all-runes-in-ttree ttree2 nil)))
                              (if runes
                                (io? proof-builder
                                  nil
                                  state
                                  (runes)
                                  (fms0 "~|--NOTE-- Using the following runes ~
                                        in addition to the indicated rule:~%  ~
                                        ~x0.~|"
                                    (list (cons #\0 runes))))
                                state))
                            (let ((new-goals (make-new-goals-fixed-hyps subst-hyps
                                   assumptions
                                   goal-name
                                   depends-on)))
                              (mv-let (changed-goal state)
                                (deposit-term-in-goal (car goals)
                                  conc
                                  current-addr
                                  (sublis-var unify-subst (access rewrite-rule lemma :rhs))
                                  state)
                                (mv (change-pc-state pc-state
                                    :instruction (make-rewrite-instr lemma-id raw-sub instantiate-free)
                                    :goals (cons (change goal
                                        changed-goal
                                        :depends-on (+ depends-on (length new-goals)))
                                      (append new-goals (cdr goals)))
                                    :local-tag-tree (push-lemma lemma-rune ttree2))
                                  state)))))))))))))))))

(defun applicable-linear-rules
  (current-term target-name-or-rune target-index wrld)
  (declare (xargs :guard (not (or (variablep current-term)
          (fquotep current-term)
          (flambdap (ffn-symb current-term))))))
  (applicable-linear-rules1 current-term
    (getpropc (ffn-symb current-term) 'linear-lemmas nil wrld)
    1
    target-name-or-rune
    target-index))

(defun make-linear-instr
  (lemma-id raw-subst instantiate-free)
  (list* (make-pretty-pc-command :apply-linear)
    lemma-id
    (cond (instantiate-free (list raw-subst instantiate-free))
      (raw-subst (list raw-subst))
      (t nil))))

(define-pc-primitive apply-linear
  (&optional rule-id raw-sub instantiate-free)
  (mv-let (erp sub state)
    (translate-subst-abb raw-sub abbreviations state)
    (if erp
      (print-no-change2 "~x0 failed."
        (list (cons #\0 (cons :rewrite args))))
      (let ((name (and (symbolp rule-id) rule-id)) (rune (and (consp rule-id)
              (member-eq (car rule-id) '(:linear))
              rule-id))
          (index (if (and (integerp rule-id) (< 0 rule-id))
              rule-id
              (if rule-id
                nil
                1)))
          (pc-ens (make-pc-ens pc-ens state))
          (w (w state))
          (current-term (fetch-term conc current-addr))
          (assumptions (union-equal hyps (governors conc current-addr))))
        (cond ((or (variablep current-term)
             (fquotep current-term)
             (flambdap (ffn-symb current-term))) (print-no-change2 "It is only possible to apply linear rules to terms that are not ~
           variables, (quoted) constants, or applications of lambda ~
           expressions.  However, the current term is:~%~ ~ ~y0.~|"
              (list (cons #\0 current-term))))
          ((not (or name index rune)) (print-no-change2 "The rule-id argument to REWRITE must be a name, a positive ~
           integer, or a :linear rune, but ~x0 is none of these.~|"
              (list (cons #\0 rule-id))))
          (t (mv-let (flg hyps-type-alist ttree)
              (hyps-type-alist assumptions pc-ens w state)
              (declare (ignore ttree))
              (if flg
                (print-no-change2 "Contradiction in the hypotheses!~%The S command should ~
                complete this goal.~|")
                (let ((app-linear-rules (applicable-linear-rules current-term
                       (or name rune)
                       index
                       w)))
                  (if (null app-linear-rules)
                    (if (and index (> index 1))
                      (print-no-change2 "There are fewer than ~x0 applicable linear rules.~%"
                        (list (cons #\0 index)))
                      (print-no-change2 "There are no applicable linear rules.~%"))
                    (let* ((sar (car app-linear-rules)) (lemma (access sar sar :lemma))
                        (start-alist (access sar sar :alist))
                        (alist (append start-alist sub))
                        (lemma-concl (access linear-lemma lemma :concl))
                        (lemma-hyps (access linear-lemma lemma :hyps))
                        (lemma-rune (access linear-lemma lemma :rune))
                        (lemma-name (base-symbol lemma-rune))
                        (lemma-id (if (cddr lemma-rune)
                            lemma-rune
                            lemma-name))
                        (non-free (union-eq (intersection-domains sub start-alist)
                            (set-difference-eq (strip-cars sub)
                              (append (all-vars lemma-concl)
                                (all-vars1-lst lemma-hyps nil))))))
                      (if non-free
                        (print-no-change2 "The variable~#0~[~/~/s~] ~&1 supplied by the ~
                        substitution in this instruction ~#0~[~/is~/are~] not ~
                        free for instantiation in the current context.~|"
                          (list (cons #\0 (zero-one-or-more (length non-free)))
                            (cons #\1 non-free)))
                        (mv-let (subst-hyps unify-subst ttree2)
                          (unrelieved-hyps lemma-rune
                            lemma-hyps
                            alist
                            hyps-type-alist
                            instantiate-free
                            w
                            state
                            pc-ens
                            nil)
                          (pprogn (let ((extra-alist (alist-difference-eq unify-subst alist)))
                              (if extra-alist
                                (io? proof-builder
                                  nil
                                  state
                                  (abbreviations extra-alist sub lemma-id)
                                  (fms0 "~|Apply linear rule ~x0 under the ~
                                        following extension of the ~
                                        substitution generated by matching ~
                                        that rule's trigger term with the ~
                                        current term ~#1~[ (after extending ~
                                        it with the substitution ~x2 supplied ~
                                        in the instruction)~/~]:  ~x3.~|"
                                    (list (cons #\0 lemma-id)
                                      (cons #\1
                                        (if sub
                                          0
                                          1))
                                      (cons #\2 sub)
                                      (cons #\3
                                        (untranslate-subst-abb extra-alist abbreviations state)))))
                                (io? proof-builder
                                  nil
                                  state
                                  (lemma-id)
                                  (fms0 "~|Applying linear rule ~x0.~|"
                                    (list (cons #\0 lemma-id))))))
                            (let ((runes (all-runes-in-ttree ttree2 nil)))
                              (if runes
                                (io? proof-builder
                                  nil
                                  state
                                  (runes)
                                  (fms0 "~|--NOTE-- Using the following runes ~
                                        in addition to the indicated rule:~%  ~
                                        ~x0.~|"
                                    (list (cons #\0 runes))))
                                state))
                            (let ((new-goals (make-new-goals-fixed-hyps subst-hyps
                                   assumptions
                                   goal-name
                                   depends-on)))
                              (let ((changed-goal (change goal
                                     (car goals)
                                     :hyps (append hyps (list (sublis-var unify-subst lemma-concl)))
                                     :depends-on (+ depends-on (length new-goals)))))
                                (mv (change-pc-state pc-state
                                    :instruction (make-linear-instr lemma-id raw-sub instantiate-free)
                                    :goals (cons changed-goal (append new-goals (cdr goals)))
                                    :local-tag-tree (push-lemma lemma-rune ttree2))
                                  state)))))))))))))))))

(define-pc-macro al
  (&rest args)
  (value (cons :apply-linear args)))

(define-pc-macro doc
  (&optional name)
  (let ((name (or name (make-official-pc-command 'doc))))
    (cond ((and (equal (assoc-eq :doc (ld-keyword-aliases state))
           '(:doc 1 xdoc))
         (function-symbolp 'colon-xdoc-initialized (w state))) (value `(lisp (if (colon-xdoc-initialized state)
              (xdoc ',NAME)
              (pprogn (fms0 "Note: Using built-in :doc command.  To use ~
                                   :xdoc command, exit the proof-builder and ~
                                   run :doc in the top-level loop.~|~%")
                (doc ',NAME))))))
      (t (value `(lisp (doc ',NAME)))))))

(define-pc-macro help
  (&optional name)
  (cond ((not (symbolp name)) (pprogn (print-no-change "The argument for :HELP requires a symbol, but ~x0 ~
                            is not a symbol."
          (list (cons #\0 name)))
        (value :fail)))
    (t (let ((name (if (equal (symbol-name name) "ALL")
             'proof-builder-commands
             (make-official-pc-command (or name 'help)))))
        (value `(doc ,NAME))))))

(defun pc-rewrite*-1
  (term type-alist
    geneqv
    iff-flg
    wrld
    rcnst
    old-ttree
    pot-lst
    normalize-flg
    rewrite-flg
    ens
    state
    repeat
    backchain-limit
    step-limit)
  (mv-let (nterm old-ttree)
    (if normalize-flg
      (normalize term
        iff-flg
        type-alist
        ens
        wrld
        old-ttree
        (backchain-limit wrld :ts))
      (mv term old-ttree))
    (sl-let (newterm ttree)
      (if rewrite-flg
        (let ((gstack nil))
          (rewrite-entry (rewrite nterm nil 'proof-builder)
            :pequiv-info nil
            :rdepth (rewrite-stack-limit wrld)
            :step-limit step-limit
            :obj '?
            :fnstack nil
            :ancestors nil
            :simplify-clause-pot-lst pot-lst
            :rcnst (change rewrite-constant
              rcnst
              :current-literal (make current-literal :atm nterm :not-flg nil))
            :gstack gstack
            :ttree old-ttree))
        (mv 0 nterm old-ttree))
      (declare (ignorable step-limit))
      (cond ((equal newterm nterm) (mv step-limit newterm old-ttree state))
        ((<= repeat 0) (mv step-limit newterm ttree state))
        (t (pc-rewrite*-1 newterm
            type-alist
            geneqv
            iff-flg
            wrld
            rcnst
            ttree
            pot-lst
            normalize-flg
            rewrite-flg
            ens
            state
            (1- repeat)
            backchain-limit
            step-limit))))))

(defun pc-rewrite*
  (term type-alist
    geneqv
    iff-flg
    wrld
    rcnst
    old-ttree
    pot-lst
    normalize-flg
    rewrite-flg
    ens
    state
    repeat
    backchain-limit
    step-limit)
  (sl-let (newterm ttree state)
    (catch-step-limit (pc-rewrite*-1 term
        type-alist
        geneqv
        iff-flg
        wrld
        rcnst
        old-ttree
        pot-lst
        normalize-flg
        rewrite-flg
        ens
        state
        repeat
        backchain-limit
        step-limit))
    (cond ((eql step-limit -1) (mv step-limit term old-ttree state))
      (t (mv step-limit newterm ttree state)))))

(defun make-goals-from-assumptions
  (assumptions conc hyps current-addr goal-name start-index)
  (if assumptions
    (cons (make goal
        :conc conc
        :hyps (cons (dumb-negate-lit (car assumptions)) hyps)
        :current-addr current-addr
        :goal-name (cons goal-name start-index)
        :depends-on 1)
      (make-goals-from-assumptions (cdr assumptions)
        conc
        hyps
        current-addr
        goal-name
        (1+ start-index)))
    nil))

(defun make-new-goals-from-assumptions
  (assumptions goal)
  (and assumptions
    (make-goals-from-assumptions assumptions
      (access goal goal :conc)
      (access goal goal :hyps)
      (access goal goal :current-addr)
      (access goal goal :goal-name)
      (access goal goal :depends-on))))

(defconst *default-s-repeat-limit* 10)

(defun hyps-type-alist-and-pot-lst
  (assumptions rcnst ens wrld state)
  (mv-let (flg type-alist ttree-or-fc-pair-lst)
    (hyps-type-alist assumptions ens wrld state)
    (cond ((or (not rcnst) flg) (mv flg type-alist nil ttree-or-fc-pair-lst))
      (t (mv-let (step-limit contradictionp pot-lst)
          (setup-simplify-clause-pot-lst (dumb-negate-lit-lst assumptions)
            nil
            ttree-or-fc-pair-lst
            type-alist
            rcnst
            wrld
            state
            *default-step-limit*)
          (declare (ignore step-limit))
          (cond (contradictionp (mv t
                nil
                nil
                (push-lemma *fake-rune-for-linear*
                  (access poly contradictionp :ttree))))
            (t (mv nil type-alist pot-lst ttree-or-fc-pair-lst))))))))

(define-pc-primitive s
  (&rest args)
  (cond ((not (keyword-value-listp args)) (print-no-change2 "The argument list to S must be a KEYWORD-VALUE-LISTP, i.e. a list of ~
      the form (:kw-1 val-1 ... :kw-n val-n), where each of the arguments ~
      :kw-i is a keyword.  Your argument list ~x0 does not have this ~
      property.  Try (HELP S)."
        (list (cons #\0 args))))
    (t (let ((comm (make-official-pc-command 's)) (w (w state))
          (current-term (fetch-term conc current-addr))
          (assumptions (union-equal hyps
              (flatten-ands-in-lit-lst (governors conc current-addr)))))
        (let ((pc-ens (make-pc-ens pc-ens state)))
          (mv-let (bcl-alist rst)
            (pair-keywords '(:backchain-limit :normalize :rewrite :repeat)
              args)
            (let* ((local-backchain-limit (or (cdr (assoc-eq :backchain-limit bcl-alist)) 0)) (normalize (let ((pair (assoc-eq :normalize bcl-alist)))
                    (if pair
                      (cdr pair)
                      t)))
                (rewrite (let ((pair (assoc-eq :rewrite bcl-alist)))
                    (if pair
                      (cdr pair)
                      t)))
                (linear (let ((pair (assoc-eq :linear bcl-alist)))
                    (if pair
                      (cdr pair)
                      rewrite)))
                (repeat (let ((pair (assoc-eq :repeat bcl-alist)))
                    (if pair
                      (if (equal (cdr pair) t)
                        *default-s-repeat-limit*
                        (cdr pair))
                      0))))
              (cond ((not (natp repeat)) (print-no-change2 "The :REPEAT argument provided to S (or a command that invoked ~
                S), which was ~x0, is illegal. ~ It must be T or a natural ~
                number."
                    (list (cons #\0 repeat))))
                ((not (natp local-backchain-limit)) (print-no-change2 "The :BACKCHAIN-LIMIT argument provided to S (or a command ~
                that invoked S), which was ~x0, is illegal.  It must be NIL ~
                or a natural number."
                    (list (cons #\0 local-backchain-limit))))
                ((not (or normalize rewrite)) (print-no-change2 "You may not specify in the S command that ~
                                 neither IF normalization nor rewriting is to ~
                                 take place."))
                ((and (null rewrite)
                   (or (assoc-eq :backchain-limit bcl-alist)
                     (assoc-eq :repeat bcl-alist)
                     rst)) (print-no-change2 "When the :REWRITE NIL option is specified, ~
                                 it is not allowed to provide arguments other ~
                                 than :NORMALIZE T.  The argument list ~x0 ~
                                 violates this requirement."
                    (list (cons #\0 args))))
                (t (mv-let (key-alist new-rst)
                    (pair-keywords '(:in-theory :hands-off :expand) rst)
                    (declare (ignore key-alist))
                    (cond (new-rst (print-no-change2 "The arguments to the S command must all be &KEY ~
                    arguments, which should be among ~&0.  Your argument list ~
                    ~x1 violates this requirement."
                          (list (cons #\0
                              '(:rewrite :normalize :backchain-limit :repeat :in-theory :hands-off :expand))
                            (cons #\1 args))))
                      (t (mv-let (erp hint-settings state)
                          (translate-hint-settings comm
                            "Goal"
                            rst
                            (if args
                              (cons comm (car args))
                              comm)
                            w
                            state)
                          (cond (erp (print-no-change2 "S failed."))
                            (t (let ((base-rcnst (and rewrite (make-rcnst pc-ens w state :force-info t))))
                                (mv-let (flg hyps-type-alist pot-lst ttree)
                                  (hyps-type-alist-and-pot-lst assumptions
                                    (and linear base-rcnst)
                                    pc-ens
                                    w
                                    state)
                                  (cond (flg (cond ((or (null current-addr)
                                           (equal assumptions hyps)
                                           (mv-let (flg hyps-type-alist ttree)
                                             (hyps-type-alist hyps pc-ens w state)
                                             (declare (ignore hyps-type-alist ttree))
                                             flg)) (pprogn (io? proof-builder
                                              nil
                                              state
                                              nil
                                              (fms0 "~|Goal proved:  Contradiction in ~
                                           the hypotheses!~|"))
                                            (mv (change-pc-state pc-state
                                                :goals (cond ((tagged-objects 'assumption ttree) (cons (change goal (car goals) :conc *t*) (cdr goals)))
                                                  (t (cdr goals)))
                                                :local-tag-tree ttree)
                                              state)))
                                        (t (print-no-change2 "A contradiction was found in the current ~
                                context using both the top-level hypotheses ~
                                and the IF tests governing the current term, ~
                                but not using the top-level hypotheses alone. ~
                                ~ You may want to issue the TOP command and ~
                                then issue s-prop to prune some branches of ~
                                the conclusion."))))
                                    (t (mv-let (erp local-rcnst state)
                                        (if rewrite
                                          (load-hint-settings-into-rcnst hint-settings
                                            base-rcnst
                                            nil
                                            w
                                            's
                                            state)
                                          (value nil))
                                        (pprogn (if erp
                                            (io? proof-builder
                                              nil
                                              state
                                              nil
                                              (fms0 "~|Note: Ignoring the above ~
                                               theory invariant error.  ~
                                               Proceeding...~|"))
                                            state)
                                          (if rewrite
                                            (maybe-warn-about-theory-from-rcnsts base-rcnst
                                              local-rcnst
                                              :s pc-ens
                                              w
                                              state)
                                            state)
                                          (sl-let (new-term new-ttree state)
                                            (pc-rewrite* current-term
                                              hyps-type-alist
                                              (geneqv-at-subterm-top conc current-addr pc-ens w)
                                              (term-id-iff conc current-addr t)
                                              w
                                              local-rcnst
                                              nil
                                              pot-lst
                                              normalize
                                              rewrite
                                              pc-ens
                                              state
                                              repeat
                                              local-backchain-limit
                                              (initial-step-limit w state))
                                            (pprogn (f-put-global 'last-step-limit step-limit state)
                                              (if (equal new-term current-term)
                                                (print-no-change2 "No simplification took place.")
                                                (pprogn (mv-let (new-goal state)
                                                    (deposit-term-in-goal (car goals)
                                                      conc
                                                      current-addr
                                                      new-term
                                                      state)
                                                    (mv (change-pc-state pc-state
                                                        :goals (cons new-goal (cdr goals))
                                                        :local-tag-tree new-ttree)
                                                      state)))))))))))))))))))))))))))

(defun build-pc-enabled-structure-from-ens
  (new-suffix ens)
  (let* ((new-name-root '(#\P #\C
         #\-
         #\E
         #\N
         #\A
         #\B
         #\L
         #\E
         #\D
         #\-
         #\A
         #\R
         #\R
         #\A
         #\Y
         #\-)) (new-name (intern (coerce (append new-name-root
              (explode-nonnegative-integer new-suffix 10 nil))
            'string)
          "ACL2"))
      (old-name (access enabled-structure ens :array-name))
      (old-alist (access enabled-structure ens :theory-array)))
    (change enabled-structure
      ens
      :theory-array (cons (list :header :dimensions (dimensions old-name old-alist)
          :maximum-length (maximum-length old-name old-alist)
          :default (default old-name old-alist)
          :name new-name)
        (cdr old-alist))
      :array-name new-name
      :array-length (access enabled-structure ens :array-length)
      :array-name-root new-name-root
      :array-name-suffix new-suffix)))

(define-pc-primitive in-theory
  (&optional theory-expr)
  (let ((w (w state)) (ens (ens state)))
    (if args
      (mv-let (erp hint-setting state)
        (translate-in-theory-hint theory-expr
          t
          'in-theory
          w
          state)
        (if erp
          (print-no-change2 "bad theory expression.")
          (let* ((new-suffix (pc-value next-pc-enabled-array-suffix)) (new-pc-ens1 (build-pc-enabled-structure-from-ens new-suffix ens)))
            (mv-let (erp new-pc-ens2 state)
              (load-theory-into-enabled-structure theory-expr
                hint-setting
                nil
                new-pc-ens1
                nil
                nil
                w
                'in-theory
                state)
              (cond (erp (print-no-change2 "bad theory expression."))
                (t (pprogn (pc-assign next-pc-enabled-array-suffix (1+ new-suffix))
                    (maybe-warn-about-theory-simple ens
                      new-pc-ens2
                      :in-theory w
                      state)
                    (mv (change-pc-state pc-state :pc-ens new-pc-ens2) state))))))))
      (if (null pc-ens)
        (print-no-change2 "The proof-builder enabled/disabled state is ~
                             already set to agree with the global state, so ~
                             your IN-THEORY command is redundant.")
        (mv (change-pc-state pc-state :pc-ens nil) state)))))

(define-pc-atomic-macro s-prop
  (&rest names)
  (value `(s :in-theory ,(IF NAMES
     `(UNION-THEORIES ',NAMES (THEORY 'MINIMAL-THEORY))
     '(THEORY 'MINIMAL-THEORY)))))

(define-pc-atomic-macro x
  (&rest args)
  (value `(do-strict (expand t) (succeed (s ,@ARGS)))))

(define-pc-primitive expand
  (&optional do-not-expand-lambda-flg)
  (let ((w (w state)) (term (fetch-term conc current-addr)))
    (cond ((or (variablep term) (fquotep term)) (print-no-change2 "It is impossible to expand a variable or a constant."))
      ((and do-not-expand-lambda-flg (flambdap (ffn-symb term))) (print-no-change2 "Expansion of lambda terms is disabled when do-not-expand-lambda-flg = ~
        t; see :DOC acl2-pc::expand."))
      (t (let* ((fn (ffn-symb term)) (def-body (and (not (flambdap fn)) (def-body fn w)))
            (formals (and def-body (access def-body def-body :formals)))
            (equiv (and def-body (access def-body def-body :equiv)))
            (body (if (flambdap fn)
                (lambda-body fn)
                (and def-body
                  (latest-body (fcons-term fn formals)
                    (access def-body def-body :hyp)
                    (access def-body def-body :concl))))))
          (cond ((null body) (assert$ (not (flambdap fn))
                (print-no-change2 "Expansion failed.  Apparently function ~x0 is ~
                     constrained, not defined."
                  (list (cons #\0 fn)))))
            ((and (not (eq equiv 'equal))
               (not (flambdap fn))
               (not (geneqv-refinementp equiv
                   (geneqv-at-subterm-top conc
                     current-addr
                     (make-pc-ens pc-ens state)
                     w)
                   w))) (print-no-change2 "Expansion failed: the equivalence relation for the definition ~
            rule ~x0 is ~x1, which is not sufficient to maintain in the ~
            current context."
                (list (cons #\0 (base-symbol (access def-body def-body :rune)))
                  (cons #\1 equiv))))
            (t (let ((new-term (cond (do-not-expand-lambda-flg (fcons-term (make-lambda formals body) (fargs term)))
                     (t (subcor-var (if (flambdap fn)
                           (lambda-formals fn)
                           formals)
                         (fargs term)
                         body)))))
                (mv-let (new-goal state)
                  (deposit-term-in-goal (car goals)
                    conc
                    current-addr
                    new-term
                    state)
                  (mv (change-pc-state pc-state
                      :goals (cons new-goal (cdr goals))
                      :local-tag-tree (if (flambdap fn)
                        nil
                        (push-lemma? (access def-body def-body :rune) nil)))
                    state))))))))))

(define-pc-atomic-macro x-dumb nil (value `(expand t)))

(define-pc-macro bookmark
  (tag &rest instr-list)
  (value `(do-all (comment :begin ,TAG)
      ,@INSTR-LIST
      (comment :end ,TAG))))

(defun change-last
  (lst val)
  (if (consp lst)
    (if (consp (cdr lst))
      (cons (car lst) (change-last (cdr lst) val))
      (list val))
    lst))

(defun assign-event-name-and-rule-classes
  (event-name rule-classes state)
  (let* ((state-stack (state-stack)) (triple (event-name-and-types-and-raw-term state-stack))
      (old-event-name (car triple))
      (old-rule-classes (cadr triple))
      (old-raw-term (caddr triple)))
    (pc-assign state-stack
      (change-last state-stack
        (change pc-state
          (car (last state-stack))
          :instruction (list :start (list (or event-name old-event-name)
              (or rule-classes old-rule-classes)
              old-raw-term)))))))

(defun save-fn
  (name ss-alist state)
  (pprogn (assign-event-name-and-rule-classes name nil state)
    (pc-assign ss-alist
      (put-assoc-eq name (cons (state-stack) (old-ss)) ss-alist))))

(define-pc-macro save
  (&optional name do-it-flg)
  (cond ((not (symbolp name)) (pprogn (print-no-change "The first argument supplied to ~x0 must be a symbol, but ~x1 is not a ~
       symbol.~@2"
          (list (cons #\0 :save)
            (cons #\1 name)
            (cons #\2
              (cond ((and (consp name)
                   (eq (car name) 'quote)
                   (consp (cdr name))
                   (symbolp (cadr name))
                   (null (cddr name))) (msg "  Perhaps you intended to submit the form ~x0."
                    `(:save ,(CADR NAME) ,@(AND DO-IT-FLG (LIST DO-IT-FLG)))))
                (t "")))))
        (value :fail)))
    (t (let ((name (or name
             (car (event-name-and-types-and-raw-term state-stack)))) (ss-alist (ss-alist)))
        (if name
          (mv-let (erp reply state)
            (if (and (assoc-eq name ss-alist) (null do-it-flg))
              (acl2-query 'save
                '("The name ~x0 is already associated with a ~
                              state-stack.  Do you really want to overwrite ~
                              that existing value?" :y t
                  :n nil)
                (list (cons #\0 name))
                state)
              (mv nil t state))
            (declare (ignore erp))
            (if reply
              (pprogn (save-fn name ss-alist state) (value :succeed))
              (pprogn (print-no-change "save aborted.") (value :fail))))
          (pprogn (print-no-change "You can't SAVE with no argument, because you didn't ~
                  originally enter VERIFY using an event name.  Try (SAVE ~
                  <event_name>) instead.")
            (value :fail)))))))

(defmacro retrieve
  (&optional name)
  `(retrieve-fn ',NAME state))

(define-pc-macro retrieve
  nil
  (pprogn (print-no-change "RETRIEVE can only be used outside the ~
                            interactive loop.  Please exit first.  To ~
                            save your state upon exit, use EX rather than EXIT.")
    (value :fail)))

(defun unsave-fn
  (name state)
  (pc-assign ss-alist (remove1-assoc-eq name (ss-alist))))

(defmacro unsave (name) `(unsave-fn ',NAME state))

(define-pc-help unsave
  (&optional name)
  (let ((name (or name
         (car (event-name-and-types-and-raw-term state-stack)))))
    (if (null name)
      (print-no-change "You must specify a name to UNSAVE, because you didn't ~
                          originally enter VERIFY using an event name.")
      (if (assoc-eq name (ss-alist))
        (pprogn (unsave-fn name state)
          (io? proof-builder
            nil
            state
            (name)
            (fms0 "~|~x0 removed from saved state-stack alist.~%"
              (list (cons #\0 name)))))
        (print-no-change "~|~x0 is does not have a value on the saved ~
                          state-stack alist.~%"
          (list (cons #\0 name)))))))

(defun show-retrieved-goal
  (state-stack state)
  (let ((raw-term (caddr (event-name-and-types-and-raw-term state-stack))))
    (assert$ raw-term
      (fmt-abbrev "~|~%Resuming proof attempt for~|~y0."
        (list (cons #\0 raw-term))
        0
        (proofs-co state)
        state
        "~%"))))

(defun retrieve-fn
  (name state)
  (let ((ss-alist (ss-alist)))
    (cond ((f-get-global 'in-verify-flg state) (er soft
          'retrieve
          "You are apparently already inside the VERIFY interactive loop.  It is ~
           illegal to enter such a loop recursively."))
      ((null ss-alist) (pprogn (io? proof-builder
            nil
            state
            nil
            (fms0 "Sorry -- there is no saved interactive proof to ~
                          re-enter! Perhaps you meant (VERIFY) rather than ~
                          (RETRIEVE).~|"))
          (value :invisible)))
      ((null name) (if (equal (length ss-alist) 1)
          (retrieve-fn (caar ss-alist) state)
          (pprogn (io? proof-builder
              nil
              state
              (ss-alist)
              (fms0 "Please specify an interactive verification to ~
                            re-enter.  Your options are ~&0.~%(Pick one of the ~
                            above:) "
                (list (cons #\0 (strip-cars ss-alist)))))
            (mv-let (erp val state)
              (read-object *standard-oi* state)
              (declare (ignore erp))
              (retrieve-fn val state)))))
      ((not (symbolp name)) (er soft
          'retrieve
          "The argument supplied to ~x0 must be a symbol, but ~x1 is not a ~
           symbol.~@2"
          'retrieve
          name
          (cond ((and (consp name)
               (eq (car name) 'quote)
               (consp (cdr name))
               (symbolp (cadr name))
               (null (cddr name))) (msg "  Perhaps you intended to submit the form ~x0."
                `(retrieve ,(CADR NAME))))
            (t ""))))
      (t (let* ((ss-pair (cdr (assoc-eq name ss-alist))) (saved-ss (car ss-pair))
            (saved-old-ss (cdr ss-pair)))
          (if saved-ss
            (pprogn (pc-assign old-ss saved-old-ss)
              (pc-assign state-stack saved-ss)
              (show-retrieved-goal saved-ss state)
              (verify))
            (pprogn (io? proof-builder
                nil
                state
                (name)
                (fms0 "~|Sorry -- There is no interactive proof saved ~
                              under the name ~x0.~|"
                  (list (cons #\0 name))))
              (value :invisible))))))))

(defun print-all-goals
  (goals state)
  (if (null goals)
    state
    (pprogn (print-pc-goal (car goals))
      (print-all-goals (cdr goals) state))))

(define-pc-help print-all-goals
  nil
  (print-all-goals (goals t) state))

(defmacro print-conc
  (&optional goal)
  `(let ((goal ,(OR GOAL '(CAR (ACCESS PC-STATE (CAR (STATE-STACK)) :GOALS)))))
    (io? proof-builder
      nil
      state
      (goal)
      (if goal
        (fms0 "~%-------  ~x3  -------~|~q0~|"
          (list (cons #\0
              (untranslate (access goal goal :conc) t (w state)))
            (cons #\3 (access goal goal :goal-name))))
        (fms0 "~%No goal in CAR of state-stack.~|")))))

(defun print-all-concs
  (goals state)
  (declare (xargs :mode :program :stobjs state))
  (if (null goals)
    state
    (pprogn (print-conc (car goals))
      (print-all-concs (cdr goals) state))))

(define-pc-help print-all-concs
  nil
  (print-all-concs (goals t) state))

(defun gen-var-marker
  (x)
  (or (null x) (and (integerp x) (>= x 0))))

(defun translate-generalize-alist-1
  (alist state-vars abbreviations state)
  (cond ((null alist) (value nil))
    ((and (true-listp (car alist)) (eql (length (car alist)) 2)) (er-let* ((term (translate-abb (caar alist)
             abbreviations
             'translate-generalize-alist
             state)) (var (if (gen-var-marker (cadar alist))
              (value (cadar alist))
              (translate-abb (cadar alist)
                nil
                'translate-generalize-alist
                state))))
        (cond ((member-eq var state-vars) (er soft
              :generalize "The variable ~x0 already appears in the current goals of ~
            the proof-builder state, and hence is not legal as a ~
            generalization variable."
              var))
          ((or (variablep var) (gen-var-marker var)) (mv-let (erp val state)
              (translate-generalize-alist-1 (cdr alist)
                state-vars
                abbreviations
                state)
              (if erp
                (mv erp val state)
                (value (cons (cons term var) val)))))
          (t (er soft
              :generalize "The second element of each doublet ~
            given to the GENERALIZE command must be a variable or ~
            natural number, but ~x0 is neither."
              (cadar alist))))))
    (t (er soft
        :generalize "Each argument to the GENERALIZE command must be a list of ~
         length 2, but ~x0 is not."
        (car alist)))))

(defun non-gen-var-markers
  (alist)
  (if (consp alist)
    (if (gen-var-marker (cdar alist))
      (non-gen-var-markers (cdr alist))
      (cons (cdar alist) (non-gen-var-markers (cdr alist))))
    nil))

(defun find-duplicate-generalize-entries
  (alist var)
  (declare (xargs :guard (true-listp alist)))
  (if alist
    (if (eq (cadar alist) var)
      (cons (car alist)
        (find-duplicate-generalize-entries (cdr alist) var))
      (find-duplicate-generalize-entries (cdr alist) var))
    nil))

(defun translate-generalize-alist-2
  (alist avoid-list)
  (declare (xargs :guard (true-listp alist)))
  (if alist
    (if (gen-var-marker (cdar alist))
      (let ((new-var (genvar 'genvar "_" (cdar alist) avoid-list)))
        (cons (cons (caar alist) new-var)
          (translate-generalize-alist-2 (cdr alist)
            (cons new-var avoid-list))))
      (cons (car alist)
        (translate-generalize-alist-2 (cdr alist) avoid-list)))
    nil))

(defun translate-generalize-alist
  (alist state-vars abbreviations state)
  (er-let* ((alist1 (translate-generalize-alist-1 alist
         state-vars
         abbreviations
         state)))
    (let ((new-vars (non-gen-var-markers alist1)))
      (if (no-duplicatesp-equal new-vars)
        (value (translate-generalize-alist-2 alist1
            (append new-vars state-vars)))
        (let* ((bad-var (car (duplicates new-vars))) (dup-entries (find-duplicate-generalize-entries alist bad-var)))
          (if (cdr dup-entries)
            (er soft
              'generalize
              "The pairs ~&0 have the same variable, ~x1, and hence your ~
                  GENERALIZE instruction is illegal."
              dup-entries
              bad-var)
            (value (er hard
                'generalize
                "Bad call to translate-generalize-alist on ~%  ~x0."
                (list alist state-vars abbreviations)))))))))

(defun all-vars-goals
  (goals)
  (if (consp goals)
    (union-eq (all-vars (access goal (car goals) :conc))
      (union-eq (all-vars1-lst (access goal (car goals) :hyps) nil)
        (all-vars-goals (cdr goals))))
    nil))

(defun pc-state-vars
  (pc-state)
  (union-eq (all-vars1-lst (strip-cdrs (access pc-state pc-state :abbreviations))
      nil)
    (all-vars-goals (access pc-state pc-state :goals))))

(define-pc-primitive generalize
  (&rest args)
  (cond (current-addr (print-no-change2 "Generalization may only be applied at the top of the current goal.  Try TOP first."))
    ((null args) (print-no-change2 "GENERALIZE requires at least one argument."))
    (t (mv-let (erp alist state)
        (translate-generalize-alist args
          (pc-state-vars pc-state)
          abbreviations
          state)
        (if erp
          (print-no-change2 "GENERALIZE failed.")
          (mv (change-pc-state pc-state
              :goals (cons (change goal
                  (car goals)
                  :hyps (sublis-expr-lst alist (access goal (car goals) :hyps))
                  :conc (sublis-expr alist (access goal (car goals) :conc)))
                (cdr goals)))
            state))))))

(define-pc-atomic-macro use
  (&rest args)
  (value `(prove :hints (("Goal" :use ,ARGS
         :do-not-induct proof-builder
         :do-not *do-not-processes*))
      :otf-flg t)))

(define-pc-atomic-macro clause-processor
  (&rest cl-proc-hints)
  (value `(:prove :hints (("Goal" :clause-processor (,@CL-PROC-HINTS)
         :do-not-induct proof-builder
         :do-not *do-not-processes*))
      :otf-flg t)))

(define-pc-macro cl-proc
  (&rest cl-proc-hints)
  (value `(:clause-processor ,@CL-PROC-HINTS)))

(define-pc-atomic-macro retain
  (arg1 &rest rest-args)
  (declare (ignore arg1 rest-args))
  (when-goals-trip (let* ((hyps (hyps t)) (bad-nums (non-bounded-nums args 1 (length hyps))))
      (if bad-nums
        (pprogn (print-no-change "The following are not in-range hypothesis numbers:  ~&0."
            (list (cons #\0 bad-nums)))
          (mv t nil state))
        (let ((retained-hyps (set-difference-eq (fromto 1 (length hyps)) args)))
          (if retained-hyps
            (value (cons :drop retained-hyps))
            (pprogn (print-no-change "All hypotheses are to be retained.")
              (mv t nil state))))))))

(define-pc-atomic-macro reduce
  (&rest hints)
  (if (alistp hints)
    (value (list :prove :hints (add-string-val-pair-to-string-val-alist! "Goal"
          :do-not-induct 'proof-builder
          hints)
        :otf-flg t))
    (pprogn (print-no-change "A REDUCE instruction must be of the form~%~ ~ ~
              (:REDUCE (goal_name_1 ...) ... (goal_name_n ...)),~%and hence ~
              your instruction,~%~ ~ ~x0,~%is not legal."
        (list (cons #\0 (cons :reduce hints))))
      (value :fail))))

(define-pc-macro run-instr-on-goal
  (instr goal-name)
  (when-goals-trip (if (equal goal-name (goal-name t))
      (value instr)
      (value `(protect (change-goal ,GOAL-NAME) ,INSTR)))))

(defun run-instr-on-goals-guts
  (instr goal-names)
  (declare (xargs :guard (true-listp goal-names)))
  (if goal-names
    (cons `(run-instr-on-goal ,INSTR ,(CAR GOAL-NAMES))
      (run-instr-on-goals-guts instr (cdr goal-names)))
    nil))

(define-pc-macro run-instr-on-new-goals
  (instr existing-goal-names &optional must-succeed-flg)
  (value (cons 'do-strict
      (run-instr-on-goals-guts (if must-succeed-flg
          instr
          (list :succeed instr))
        (set-difference-equal (goal-names (goals t))
          existing-goal-names)))))

(define-pc-macro then
  (instr &optional completion must-succeed-flg)
  (value (list 'do-strict
      instr
      (list 'run-instr-on-new-goals
        (or completion :reduce)
        (goal-names (goals t))
        must-succeed-flg))))

(define-pc-macro nil nil (value 'exit))

(define-pc-atomic-macro free
  (var)
  (er-let* ((var (trans0 var nil :free)))
    (if (variablep var)
      (value `(add-abbreviation ,VAR (hide ,VAR)))
      (pprogn (print-no-change "The FREE command requires an argument that is a variable, ~
                       which ~x0 is not."
          (list (cons #\0 var)))
        (value :fail)))))

(define-pc-macro replay
  (&optional n replacement-instr)
  (if (or (null n) (and (integerp n) (> n 0)))
    (let* ((len (length state-stack)) (n (and n (min (1+ n) len)))
        (instrs (instructions-of-state-stack (if n
              (take n state-stack)
              state-stack)
            nil)))
      (value `(do-strict (undo ,(1- (OR N LEN)))
          ,@(IF REPLACEMENT-INSTR
      (CONS REPLACEMENT-INSTR (CDR INSTRS))
      INSTRS))))
    (pprogn (print-no-change "The optional argument to the REPLAY command ~
                              must be a positive integer, but ~x0 is not!"
        (list (cons #\0 n)))
      (value :fail))))

(defun instr-name
  (instr)
  (if (atom instr)
    instr
    (car instr)))

(defun pc-free-instr-p
  (var pc-state)
  (let ((instr (access pc-state pc-state :instruction)))
    (and (eq (instr-name instr) :free) (eq (cadr instr) var))))

(defun find-possible-put
  (var state-stack)
  (if state-stack
    (if (pc-free-instr-p var (car state-stack))
      1
      (let ((n (find-possible-put var (cdr state-stack))))
        (and n (1+ n))))
    nil))

(define-pc-macro put
  (var expr)
  (let ((n (find-possible-put var state-stack)))
    (if n
      (value `(do-strict (replay ,N (add-abbreviation ,VAR ,EXPR))
          (remove-abbreviations ,VAR)))
      (pprogn (print-no-change "There is no FREE command for ~x0."
          (list (cons #\0 var)))
        (value :fail)))))

(define-pc-macro reduce-by-induction
  (&rest hints)
  (if (alistp hints)
    (value (cons :reduce (add-string-val-pair-to-string-val-alist "Goal"
          :induct t
          hints)))
    (pprogn (print-no-change "A REDUCE-BY-INDUCTION instruction must be of the form~%~ ~ ~
              (:REDUCE-BY-INDUCTION (goal_name_1 ...) ... (goal_name_n ...)),~%and hence ~
              your instruction,~%~ ~ ~x0,~%is not legal."
        (list (cons #\0 (cons :reduce-by-induction hints))))
      (value :fail))))

(define-pc-macro r
  (&rest args)
  (value (cons :rewrite args)))

(define-pc-atomic-macro sl
  (&optional backchain-limit)
  (value (if backchain-limit
      `(s :backchain-limit ,BACKCHAIN-LIMIT
        :in-theory (union-theories (theory 'minimal-theory)
          (set-difference-theories (current-theory :here)
            (function-theory :here))))
      `(s :in-theory (union-theories (theory 'minimal-theory)
          (set-difference-theories (current-theory :here)
            (function-theory :here)))))))

(define-pc-atomic-macro elim
  nil
  (value (list :prove :otf-flg t
      :hints '(("Goal" :do-not-induct proof-builder
         :do-not (set-difference-eq *do-not-processes*
           '(eliminate-destructors)))))))

(define-pc-macro ex nil (value '(do-strict save exit)))

(defun save-fc-report-settings
  nil
  (declare (xargs :guard t))
  (wormhole-eval 'fc-wormhole
    '(lambda (whs)
      (let* ((data (wormhole-data whs)) (criteria (cdr (assoc-eq :criteria data)))
          (flyp (cdr (assoc-eq :report-on-the-flyp data))))
        (set-wormhole-data whs
          (put-assoc-eq :criteria-saved criteria
            (put-assoc-eq :report-on-the-flyp-saved flyp data)))))
    nil))

(defun restore-fc-report-settings
  nil
  (declare (xargs :guard t))
  (wormhole-eval 'fc-wormhole
    '(lambda (whs)
      (let* ((data (wormhole-data whs)) (criteria-saved (cdr (assoc-eq :criteria-saved data)))
          (flyp-saved (cdr (assoc-eq :report-on-the-flyp-saved data))))
        (set-wormhole-data whs
          (put-assoc-eq :criteria criteria-saved
            (put-assoc-eq :report-on-the-flyp flyp-saved data)))))
    nil))

(defun proof-builder-assumptions
  (concl-flg govs-flg conc current-addr state-stack)
  (cond (concl-flg (union-equal (hyps t)
        (cond (govs-flg (add-to-set-equal (dumb-negate-lit conc)
              (governors conc current-addr)))
          (t (list (dumb-negate-lit conc))))))
    (govs-flg (union-equal (hyps t) (governors conc current-addr)))
    (t (hyps t))))

(define-pc-help type-alist
  (&optional concl-flg govs-flg fc-report-flg alistp)
  (when-goals (let ((conc (conc t)) (current-addr (current-addr t))
        (w (w state))
        (govs-flg (if (cdr args)
            govs-flg
            (not concl-flg))))
      (prog2$ (and fc-report-flg
          (prog2$ (save-fc-report-settings)
            (prog2$ (wormhole-eval 'fc-wormhole
                '(lambda (whs)
                  (set-wormhole-data whs
                    (put-assoc-eq :criteria '((t t t)) (wormhole-data whs))))
                nil)
              (set-fc-report-on-the-fly t))))
        (mv-let (flg hyps-type-alist ign)
          (hyps-type-alist (proof-builder-assumptions concl-flg
              govs-flg
              conc
              current-addr
              state-stack)
            (make-pc-ens (pc-ens t) state)
            w
            state)
          (declare (ignore ign))
          (prog2$ (and fc-report-flg (restore-fc-report-settings))
            (if flg
              (io? proof-builder
                nil
                state
                nil
                (fms0 "*** Contradiction in the hypotheses! ***~%The S ~
                        command should complete this goal.~|"))
              (io? proof-builder
                nil
                state
                (hyps-type-alist alistp w)
                (pprogn (fms0 "~|Current type-alist, including forward chaining:~%")
                  (prog2$ (cond ((eq alistp :raw) (cw "~x0~|" hyps-type-alist))
                      (alistp (cw "~x0~|"
                          (alist-to-doublets (decode-type-alist hyps-type-alist))))
                      (t (print-type-alist hyps-type-alist w nil)))
                    state))))))))))

(define-pc-help pot-lst
  (&optional concl-flg govs-flg rawp)
  (when-goals (let* ((conc (conc t)) (current-addr (current-addr t))
        (wrld (w state))
        (govs-flg (if (cdr args)
            govs-flg
            (not concl-flg)))
        (assumptions (proof-builder-assumptions concl-flg
            govs-flg
            conc
            current-addr
            state-stack))
        (clause (dumb-negate-lit-lst (expand-assumptions assumptions)))
        (ens (make-pc-ens (pc-ens t) state))
        (clause-pts (enumerate-elements clause 0)))
      (mv-let (contradictionp type-alist fc-pair-lst)
        (forward-chain-top 'pot-lst
          clause
          nil
          (ok-to-force-ens ens)
          nil
          wrld
          ens
          (match-free-override wrld)
          state)
        (cond (contradictionp (io? proof-builder
              nil
              state
              (concl-flg)
              (fms0 "*** Contradiction (from forward-chaining, towards ~
                     building a pot-lst)! ***~|~#0~[The S command should ~
                     complete this goal.~|~/~]"
                (list (cons #\0
                    (if concl-flg
                      1
                      0))))))
          (t (let ((rcnst (make-rcnst ens
                   wrld
                   state
                   :force-info (if (ffnnamep-lst 'if clause)
                     'weak
                     t)
                   :top-clause clause
                   :current-clause clause)))
              (mv-let (step-limit contradictionp pot-lst)
                (setup-simplify-clause-pot-lst clause
                  (pts-to-ttree-lst clause-pts)
                  fc-pair-lst
                  type-alist
                  rcnst
                  wrld
                  state
                  *default-step-limit*)
                (declare (ignore step-limit))
                (cond (contradictionp (io? proof-builder
                      nil
                      state
                      (concl-flg)
                      (fms0 "*** Contradiction from attempting to build a ~
                           pot-lst)! ***~|~#0~[The S command should complete ~
                           this goal.~|~/~]"
                        (list (cons #\0
                            (if concl-flg
                              1
                              0))))))
                  (t (io? proof-builder
                      nil
                      state
                      (pot-lst rawp)
                      (pprogn (fms0 "~|Current pot-lst:~%")
                        (prog2$ (if rawp
                            (cw "~x0~|" pot-lst)
                            (print-pot-lst pot-lst nil))
                          state)))))))))))))

(define-pc-macro print-main
  nil
  (value '(print (caddr (event-name-and-types-and-raw-term (state-stack))))))

(define-pc-macro pso nil (value '(lisp (pso))))

(define-pc-macro psog nil (value '(lisp (psog))))

(define-pc-macro pso! nil (value '(lisp (pso!))))

(define-pc-macro acl2-wrap (x) (value `(lisp ,X)))

(defmacro acl2-wrap (x) x)

(define-pc-macro check-proved-goal
  (goal-name cmd)
  (if (member-equal goal-name (goal-names (goals)))
    (er soft
      'check-proved
      "The command ~x0 failed to prove the goal ~x1."
      cmd
      goal-name)
    (value 'succeed)))

(define-pc-macro check-proved
  (x)
  (when-goals-trip (let ((goal-name (goal-name)))
      (value `(do-all ,X (quiet (check-proved-goal ,GOAL-NAME ,X)))))))

(define-pc-atomic-macro forwardchain
  (hypn &optional hints quiet-flg)
  (when-goals-trip (let* ((hyps (hyps)) (len (length hyps)))
      (cond ((null hyps) (mv-let (erp val state)
            (er soft
              'forwardchain
              "The are no top-level hypotheses.  Hence it makes no sense to ~
              forward chain here.")
            (declare (ignore erp val))
            (value 'fail)))
        ((and (integerp hypn) (< 0 hypn) (<= hypn len)) (let ((hyp (nth (1- hypn) hyps)))
            (case-match hyp
              (('implies ant consequent) (let ((instr `(protect (claim ,CONSEQUENT 0 :do-not-flatten t)
                       (drop ,HYPN)
                       change-goal
                       (demote ,HYPN)
                       (claim ,ANT
                         ,@(IF HINTS
      '(:HINTS HINTS)
      NIL))
                       (demote ,LEN)
                       (check-proved (s :backchain-limit 0 :in-theory (theory 'minimal-theory))))))
                  (if quiet-flg
                    (value (list 'quiet instr))
                    (value instr))))
              (& (mv-let (erp val state)
                  (er soft
                    'forwardchain
                    "The ~n0 hypothesis~|  ~x1~|is not of the form (implies x ~
                     y)."
                    (list hypn)
                    (untrans0 (nth (1- hypn) hyps) t (abbreviations)))
                  (declare (ignore erp val))
                  (value 'fail))))))
        (t (mv-let (erp val state)
            (er soft
              'forwardchain
              "The index ~x0 is not a valid index into the hypothesis list.  ~
                The valid indices are the integers from 1 to ~x1."
              hypn
              len)
            (declare (ignore erp val))
            (value 'fail)))))))

(define-pc-atomic-macro bdd
  (&rest kw-listp)
  (let ((bdd-hint (if (assoc-keyword :vars kw-listp)
         kw-listp
         (list* :vars nil kw-listp))))
    (value `(:prove :hints (("Goal" :bdd ,BDD-HINT))))))

(define-pc-macro runes
  (&optional flg)
  (value `(print (merge-sort-runes (all-runes-in-ttree (,(IF FLG
     'TAG-TREE
     'LOCAL-TAG-TREE))
          nil)))))

(define-pc-macro lemmas-used
  (&optional flg)
  (value `(runes ,FLG)))

(defun goal-terms
  (goals)
  (if (endp goals)
    nil
    (cons (make-implication (access goal (car goals) :hyps)
        (access goal (car goals) :conc))
      (goal-terms (cdr goals)))))

(defun wrap1-aux1
  (kept-goal-names all-goals kept-goals removed-goals)
  (cond ((endp all-goals) (mv (reverse kept-goals) (reverse removed-goals)))
    ((member-equal (access goal (car all-goals) :goal-name)
       kept-goal-names) (wrap1-aux1 kept-goal-names
        (cdr all-goals)
        (cons (car all-goals) kept-goals)
        removed-goals))
    (t (wrap1-aux1 kept-goal-names
        (cdr all-goals)
        kept-goals
        (cons (car all-goals) removed-goals)))))

(defun wrap1-aux2
  (sym index goals kept-goals removed-goals)
  (if (endp goals)
    (mv (reverse kept-goals) (reverse removed-goals))
    (let* ((goal (car goals)) (goal-name (access goal goal :goal-name)))
      (if (and (consp goal-name)
          (eq sym (car goal-name))
          (<= index (cdr goal-name)))
        (wrap1-aux2 sym
          index
          (cdr goals)
          kept-goals
          (cons (car goals) removed-goals))
        (wrap1-aux2 sym
          index
          (cdr goals)
          (cons (car goals) kept-goals)
          removed-goals)))))

(define-pc-primitive wrap1
  (&optional kept-goal-names)
  (let* ((current-goal (car goals)) (current-goal-name (access goal current-goal :goal-name)))
    (cond ((not (true-listp kept-goal-names)) (print-no-change2 "The (optional) argument to wrap1 must be a true list of goal names.  ~
        ~x0 is thus illegal."
          (list (cons #\0 kept-goal-names))))
      ((and (null kept-goal-names)
         (not (and (consp current-goal-name)
             (symbolp (car current-goal-name))
             (integerp (cdr current-goal-name))))) (print-no-change2 "The current goal's name, ~x0, is not of the form (SYMBOL . N) for ~
        integer N."
          (list (cons #\0 current-goal-name))))
      (t (mv-let (kept-goals removed-goals)
          (if kept-goal-names
            (wrap1-aux1 kept-goal-names (cdr goals) nil nil)
            (wrap1-aux2 (car current-goal-name)
              (cdr current-goal-name)
              (cdr goals)
              nil
              nil))
          (pprogn (io? proof-builder
              nil
              state
              (current-goal-name removed-goals)
              (if removed-goals
                (fms0 "~|Conjoining the following goals into the current ~
                         goal, ~x0:~|  ~X1n~%"
                  (list (cons #\0 current-goal-name)
                    (cons #\1 (goal-names removed-goals))
                    (cons #\n nil)))
                (fms0 "~|NOTE (wrap1): There are no goals to conjoin into the ~
                       current goal, but we proceed anyhow.~%")))
            (mv (change-pc-state pc-state
                :goals (cons (change goal
                    current-goal
                    :conc (conjoin (goal-terms (cons current-goal removed-goals)))
                    :hyps nil
                    :current-addr nil)
                  kept-goals))
              state)))))))

(define-pc-atomic-macro wrap
  (&rest instrs)
  (cond ((null instrs) (pprogn (print-no-change "Wrap takes at least one argument.")
        (value :fail)))
    (t (let ((goal-names (goal-names (goals t))))
        (value `(sequence ((do-all ,@INSTRS) (quiet (wrap1 ,GOAL-NAMES))
              (lisp (io? proof-builder
                  nil
                  state
                  nil
                  (let ((new-current-goal-name (access goal (car (goals)) :goal-name)) (state-stack (state-stack)))
                    (when-goals (fms0 (if (member-equal new-current-goal-name ',GOAL-NAMES)
                          "~|~%NOTE: Created no new goals.  Current ~
                                     goal:~%  ~X0n~|"
                          "~|~%NOTE: Created ONLY one new goal, which ~
                                   is the current goal:~%  ~X0n~|")
                        (list (cons #\0 new-current-goal-name) (cons #\n nil))))))))
            t
            nil
            nil
            t))))))

(define-pc-atomic-macro wrap-induct
  (&optional raw-term)
  (value (if raw-term
      `(wrap (induct ,RAW-TERM))
      `(wrap induct))))

(define-pc-macro finish-error
  (instrs)
  (er soft
    'finish
    "~%The following instruction list created at least one subgoal:~|~x0~|"
    instrs))

(define-pc-macro finish
  (&rest instrs)
  (value `(then (check-proved (do-strict ,@INSTRS))
      (finish-error ,INSTRS)
      t)))

(define-pc-macro geneqv
  (&optional with-runes-p)
  (value `(print (show-geneqv (geneqv-at-subterm-top (conc)
          (current-addr)
          (make-pc-ens (pc-ens) state)
          (w state))
        ',WITH-RUNES-P))))

(defun goals-to-clause-list
  (goals)
  (if (endp goals)
    nil
    (cons (append (dumb-negate-lit-lst (access goal (car goals) :hyps))
        (list (access goal (car goals) :conc)))
      (goals-to-clause-list (cdr goals)))))

(defun proof-builder-clause-list
  (state)
  (goals-to-clause-list (goals)))

(defun ttree-to-summary-data
  (ttree)
  (and ttree
    (mv-let (use-names by-names cl-proc-fns)
      (cl-proc-data-in-ttree ttree nil)
      (make-summary-data :runes (all-runes-in-ttree ttree nil)
        :use-names (append use-names (use-names-in-ttree ttree nil))
        :by-names (append by-names (by-names-in-ttree ttree nil))
        :clause-processor-fns cl-proc-fns))))

(defun proof-builder-cl-proc-1
  (cl instr-list state)
  (let ((ctx 'proof-builder-cl-proc))
    (cond ((null cl) (er soft
          ctx
          "There is no legal way to prove a goal of NIL!"))
      ((not (true-listp instr-list)) (er soft
          ctx
          "The value of the :INSTRUCTIONS hint must be a true ~
           (null-terminated) list.  The value ~x0 is thus illegal."
          instr-list))
      (t (let ((term (make-implication (dumb-negate-lit-lst (butlast cl 1))
               (car (last cl)))) (wrld (w state))
            (new-pc-depth (1+ (pc-value pc-depth))))
          (er-let* ((new-inhibit-output-lst (cond ((and (consp instr-list)
                    (true-listp (car instr-list))
                    (eq (make-pretty-pc-command (caar instr-list)) :comment)
                    (eq (cadar instr-list) 'inhibit-output-lst)) (cond ((eq (caddar instr-list) :same) (value (f-get-global 'inhibit-output-lst state)))
                     (t (chk-inhibit-output-lst (caddar instr-list)
                         :instructions state))))
                 (t (value (union-eq '(prove proof-tree proof-builder)
                       (f-get-global 'inhibit-output-lst state)))))) (outputp (value (not (subsetp-eq '(prove proof-builder proof-tree)
                      new-inhibit-output-lst)))))
            (state-global-let* ((inhibit-output-lst new-inhibit-output-lst) (pc-output (f-get-global 'pc-output state)))
              (mv-let (erp clause-list state)
                (pprogn (pc-assign pc-depth new-pc-depth)
                  (cond (outputp (io? prove
                        nil
                        state
                        (new-pc-depth)
                        (fms0 "~|~%[[~x0> Executing ~
                                            proof-builder instructions]]~%~%"
                          (list (cons #\0 new-pc-depth)))))
                    (t state))
                  (pc-assign next-pc-enabled-array-suffix
                    (1+ (pc-value next-pc-enabled-array-suffix)))
                  (mv-let (erp pc-val state)
                    (pc-main term
                      (untranslate term t wrld)
                      nil
                      nil
                      instr-list
                      '(signal value)
                      t
                      nil
                      state)
                    (pprogn (cond (outputp (io? prove
                            nil
                            state
                            (new-pc-depth)
                            (fms0 "~|~%[[<~x0 Completed ~
                                                 proof-builder ~
                                                 instructions]]~%"
                              (list (cons #\0 new-pc-depth)))))
                        (t state))
                      (cond ((or erp (null pc-val)) (let ((name (intern (concatenate 'string
                                   "ERROR"
                                   (coerce (explode-atom new-pc-depth 10) 'string))
                                 "KEYWORD")))
                            (pprogn (io? error
                                nil
                                state
                                (name)
                                (fms0 "~%Saving proof-builder error ~
                                            state; see :DOC instructions.  To ~
                                            retrieve:~|~x0"
                                  (list (cons #\0 `(retrieve ,NAME)))))
                              (save-fn name (ss-alist) state)
                              (er soft
                                ctx
                                "The above :INSTRUCTIONS hint failed.  ~
                                     For a discussion of ``failed'', follow ~
                                     the link to the SEQUENCE command under ~
                                     :DOC proof-builder-commands."))))
                        (t (value (proof-builder-clause-list state)))))))
                (cond (erp (silent-error state))
                  (t (value (cons clause-list (state-stack)))))))))))))

(defun proof-builder-cl-proc
  (cl instr-list state)
  (mv-let (erp clause-list/state-stack state)
    (proof-builder-cl-proc-1 cl instr-list state)
    (cond (erp (mv erp clause-list/state-stack state nil))
      (t (mv erp
          (car clause-list/state-stack)
          state
          (let ((state-stack (cdr clause-list/state-stack)))
            (and (consp state-stack)
              (ttree-to-summary-data (access pc-state (car state-stack) :tag-tree)))))))))

(define-trusted-clause-processor proof-builder-cl-proc nil)

(add-custom-keyword-hint :instructions (splice-keyword-alist :instructions (list :clause-processor (list :function 'proof-builder-cl-proc :hint (kwote val)))
    keyword-alist))