Evaluating App on Sample Input

ACL2 !>(app nil '(x y z))
(X Y Z)

ACL2 !>(app '(1 2 3) '(4 5 6 7)) (1 2 3 4 5 6 7)

ACL2 !>(app '(a b c d e f g) '(x y z)) ; click here for an explanation (A B C D E F G X Y Z)

ACL2 !>(app (app '(1 2) '(3 4)) '(5 6)) (1 2 3 4 5 6)

ACL2 !>(app '(1 2) (app '(3 4) '(5 6))) (1 2 3 4 5 6)

ACL2!>(let ((a '(1 2)) (b '(3 4)) (c '(5 6))) (equal (app (app a b) c) (app a (app b c)))) T

As we can see from these examples, ACL2 functions can be executed more or less as Common Lisp.

The last three examples suggest an interesting property of app.