Tree bisimilarity

Define (coinductively) the notion of bisimilarity on LTree A.
Prove that it an equivalence on LTree A.
Prove that two trees t1 and t2 are bisimilar if and only if the function LTree_label always returns the same result for t1 and t2.


You may use all the developments made for the preceding exercises in this thread.


Follow this link

Going home
Pierre Castéran