boot-strap-pass-2-b

(defun pair-fns-with-measured-subsets
  (fns wrld acc)
  (declare (xargs :guard (and (symbol-listp fns)
        (plist-worldp wrld)
        (true-listp acc))))
  (cond ((endp fns) (reverse acc))
    (t (pair-fns-with-measured-subsets (cdr fns)
        wrld
        (cons (let* ((fn (car fns)) (justification (getpropc fn 'justification nil wrld))
              (ms0 (and (weak-justification-p justification)
                  (access justification justification :measure)))
              (ms (and ms0
                  (if (and (pseudo-termp ms0) (system-pseudo-termp ms0 wrld))
                    ms0
                    (cons :? (access justification justification :subset))))))
            (cons fn ms))
          acc)))))

(defun new-verify-guards-fns1
  (wrld installed-wrld acc)
  (declare (xargs :guard (and (plist-worldp wrld)
        (plist-worldp installed-wrld)
        (symbol-listp acc))))
  (cond ((or (endp wrld)
       (and (eq (caar wrld) 'command-landmark)
         (eq (cadar wrld) 'global-value)
         (equal (safe-access-command-tuple-form (cddar wrld))
           '(exit-boot-strap-mode)))) (pair-fns-with-measured-subsets (strict-merge-sort-symbol< acc)
        installed-wrld
        nil))
    ((and (eq (cadar wrld) 'symbol-class)
       (eq (cddar wrld) :common-lisp-compliant)
       (not (eq (caar wrld) 'do$))
       (getpropc (caar wrld) 'predefined nil installed-wrld)) (new-verify-guards-fns1 (cdr wrld)
        installed-wrld
        (cons (caar wrld) acc)))
    (t (new-verify-guards-fns1 (cdr wrld) installed-wrld acc))))

(defun new-verify-guards-fns
  (state)
  (declare (xargs :stobjs state))
  (let ((wrld (w state)))
    (new-verify-guards-fns1 wrld wrld nil)))

(defun system-verify-guards-aux
  (fns-alist acc acc1 old-num)
  (declare (xargs :guard (and (alistp fns-alist)
        (nat-listp (strip-cars fns-alist))
        (symbol-alistp (strip-cdrs fns-alist))
        (true-list-listp acc1))
      :ruler-extenders :lambdas))
  (let* ((num/pair (car fns-alist)) (num (car num/pair))
      (entry (cdr num/pair))
      (next (and fns-alist
          `(,(CAR ENTRY) ,@(LET ((MEASURE (CDR ENTRY)))
    (AND MEASURE `((DECLARE (XARGS :MEASURE ,MEASURE))))))))
      (same-num-p (and fns-alist (eql num old-num)))
      (acc (if (or (null acc1) same-num-p)
          acc
          (list* `(skip-proofs (verify-termination-boot-strap ,@ACC1))
            `(skip-proofs (verify-guards ,(CAAR ACC1)))
            acc))))
    (cond ((endp fns-alist) acc)
      (t (system-verify-guards-aux (cdr fns-alist)
          acc
          (if same-num-p
            (cons next acc1)
            (list next))
          num)))))

(defun cons-absolute-event-numbers
  (fns-alist wrld acc)
  (declare (xargs :guard (and (symbol-alistp fns-alist)
        (plist-worldp wrld)
        (alistp acc))))
  (cond ((endp fns-alist) acc)
    (t (cons-absolute-event-numbers (cdr fns-alist)
        wrld
        (acons (or (getpropc (caar fns-alist) 'absolute-event-number nil wrld)
            (er hard?
              'cons-absolute-event-numbers
              "The 'absolute-event-number property is missing ~
                            for ~x0."
              (caar fns-alist)))
          (car fns-alist)
          acc)))))

(defun sort->-absolute-event-number
  (fns-alist wrld)
  (declare (xargs :mode :program))
  (merge-sort-car-> (cons-absolute-event-numbers fns-alist wrld nil)))

(defun system-events-fn
  (events)
  (declare (xargs :guard (true-listp events)))
  (cond ((endp events) nil)
    (t (cons `(system-event ,(CAR EVENTS))
        (system-events-fn (cdr events))))))

(defun-sk apply$-equivalence
  (fn1 fn2)
  (declare (xargs :verify-guards t :guard t))
  (forall (args)
    (equal (ec-call (apply$ fn1 args))
      (ec-call (apply$ fn2 args)))))

(defun fn-equal
  (fn1 fn2)
  (declare (xargs :mode :logic :guard t))
  (if (equal fn1 fn2)
    t
    (and (tamep-functionp fn1)
      (tamep-functionp fn2)
      (apply$-equivalence fn1 fn2))))

(defun mempos
  (e lst)
  (declare (xargs :guard (true-listp lst)))
  (cond ((endp lst) 0)
    ((equal e (car lst)) 0)
    (t (+ 1 (mempos e (cdr lst))))))