		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-induction-schemas

Expressions-induction2

Induction on two expressions simultaneously.

Definitions and Theorems

Function: expression-induct2

(defun expression-induct2 (old new)
 (declare (xargs :guard (and (expressionp old)
                             (expressionp new))))
 (let ((__function__ 'expression-induct2))
  (declare (ignorable __function__))
  (expression-case
     old
     :path (expression-case new
                            :path nil
                            :literal nil
                            :funcall nil)
     :literal (expression-case new
                               :path nil
                               :literal nil
                               :funcall nil)
     :funcall
     (expression-case new
                      :path nil
                      :literal nil
                      :funcall (funcall-induct2 old.get new.get)))))

Function: expression-list-induct2

(defun expression-list-induct2 (old new)
  (declare (xargs :guard (and (expression-listp old)
                              (expression-listp new))))
  (let ((__function__ 'expression-list-induct2))
    (declare (ignorable __function__))
    (cond ((endp old) nil)
          ((endp new) nil)
          (t (list (expression-induct2 (car old) (car new))
                   (expression-list-induct2 (cdr old)
                                            (cdr new)))))))

Function: funcall-induct2

(defun funcall-induct2 (old new)
  (declare (xargs :guard (and (funcallp old) (funcallp new))))
  (let ((__function__ 'funcall-induct2))
    (declare (ignorable __function__))
    (expression-list-induct2 (funcall->args old)
                             (funcall->args new))))

Subtopics

Funcall-induct2
Expression-list-induct2
Expression-induct2