DCR-ExecutionEquivalence