Closed eupp closed 2 years ago
Several auxiliary definitions and lemmas for pomsets.
lFsPreposet.Build.build
lfspreposet
lfsp_tseq
lfsp_idx
lfsp_event
lfsposet_eqP
choiceType
countType
lfsposet
pomset
Several auxiliary definitions and lemmas for pomsets.
lFsPreposet.Build.build
to buildlfspreposet
from finite graph (labeling function and covering relation/Hasse diagram)lfsp_tseq
--- topological sorting of posetlfsp_idx
--- index of event in topological sortinglfsp_event
--- get event by its indexlfsposet_eqP
--- reflect lemma for equality over lposetschoiceType
andcountType
instances forlfspreposet
,lfsposet
,pomset
.