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.

Resources

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

Solution

Follow this link

Going home

Pierre Castéran