Fair enough :) that&#39;ll teach me to hypothesize something without thinking about it! I guess I could amend my coinductive proof:<div><br></div><div><a href="http://hpaste.org/paste/42516/mirrormirror_with_bottom#p42517">http://hpaste.org/paste/42516/mirrormirror_with_bottom#p42517</a></div>
<div><br></div><div>does that cover bottom-ness adequately? I can&#39;t say I&#39;ve thought through it terribly carefully.<br><br><div class="gmail_quote">On Thu, Dec 23, 2010 at 12:30 PM, Ryan Ingram <span dir="ltr">&lt;<a href="mailto:ryani.spam@gmail.com">ryani.spam@gmail.com</a>&gt;</span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;"><div class="im">On Thu, Dec 23, 2010 at 8:19 AM, Daniel Peebles &lt;<a href="mailto:pumpkingod@gmail.com">pumpkingod@gmail.com</a>&gt; wrote:<br>

&gt; Simulating bottoms wouldn&#39;t be too hard, but I don&#39;t think the statement is<br>
&gt; even true in the presence of bottoms, is it?<br>
<br>
</div>Isn&#39;t it?<br>
<div class="im"><br>
data Tree a = Tip | Node (Tree a) a (Tree a)<br>
<br>
mirror :: Tree a -&gt; Tree a<br>
</div>mirror Tip = Tip<br>
<div class="im">mirror (Node x y z) = Node (mirror z) y (mirror x)<br>
<br>
</div>--<br>
<br>
-- base cases<br>
mirror (mirror _|_)<br>
 = mirror _|_<br>
 = _|_<br>
<br>
mirror (mirror Tip)<br>
 = mirror Tip<br>
 = Tip<br>
<br>
-- inductive case<br>
mirror (mirror (Node x y z))<br>
  = mirror (Node (mirror z) y (mirror x))<br>
  = Node (mirror (mirror x)) y (mirror (mirror z))<br>
  -- induction<br>
  = Node x y z<br>
<font color="#888888"><br>
  -- ryan<br>
</font></blockquote></div><br></div>