Revisiting the Admission of App

Here is the definition of app again with certain parts highlighted. If you are taking the Walking Tour, please read the text carefully and click on each of the links below, except those marked . Then come back here.

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