The Admission of App
Here is what it looks like to submit the definition of
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 O< (which is known to be well-founded on the domain recognized by O-P) 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)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) APP
The text between the lines above is one interaction with the ACL2 command loop. Interacting with the latest version of ACL2 may not produce the very same output, but we trust you'll recognize the basics.
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.