ev-find-rules

(defun find-ev-counterpart
  (ev world)
  (car (remove ev (fgetprop ev 'siblings nil world))))

(defun find-matching-rule
  (hyps equiv lhs rhs lemmas)
  (if (atom lemmas)
    nil
    (or (let* ((rune (access rewrite-rule (car lemmas) :rune)) (rhyps (access rewrite-rule (car lemmas) :hyps))
          (rlhs (access rewrite-rule (car lemmas) :lhs))
          (rrhs (access rewrite-rule (car lemmas) :rhs))
          (requiv (access rewrite-rule (car lemmas) :equiv)))
        (and (or (eq hyps :dont-care) (equal rhyps hyps))
          (or (eq lhs :dont-care) (equal rlhs lhs))
          (or (eq rhs :dont-care) (equal rrhs rhs))
          (or (eq equiv :dont-care) (equal requiv equiv))
          rune))
      (find-matching-rule hyps equiv lhs rhs (cdr lemmas)))))

(defun ev-find-fncall-rule-in-lemmas
  (ev fn lemmas)
  (find-matching-rule `((consp x) (equal (car x) ',FN))
    'equal
    `(,EV x a)
    :dont-care lemmas))

(defun ev-find-fncall-rule
  (ev fn world)
  (find-matching-rule `((consp x) (equal (car x) ',FN))
    'equal
    `(,EV x a)
    :dont-care (fgetprop ev 'lemmas nil world)))

(defun ev-find-fncall-generic-rule
  (ev world)
  (let ((ev-lst (find-ev-counterpart ev world)))
    (find-matching-rule '((consp x) (synp 'nil
          '(syntaxp (not (equal a ''nil)))
          '(if (not (equal a ''nil))
            't
            'nil))
        (not (equal (car x) 'quote)))
      'equal
      `(,EV x a)
      `(,EV (cons (car x) (kwote-lst (,EV-LST (cdr x) a))) 'nil)
      (fgetprop ev 'lemmas nil world))))

(defun ev-find-variable-rule
  (ev world)
  (find-matching-rule '((symbolp x))
    'equal
    `(,EV x a)
    '(if x
      (cdr (assoc-equal x a))
      'nil)
    (fgetprop ev 'lemmas nil world)))

(defun ev-find-nonsymbol-atom-rule
  (ev world)
  (find-matching-rule '((not (consp x)) (not (symbolp x)))
    'equal
    `(,EV x a)
    ''nil
    (fgetprop ev 'lemmas nil world)))

(defun ev-find-bad-fncall-rule
  (ev world)
  (find-matching-rule '((consp x) (not (consp (car x))) (not (symbolp (car x))))
    'equal
    `(,EV x a)
    ''nil
    (fgetprop ev 'lemmas nil world)))

(defun ev-find-quote-rule
  (ev world)
  (find-matching-rule '((consp x) (equal (car x) 'quote))
    'equal
    `(,EV x a)
    '(car (cdr x))
    (fgetprop ev 'lemmas nil world)))

(defun ev-find-lambda-rule
  (ev world)
  (let ((ev-lst (find-ev-counterpart ev world)))
    (find-matching-rule '((consp x) (consp (car x)))
      'equal
      `(,EV x a)
      `(,EV (car (cdr (cdr (car x))))
        (pairlis$ (car (cdr (car x))) (,EV-LST (cdr x) a)))
      (fgetprop ev 'lemmas nil world))))

(defun ev-lst-find-atom-rule
  (ev-lst world)
  (find-matching-rule '((not (consp x-lst)))
    'equal
    `(,EV-LST x-lst a)
    ''nil
    (fgetprop ev-lst 'lemmas nil world)))

(defun ev-lst-find-cons-rule
  (ev-lst world)
  (let ((ev (find-ev-counterpart ev-lst world)))
    (find-matching-rule '((consp x-lst))
      'equal
      `(,EV-LST x-lst a)
      `(cons (,EV (car x-lst) a) (,EV-LST (cdr x-lst) a))
      (fgetprop ev-lst 'lemmas nil world))))