Question 235

[Leo Schnee]

I have this as my induction step:

(~ (endp x))
^
(rev1 (rest x) a) = (app (rev (rest x)) a)
-->
(rev1 x a) = (app (rev x) a)

Is this correct? I can't seem to get anywhere after about two steps,
any help / hints would be appreciated.

Thanks.

[Aaron Stolarz]

That's the induction step I have, but I'm stuck after about 6 steps...

[Leo Schnee]

Ok, I think I have it figured out. It has to do with the induction
which is explained more in depth on page 157. From what I understand
you can use {x <-- (rest x), a <-- (cons (first x) a) } as your
substitution step, and then you can actually solve it.

[Behnam Robatmili]

Good point Leo. I'm happy your figured it.

{x <-- (rest x), a <-- (cons (first x) a) } is the right substitution
for this induction.
Remember from the book that to write down the induction step, you
should replace the induction variable, here x, with (rest x). However,
the other variables, here a, can be replaced by anything! So yes, a
can be replaced by (cons (first x) a).

Thanks,
Behnam

> 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.