Here is the
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 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)) Warnings: None Time: 0.03 seconds (prove: 0.00, print: 0.00, other: 0.03) APP