Induction on two expressions simultaneously.
Function:
(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:
(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:
(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))))