 C0 formula_1

C1 If a transition formula_2 depends on some transition relation in formula_3, this transition cannot be invoked until some transition in the ample set is executed.Conditions C0 and C1 are sufficient for preserving all the deadlocks in the state space.Further restrictions are needed in order to preserve more nuanced properties.