Relating Machine type to the Global Lift type
Currently, we have a global Lift type (L^gl X = ∀ k . L℧ k X) and a type of Machines.
We would like to relate these types by showing L^gl X ≅ Machine (∀ k. X)
. We also want to relate the notion of step-insensitive/weak bisimilarity defined on L^gl X, to that defined on Machines.
This will involve the following steps:
-
Show that L^gl X ≅ Machine (∀ k. X) -
Define weak/step-insensitive bisimilarity on Machines -
Relate step-insentitive bisimilarity on L^gl to step-insensitive bisimilarity of Machines