Question 228

[stevecahail]

Has anyone tried to do Question 228 yet? I have been working on it for
quite a while and have not been able to prove the induction step.

Here is where I am currently stuck:

((~ (endp a))
&&
((rev (mapnil (rest a))) = (mapnil (rev (rest a))))
-->
((app (rev (mapnil (rest a)))
(cons nil nil))
=
(app (mapnil (rev (rest a)))
(mapnil (cons (first a) nil))))

<--> {Hyp}

((~ (endp a))
&&
((rev (mapnil (rest a))) = (mapnil (rev (rest a))))
-->
((app (rev (mapnil (rest a)))
(cons nil nil))
=
(app (rev (mapnil (rest a)))
(mapnil (cons (first a) nil))))

I really have no idea where to go from here. I'm not sure which side
of the equality in my hypothesis to use [(rev (mapnil (rest a))) or
(mapnil (rev (rest a)))] and that (cons nil nil) in the left hand side
of the conclusion is pretty troublesome. Any ideas or things that I
am doing wrong?

[stevecahail]

Also, I'm pretty sure my induction step is right, but I'll post it
here in case it isn't. I am inducting on a.

Induction Step:

((~ (endp a))
&&
((rev (mapnil (rest a))) = (mapnil (rev (rest a))))
-->

((rev (mapnil a)) = (mapnil (rev a)))

[Bryan Garcia]

That is the typical "bogus induction step" look on page 154

[Brad Burlage]

You can use the definition of mapnil to simplify (mapnil (cons (first
a) nil)). If you'd like, I can send you my proof.

Brad Burlage

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