Open fresheed opened 4 years ago
These lemmas are used in the 'relive' project. Most of them are general, except for LTS_traceE' which, together with existing LTS_traceE, states the equivalence of two LTS trace definitions.
LTS_traceE'
LTS_traceE
These lemmas are used in the 'relive' project. Most of them are general, except for
LTS_traceE'which, together with existingLTS_traceE, states the equivalence of two LTS trace definitions.