<br>
<blockquote class="gmail_quote" style="margin: 0pt 0pt 0pt 0.8ex; border-left: 1px solid rgb(204, 204, 204); padding-left: 1ex;">Actually, you are missing the point. ;)  The point of bisimulations is<br>
that they are defined *coinductively*, so they let you work with<br>
potentially infinite data structures.  In your example, proving that<br>
xs and ys are in the relation R really is that simple -- 1 = 1, and<br>
then to complete the proof we are allowed to use the coinduction<br>
hypothesis that xs and ys are in the relation R, since they are<br>
guarded by a constructor (:).<br>
<br>
Dan, does this help answer your original question?  If not I can try<br>
to give a more detailed answer in the morning.<br></blockquote><br>I 
understand the coinduction principle for data structures like streams 
(e.g., Felipe&#39;s example) and finitely branching trees (from papers like 
&quot;A calculus of binary trees&quot;). In general, for lists and types 
constructed from arrow, product, and so on, it&#39;s easy to define 
conditions for a relation to be a bisimulation. For instance, I know 
that a relation <i>R</i> is a bisimulation over <i>n</i>-branching trees <i>t1 </i>and <i>t2</i> (for some <i>n</i>) if their roots are equal and each of their subtrees are in <i>R</i>. My problem is, specifically, with the case of infinitely branching trees. In Haskell, these are modeled by the data type<br>
<br><div style="margin-left: 40px;">T a = T a [T a]<br><br></div>and the possibility arises, of course, that the list [T a] is a stream. Clearly, we can&#39;t just say that a relation <i>R</i> is a bisimulation on trees <i>t1</i> and <i>t2</i> of type T a if their root values are equal and their <i>lists</i>
 of subtrees are equal. Because if the lists are infinite, we have to 
prove that they are bisimilar. And the coinduction principle for lists 
requires us to have established that the head of each list is equal. But
 this is what we&#39;re trying to prove!<br><br>So my questions is: what 
must be established to show that a relation is a bisimulation on an 
infinitely branching tree of type T a? This question arises because I&#39;m 
having trouble &quot;combining&quot; the individual principles for trees and 
lists.<br>