The Admission of App

Here is what it looks like to submit the definition of app to ACL2:

ACL2 !>(defun app (x y)
  (cond ((endp x) y)
        (t (cons (car x) 
                 (app (cdr x) y)))))


The admission of APP is trivial, using the relation E0-ORD-< (which
is known to be well-founded on the domain recognized by E0-ORDINALP)
and the measure (ACL2-COUNT X).  We observe that the type of APP is
described by the theorem (OR (CONSP (APP X Y)) (EQUAL (APP X Y) Y)).
We used primitive type reasoning.


Summary
Form:  ( DEFUN APP ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings:  None
Time:  0.03 seconds (prove: 0.00, print: 0.00, other: 0.03)
 APP

The text between the lines above is one interaction with the ACL2 command loop.

Above you see the user's input and how the system responds. This little example shows you what the syntax looks like and is a very typical successful interaction with the definitional principle.

Let's look at it a little more closely.