The main contribution of this PR is lemma tomset_labelsK, which is a part of the proof that tomsets are isomorphic to sequences.
Additional features introduced in this PR:
conseq_num property of posets, asserting that events of the poset form a consecutive sequence of events, from 0 to n
changed definition of fresh_seq to simplify proof of tomset_labelsK, as a by-product simplify proofs in pomset_lts.v to remove unnecessary case-analysis.
The main contribution of this PR is lemma
tomset_labelsK, which is a part of the proof that tomsets are isomorphic to sequences.Additional features introduced in this PR:
conseq_numproperty of posets, asserting that events of the poset form a consecutive sequence of events, from0tonfresh_seqto simplify proof oftomset_labelsK, as a by-product simplify proofs inpomset_lts.vto remove unnecessary case-analysis.