Simulation Transitivity

[minkiminki]

Let foo be o <- Choose Ord;; do sth finishes in o steps.
There are simulations between foo;; foo;; tau Ret 0 and foo;; tau Ret 0,
and between foo;; tau Ret 0 and tau;; Ret 0.
However, foo;; foo;; tau Ret 0 ~ tau Ret 0 is not true. i.e. simulation is not transitive!

The problem is that there is no upper bound of possible simulation indexes.
If each index is smaller than kappa, or if we allow an itree to branch only with a set less than Ord (which is not possible due to Hoareproof1),
we may be able to prove transitivity.
(Roughly saying, if itr0 ~ itr1 with an index i0 and itr1 ~ itr2 with an index i1,
itr0 ~ itr2 with the kappa * i0 + i1)

Or, we can use transitivity of behavioral refinement directly, instead of transitivity of simulation.
Then, we should define intermediate interaction trees.