Question 225

[Mathew Vogel]

A bit of a quick question about this problem. In this proof, from part
6 to part 7, are the axioms first-cons and rest-cons even used? It
seems like the proof can be solved without those axioms, and I do not
even see how to use them in the part of the proof. If anyone has found
a way, could you kind of enlighten me a bit on how to use them for
this part?

[Xu Wang]

I emailed Dr. Moore about this problem and he said you don't need to
use first-cons or rest-cons.

Xu
Quoting Mathew Vogel <mathew...@gmail.com>:

> To unsubscribe from this group, send email to
> utexas-cs313k-spring2010+unsubscribegooglegroups.com or reply to
> this email with the words "REMOVE ME" as the subject.
>

[J Strother Moore]

Hi Mathew. You're right. It was wrong for me to
say that first-cons and rest-cons were needed in
step 7. Last year, I hadn't listed app-cons as a
lemma to use there, and instead listed def app.
If the definition of app is used, then you really
need those others. But if app-cons is used, you
don't. Several of you have caught this mistake
and I'm really glad. Thanks.

J